ePrints

Modelling and Analysis Mobile Systems Using π-calculus (EFCP)

Lookup NU author(s): Dr Victor Khomenko, Vasileios Germanos

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.

Abstract

Reference passing systems, like mobile and reconfigurable 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 difficult to verify, as their logical structure is dynamic. Traditionally, decidable fragments of π-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 efficient model checking of EFCPs.

Publication metadata

Author(s): Khomenko V, Germanos V

Publication type: Article

Publication status: Published

Journal: LNCS Transactions on Petri Nets and Other Models of Concurrency X (ToPNoC)

Year: 2015

Volume: 9410

Pages: 153-175

Online publication date: 24/11/2015

Acceptance date: 01/01/1900

ISSN (electronic): 0302-9743

Publisher: Springer Verlag

URL: http://dx.doi.org/10.1007/978-3-662-48650-4_8

DOI: 10.1007/978-3-662-48650-4_8

Altmetrics

Share