A compositional axiomatisation of Statecharts

J.J.M. Hooman, S. Ramesh, W.P. Roever, de

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

32 Citaten (Scopus)


Statecharts is a behavioural specification language proposed for specifying large real-time, event-driven reactive systems. It is a graphical language based on state-transition diagrams for finite state machines extended with many features like hierarchy, concurrency, broadcast communication and time-out. We supply Statecharts with a compositional axiomatization for both safety and liveness properties. By generating external events symbolically, Statecharts can be executed, thereby turning it into a programming language for real-time concurrency (as well as enabling rapid prototyping). As such it is well suited for compositional program verification. In addition to our compositional axiomatic system, we give a denotational semantics and prove that the axiomatization is sound and relatively complete with respect to this semantics
Originele taal-2Engels
Pagina's (van-tot)289-335
Aantal pagina's47
TijdschriftTheoretical Computer Science
Nummer van het tijdschrift2
StatusGepubliceerd - 1992


Citeer dit

Hooman, J. J. M., Ramesh, S., & Roever, de, W. P. (1992). A compositional axiomatisation of Statecharts. Theoretical Computer Science, 101(2), 289-335. https://doi.org/10.1016/0304-3975(92)90053-I