Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    On Formal Semantics of Statecharts as Supported by STATEMATE

    2nd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th July 1997


    E. Mikk, Y. Lakhnech, C. Petersohn & M. Siegel


    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.


    PDF filePDF Version of this Paper (156kb)