Deadlock Detection Based on Automatic Code Generation from Graphical CSP Models

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.