A compositional axiomatisation of safety and liveness properties for statecharts

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

Samenvatting

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.
Originele taal-2Engels
TitelSemantics for Concurrency (Proceedings International BCS-FACS Workshop, Leicester, UK, July 1990)
RedacteurenM.Z. Kwiatkowska, M.W. Shields, R.M. Thomas
Plaats van productieBerlin
UitgeverijSpringer
Pagina's242-261
ISBN van geprinte versie3-540-19625-0
StatusGepubliceerd - 1990

    Vingerafdruk

Citeer dit

Hooman, J. J. M., Ramesh, S., & Roever, de, W. P. (1990). A compositional axiomatisation of safety and liveness properties for statecharts. In M. Z. Kwiatkowska, M. W. Shields, & R. M. Thomas (editors), Semantics for Concurrency (Proceedings International BCS-FACS Workshop, Leicester, UK, July 1990) (blz. 242-261). Berlin: Springer.