Abstract
Statecharts is a behavioral 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 fea
tures like hierarchy, concurrency, broadcast communication and time-out. 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 amenable to compositional pro
gram verification. We supply Statecharts with a compositional proof system
for both safety and liveness properties which we prove to be sound and (rela
tively) complete. Especially, we focus on extending compositional techniques
for proving safety properties to liveness, without immediately adopting tem
poral logic, since that formalism, elegant as it is, introduces some difficulties
with a compositional treatment of sequentiality and looping.
Original language | English |
---|---|
Title of host publication | Semantics for Concurrency (Proceedings International BCS-FACS Workshop, Leicester, UK, July 1990) |
Editors | M.Z. Kwiatkowska, M.W. Shields, R.M. Thomas |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 242-261 |
ISBN (Print) | 3-540-19625-0 |
Publication status | Published - 1990 |