Static Analysis of IMC

Nataliya Skrypnyuk, Flemming Nielson, Henrik Pilegaard

    Research output: Contribution to journalJournal articleResearchpeer-review

    2 Downloads (Pure)

    Abstract

    Process algebras formalism is highly suitable for producing succinct descriptions of reactive concurrent systems. Process algebras allow to represent them in a compositional way, as processes that run in parallel and interact, for example, through synchronisation or message passing. On the other hand, checking properties on process algebraic descriptions is often hard, while “unfolding” them into the Labelled Transition Systems can lead to the infamous state space explosion problem.In this work we use a subtype of Data Flow Analysis on systems defined by finite-state process algebras with CSP-type synchronisation – in particular, on our variant of IMC with a more permissive syntax, i.e. with a possibility to start a bounded number of new processes. We prove that the defined Pathway Analysis captures all the properties of the systems, i.e. is precise. The results of the Pathway Analysis can be therefore used as an intermediate representation format, which is more concise than the Labelled Transition System with all the states explicitly represented and more suitable for devising efficient verification algorithms of concurrent systems than their process algebraic descriptions – see, for example, the reachability algorithm in Skrypnyuk and Nielson (2011) [17].
    Original languageEnglish
    JournalJournal of Logic and Algebraic Programming
    Volume81
    Issue number4
    Pages (from-to)522-540
    ISSN2352-2208
    DOIs
    Publication statusPublished - 2012

    Keywords

    • Process algebras
    • Data Flow Analysis
    • Pathway Analysis
    • IMC

    Cite this