Static Analysis of IMC

Publication: Research - peer-reviewJournal article – Annual report year: 2012

View graph of relations

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
Issue number4
Pages (from-to)522-540
StatePublished - 2012
CitationsWeb of Science® Times Cited: 1


  • Process algebras, Data Flow Analysis, Pathway Analysis, IMC
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

ID: 7873602