Deadlock Detection Based on Automatic Code Generation from Graphical CSP Models


Share/Save/Bookmark

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
[img]
Preview
PDF
867kB
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/49240
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 221419