Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker

DOI10.1007/s001659970003zbMath0966.68124OpenAlexW1977237988MaRDI QIDQ1578397

Mieke Massink, Diego Latella, István Majzik

Publication date: 27 August 2000

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001659970003

zbMATH Keywords

unified modelling languagestatechart diagrams

Mathematics Subject Classification ID

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

Related Items (11)

Formalising concurrent UML state machines using coloured Petri nets ⋮ A state/event-based model-checking approach for the analysis of abstract system properties ⋮ An accessible verification environment for UML models of services ⋮ Towards Verifying Model Transformations ⋮ Integrating a formal method into a software engineering process with UML and Java ⋮ Model Checking of Extended OCL Constraints on UML Models in SOCLe ⋮ On testing UML statecharts ⋮ Reconciling statechart semantics ⋮ Synergistic verification and validation of systems and software engineering models ⋮ Towards automated software model checking using graph transformation systems and bogor ⋮ Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking

Uses Software

• SPIN

This page was built for publication: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker