On formal semantics of statecharts as supported by STATEMATE

We formalize the rigorous but informal description of the semantics of statecharts given by Harel and Naamad in [3] which corresponds to the semantics underlying the commercial tool STATEMATE. We closely follow [3] to increase confidence that our semantics actually corresponds to their informal description. In [3] the semantics is given by a detailed description of the so-called basic step algorithm. Based on a formalization of this basic step algorithm we associate to each statechart a transition system which defines its computations. This is the first step towards linking the language of statecharts as supported by STATEMATE with other automatic verification tools. Our formalization uses Z notation rather than "standard mathematics". This allows to structure the definition of the formal semantics and to use tools like type-checkers.

• Publication year

  1997

• Venue

  FME 1997

• Publication date

  1997-07-14

• Fields of study

  Computer Science

• Identifiers
  DOI 10.14236/EWIC/FA1997.12
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The STATEMATE semantics of statecharts

  1996cited by this paper
• Completeness and Consistency in Hierarchical State-Based Requirements

  1996influential reference
• A Comparison of Statecharts Variants

  1994cited by this paper
• Requirements Specification for Process-Control Systems

  1994cited by this paper
• A Process Algebraic Semantics for Statecharts via State Refinement

  1994cited by this paper
• A Compositional Axiomatization of Statecharts

  1992cited by this paper
• The Esterel Synchronous Programming Language: Design, Semantics, Implementation

  1992cited by this paper
• Operational and Compositional Semantics of Synchronous Automaton Compositions

  1992cited by this paper
• Semantics of reactive systems : comparison and full abstraction

  1991cited by this paper
• Introduction to Design Choices in the Semantics of Statecharts

  1991cited by this paper
• What is in a Step: On the Semantics of Statecharts

  1991cited by this paper
• On the Formal Semantics of Statecharts (Extended Abstract)

  1987influential reference
• Statecharts: A Visual Formalism for Complex Systems

  1987cited by this paper
• Towards Eecient Model Checking Statecharts: a Statecharts to Promela Complier

  year unknowncited by this paper

• A From a Formalized Parallel Action Language to its Efficient Code Generation

  2023cites this paper
• Semantic Variations among UML StateMachines

  2019cites this paper
• Model-based Network Fault Injection for IoT Protocols

  2019cites this paper
• Hierarchical featured state machines

  2019influential citation
• Automatic generation of configurable test-suites for software product lines

  2017cites this paper
• From a Formalized Parallel Action Language to Its Efficient Code Generation

  2017influential citation
• Towards Executable Specifications for Case Management Processes

  2017cites this paper
• Semantics of Higraphs for Process Modeling and Analysis

  2016cites this paper
• A coordination model for agent behaviors using hierarchical finite state machine with inter-level concurrency

  2016cites this paper
• Programming Embedded Manycore : Refinement and Optimizing Compilation of a Parallel Action Language for Hierarchical State Machines. (Programmation de systèmes embarqués many-core : Raffinement et compilation optimisante d'un langage d'action parallèle pour machines à états hiérarchiques)

  2016influential citation
• Extending statecharts to model system interactions

  2015cites this paper
• Refinement-based verification of implementations of Stateflow charts

  2014cites this paper
• Mapping of UML Diagrams to Extended Petri Nets for Formal Verification

  2013influential citation
• Monitoring and Diagnosis for Autonomic Systems: A Requirement Engineering Approach

  2010cites this paper
• Specialization and Validation of Statecharts in OWL

  2010cites this paper
• Using Modeler Intent in Software Engineering

  2010cites this paper
• Diagnosing software using statecharts

  2010influential citation
• An Operational Semantics for UML RT-Statechart in Model Checking Context

  2009cites this paper
• Gaia Agents Implementation through Models Transformation

  2009cites this paper
• Hardware-in-the-loop simulation testbed design of FCS-VP based on statemate

  2008cites this paper
• MOOA: An Object Oriented Formalism for Wireless Sensor Networks

  2008cites this paper
• Graphical inheritance notation for state-based classes

  2007cites this paper
• Real-Time Veri cation of Statemate DesignsUdo

  2007cites this paper
• Verifying Statemate Statecharts Using CSP and FDR

  2006cites this paper
• Compositional Semantics and Refinement of Statecharts

  2006cites this paper
• An integrated framework for the analysis of dependable interactive systems (IFADIS): Its tool support and evaluation

  2006cites this paper
• Die-Verification of STATEMATE Des igns

  2006cites this paper
• Semantic variations among UML statemachines

  2006cites this paper
• ON SPECIFYING COMPLEX SYSTEMS THROUGH STOCHASTIC STATECHARTS FOR PERFORMANCE ANALYSIS

  2005cites this paper
• An operational semantics for Stateflow

  2004cites this paper
• A framework and supporting tool for the model-based analysis for dependable interactive systems in the context of industrial design

  2004cites this paper
• Integrating model checking with the industrial design of interactive systems

  2004cites this paper
• Formalizing the semantics of UML statecharts with Z

  2004cites this paper
• An Approach to Formalizing the Semantics of UML Statecharts

  2004cites this paper
• Hierarchical modeling and analysis of timed systems

  2003cites this paper
• An Approach of Model Checking UML Statecharts

  2003influential citation
• Translating Statecharts to B

  2002cites this paper
• Automated generation of high-integrity test suites from graphical specifications

  2002cites this paper
• Defining OCL expressions using templates.

  2002cites this paper
• On the Formal Semantics of VisualSTATE Statecharts

  2002cites this paper
• Performance Evaluation of Complex Systems: Queuing Statecharts Approach

  2002influential citation
• Structure and Hierarchy in Real-Time Systems

  2002cites this paper
• Verify UML statecharts with SMV

  2001cites this paper
• Model checking UML statecharts

  2001cites this paper
• Integrating behavioural design into the virtual environment development process

  2001cites this paper
• Lfm2000 - Fifth NASA Langley Formal Methods Workshop

  2000cites this paper
• Automated V&V for high integrity systems, a targeted formal methods approach

  2000cites this paper
• Automatic Generation of Natural Language Documentation from Statecharts by

  2000cites this paper
• Model-based Automated Analysis for the Development of Dependable Interactive Systems

  2000cites this paper
• A compositional approach to statecharts semantics

  2000cites this paper
• Early hazard identification of chemical plants with statechart modelling techniques

  2000cites this paper
• Towards Automated Unit Testing of Statechart Implementations

  1999cites this paper
• Statecharts Via Process Algebra

  1999cites this paper
• Higher Order Process-Algebraic Axiomatizations of Statecharts Variants

  1998cites this paper
• Implementing statecharts in PROMELA/SPIN

  1998cites this paper
• Tamagotchis Need Not Die { Veri cation ofStatemate DesignsUdo

  1998cites this paper
• Tamagotchis Need Not Die - Verification of STATEMENT Design

  1998cites this paper
• Hierarchical Automata as Model for Statecharts

  1997cites this paper
• Combining Z and Temporal Interval Logics for the Formalization of Properties and Behaviors of Embedded Systems

  1997influential citation
• Some Thoughts on Statecharts, 13 Years Later

  1997cites this paper
• Towards Eecient Model Checking Statecharts: a Statecharts to Promela Complier

  year unknowncites this paper
• Statechart Slicing

  year unknowncites this paper