Abstract
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
Original language | English |
---|---|
Pages (from-to) | 289-335 |
Number of pages | 47 |
Journal | Theoretical Computer Science |
Volume | 101 |
Issue number | 2 |
DOIs | |
Publication status | Published - 1992 |