Deadlock Detection Based on Automatic Code Generation from Graphical CSP Models

D.S. Jovanovic, Geert K. Liet, Johannes F. Broenink

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    94 Downloads (Pure)


    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 languageUndefined
    Title of host publicationProceedings of the 5th Progress Symposium on Embedded Systems
    EditorsF. Karelse
    Place of PublicationNieuwegein
    ISBN (Print)90-73461-41-3
    Publication statusPublished - 30 Sep 2004
    Event5th PROGRESS Symposium on Embedded Systems 2004 - Nieuwegein, Netherlands
    Duration: 20 Oct 200420 Oct 2004
    Conference number: 5

    Publication series

    PublisherSTW Technology Foundation


    Conference5th PROGRESS Symposium on Embedded Systems 2004
    Abbreviated titlePROGRESS


    • IR-49240
    • METIS-221419

    Cite this