A compositional axiomatisation of safety and liveness properties for statecharts

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


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 languageEnglish
Title of host publicationSemantics for Concurrency (Proceedings International BCS-FACS Workshop, Leicester, UK, July 1990)
EditorsM.Z. Kwiatkowska, M.W. Shields, R.M. Thomas
Place of PublicationBerlin
ISBN (Print)3-540-19625-0
Publication statusPublished - 1990


Dive into the research topics of 'A compositional axiomatisation of safety and liveness properties for statecharts'. Together they form a unique fingerprint.

Cite this