A structural transformation from p-pi to MSVL

作者：Luo, Ling; Duan, Zhenhua^*; Tian, Cong; Wang, Xiaobing

来源：Journal of Combinatorial Optimization, 2015, 29(1): 308-329.

DOI：10.1007/s10878-014-9779-0

• Process algebra
• Temporal logic
• pi-calculus
• MSVL
• Verification

This paper presents a structural transformation approach from p-p processes to MSVL programs. To this end, channel and communication primitives are firstly defined in MSVL. Further, based on these definitions, a mapping function F which transforms bounded p-p processes into MSVL programs is formalized. Moreover, the soundness of the transformation is proved. By the transformation, p-p can provide a mechanism to model, simulate and verify concurrent time-dependent systems by means of the techniques of MSVL. Finally, a case study is given to illustrate how the transformation can be used in practice.

• 出版日期2015-1
• 单位西安电子科技大学