Modeling statecharts and activitycharts as signal equations

Citation
Jr. Beauvais et al., Modeling statecharts and activitycharts as signal equations, ACM T SOFTW, 10(4), 2001, pp. 397-451
Citations number
34
Categorie Soggetti
Computer Science & Engineering
Journal title
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY
ISSN journal
1049331X → ACNP
Volume
10
Issue
4
Year of publication
2001
Pages
397 - 451
Database
ISI
SICI code
1049-331X(200110)10:4<397:MSAAAS>2.0.ZU;2-S
Abstract
The languages for modeling reactive systems are of different styles, like t he imperative, state-based ones and the declarative, data-flow ones. They a re adapted to different application domains. This paper, through the exampl e of the languages Statecharts and Signal, shows a way to give a model of a n imperative specification (Statecharts) in a declarative, equational one ( Signal). This model constitutes a formal model of the Statemate semantics o f Statecharts, upon which formal analysis techniques can be applied. Being a transformation from an imperative to a declarative structure, it involves the definition of generic models for the explicit management of state (in the case of control as well as of data). In order to obtain a structural co nstruction of the model, a hierarchical and modular organization is propose d, including proper management and propagation of control along the hierarc hy. The results presented here cover the essential features of Statecharts as well as of another language of Statemate: Activitycharts. As a translati on, it makes multiformalism specification possible, and provides support fo r the integrated operation of the languages. The motivation hes also in the perspective of gaining access to the various formal analysis and implement ation tools of the synchronous technology, using the DC+ exchange format, a s in the Sacres programming environment.