Abstract
The paper describes a way of using standard formal analysis tools for checking deadlock freedom in graphical models for CSP descriptions of concurrent systems. The models capture specification of a possible concurrent implementation of a system to be realized. Building the graphical models and transforming them to a textual machine-readable form is supported by a CASE tool under development called gCSP. The model transformation allows checking certain important behavioral properties of a candidate implementation before it gets refined with application specific details and deployed in exploitation conditions. A short introduction to the modeling forms and tools is given before a demonstration of the checking procedure on two examples of (embedded) control systems is presented. These systems are modeled by a special class of CSP processes, for which a graphical mechanism for revealing and healing ill-posed concurrent compositions is prototyped too.
Original language | Undefined |
---|---|
Title of host publication | Proceedings of the 5th Progress Symposium on Embedded Systems |
Editors | F. Karelse |
Place of Publication | Nieuwegein |
Publisher | STW |
Pages | 70-89 |
ISBN (Print) | 90-73461-41-3 |
Publication status | Published - 30 Sep 2004 |
Event | 5th PROGRESS Symposium on Embedded Systems 2004 - Nieuwegein, Netherlands Duration: 20 Oct 2004 → 20 Oct 2004 Conference number: 5 |
Publication series
Name | |
---|---|
Publisher | STW Technology Foundation |
Conference
Conference | 5th PROGRESS Symposium on Embedded Systems 2004 |
---|---|
Abbreviated title | PROGRESS |
Country/Territory | Netherlands |
City | Nieuwegein |
Period | 20/10/04 → 20/10/04 |
Keywords
- IR-49240
- METIS-221419