A compositional axiomatisation of Statecharts

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

Research output: Contribution to journal › Article › Academic › peer-review

32 Citations (Scopus)

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 languageEnglish
Pages (from-to)289-335
Number of pages47
JournalTheoretical Computer Science
Volume101
Issue number2
DOIs
Publication statusPublished - 1992

Fingerprint

Statecharts
Axiomatization
Semantics
Concurrency
Specification languages
Rapid prototyping
Finite automata
Computer programming languages
Compositional Verification
Real-time
Denotational Semantics
Program Verification
Liveness
Reactive Systems
Rapid Prototyping
Event-driven
Specification Languages
Acoustic waves
State Transition
State Machine

Cite this

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
Hooman, J.J.M. ; Ramesh, S. ; Roever, de, W.P. / A compositional axiomatisation of Statecharts. In: Theoretical Computer Science. 1992 ; Vol. 101, No. 2. pp. 289-335.
@article{7070ff12f18c4917b4d5a22b5877c898,
title = "A compositional axiomatisation of Statecharts",
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",
author = "J.J.M. Hooman and S. Ramesh and {Roever, de}, W.P.",
year = "1992",
doi = "10.1016/0304-3975(92)90053-I",
language = "English",
volume = "101",
pages = "289--335",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "2",

}

Hooman, JJM, Ramesh, S & Roever, de, WP 1992, 'A compositional axiomatisation of Statecharts', Theoretical Computer Science, vol. 101, no. 2, pp. 289-335. https://doi.org/10.1016/0304-3975(92)90053-I

A compositional axiomatisation of Statecharts. / Hooman, J.J.M.; Ramesh, S.; Roever, de, W.P.

In: Theoretical Computer Science, Vol. 101, No. 2, 1992, p. 289-335.

Research output: Contribution to journal › Article › Academic › peer-review

TY - JOUR

T1 - A compositional axiomatisation of Statecharts

AU - Hooman, J.J.M.

AU - Ramesh, S.

AU - Roever, de, W.P.

PY - 1992

Y1 - 1992

N2 - 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

AB - 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

U2 - 10.1016/0304-3975(92)90053-I

DO - 10.1016/0304-3975(92)90053-I

M3 - Article

VL - 101

SP - 289

EP - 335

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -

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

Access to Document