Static Analysis of IMC

详细信息	查看全文 | 推荐本文 |

• 作者：Nataliya Skrypnyuk^a ; ^{nsk@imm.dtu.dk} ; Flemming Nielson^a ; ^{nielson@imm.dtu.dk} ; Henrik Pilegaard^b ; ^{henrik@pilegaard.org}
• 关键词：Process algebras ; Data Flow Analysis ; Pathway Analysis ; IMC
• 刊名：Journal of Logic and Algebraic Programming
• 出版年：2012
• 期刊代码：73_15678326
• 类别：cp
• 出版时间：May, 2012
• 卷：81
• 期：4
• 页码：522-540
• 文件大小：420 K

摘要

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 鈥渦nfolding鈥?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) .