Deadlock Detection Based on Automatic Code Generation from Graphical CSP Models


Jovanovic, Dusko and Liet, Geert K. and Broenink, Jan F. (2004) Deadlock Detection Based on Automatic Code Generation from Graphical CSP Models. In: PROGRESS 2004 Symposium on Embedded Systems, Oct. 30, 2004, Nieuwegein, the Netherlands (pp. pp. 70-89).

open access
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.
Item Type:Conference or Workshop Item
Copyright:© 2004 STW Technology Foundation
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 221419