Modelling and Analysis Mobile Systems Using �pi-calculus (EFCP)

Khomenko, Victor and Germanos, Vasileios (2015) Modelling and Analysis Mobile Systems Using �pi-calculus (EFCP). Transactions on Petri Nets and Other Models of Concurrency X, 9410. pp. 153-175. ISSN 0302-9743

[img]
Preview
Text
paper.pdf

Download (802kB) | Preview
Official URL: http://link.springer.com/chapter/10.1007%2F978-3-6...

Abstract

Reference passing systems, like mobile and recon�gurable systems are common nowadays. The common feature of such systems is the possibility to form dynamic logical connections between the individual modules. However, such systems are very di�cult to verify, as their logical structure is dynamic. Traditionally, decidable fragments of pi-calculus, e.g. the well-known Finite Control Processes (FCP), are used for formal modelling of reference passing systems. Unfortunately, FCPs allow only `global' concurrency between processes, and thus cannot naturally express scenarios involving `local' concurrency inside a process, such as multicast. In this paper we propose Extended Finite Control Processes (EFCP), which are more convenient for practical modelling. Moreover, an almost linear translation of EFCPs to FCPs is developed, which enables e�cient model checking of EFCPs.

Item Type: Article
Keywords: The final publication is available at http://link.springer.com/chapter/10.1007%2F978-3-662-48650-4_8
Faculty / Department: Faculty of Science > Mathematics and Computer Science
Depositing User: Vasileios Germanos
Date Deposited: 02 Jun 2016 08:38
Last Modified: 02 Jun 2016 08:38
URI: http://hira.hope.ac.uk/id/eprint/1314

Actions (login required)

View Item View Item