ICAR Research Data Repository for Knowledge Management
DSpace at IIT Bombay
View Archive InfoMetadata
| Field | Value |
| Title | A compositional axiomatization of statecharts |
| Names |
HOOMAN, JJM
(author) RAMESH, S (author) DEROEVER, WP (author) |
| Date Issued | 1992 (iso8601) |
| 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. |
| Genre | Article; Proceedings Paper |
| Topic | proof system |
| Identifier | 0304-3975 |
| Related Item | |
| Related Item | |