Scenario and Property Checking of Real-Time Systems Using a Synchronous Approach

Authors

. ANDRÉ, M-A. PERALDI-FRATI, J-P. RIGAULT

Abstract

This paper addresses the design of control-dominated systems using a synchronous approach and the UML. The work aims at formally checking the design: scenarios/controller consistency, and safety properties. For this, a strengthening of UML behavioral models is necessary: SyncCharts are used instead of Statecharts, and Sequence Diagrams are modified by adding synchronously sound constructs akin to Message Sequence Charts. The formal foundations of the approach and the associated tools are briefly presented.

Keywords

Scenario, Sequence Diagram, Statecharts, SyncCharts, UML, Design, Model Checking.

Reference

@INPROCEEDINGS{sp:isorc2001,
AUTHOR = "C. Andr\'e and M-A {Peraldi-Frati} and J-P. Rigault",
TITLE = "Scenario and Property Checking of Real-Time Systems Using
a Synchronous Approach",
sorte= "colin" ,
PAGES = {438--444},
BOOKTITLE = {Fourth IEEE International Symposium on
Object-Oriented Real-Time Distributed Computing (ISORC 2001)},
ADDRESS = {Magdeburg (Germany)},
MONTH = {May},
YEAR = {2001}
}

Paper

pdf, 83KB

Slides

pdf, 192KB