Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking

DOI10.1016/S1567-8326(01)00012-1zbMath1008.68074MaRDI QIDQ1858428

Diego Latella, Mieke Massink, Stefania Gnesi

Publication date: 13 February 2003

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

zbMATH Keywords

formal semanticsformal verificationformal specificationmodel-checkingUMLACTLJACK

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

Formalising concurrent UML state machines using coloured Petri nets ⋮ On testing UML statecharts

Uses Software

• SPIN
• CADP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Statecharts: a visual formalism for complex systems
• Model checking for action-based logics
• Advances in computing science - ASIAN '97. 3rd Asian computing science conference, Kathmandu, Nepal, December 9--11, 1997. Proceedings
• Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Inductive methods for proving properties of programs
• An action-based framework for veryfying logical and behavioural properties of concurrent systems

This page was built for publication: Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking