Automatic Analysis of TiMo Systems in PAT

被引：5

作者：

Ciobanu, Gabriel ^{[1
]}

Zheng, Manchun ^{[2
]}

机构：

[1] Romanian Acad, Inst Comp Sci, Bucharest, Romania

[2] Univ Singapore Technol & Design, Singapore, Singapore

来源：

2013 18TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS) | 2013年

关键词：

TiMo; Timed Mobility; PAT; Model Checking;

D O I：

10.1109/ICECCS.2013.25

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

TiMo is a process calculus for mobile systems where timers could be to used to control process mobility and interaction. Despite its syntactic simplicity, TiMo is able to describe complex systems. Interesting properties of such systems refers to process migration, time constraints, bounded liveness and optimal reachability. In this work we describe a tool, called TiMo@ PAT, developed by using Process Analysis Toolkit (PAT), an extensible platform for model checkers. We illustrate the capability of TiMo@ PAT by analysing some properties of a distributed system.

引用

页码：121 / 124

页数：4

共 6 条

[1]

Ciobanu Gabriel, 2011, FM 2011: Formal Methods. Proceedings 17th International Symposium on Formal Methods, P293, DOI 10.1007/978-3-642-21437-0_23

[2]

CIOBANU G, 2008, FASE, V4961, P215

[3] Flexible software architecture and language for mobile agents [J].

Ciobanu, Gabriel ;

Juravle, Calin .

CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2012, 24 (06) :559-571

[4] Timed Mobility in process algebra and Petri nets [J].

Ciobanu, Gabriel ;

Koutny, Maciej .

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2011, 80 (07) :377-391

[5] PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers [J].

Liu, Yang ;

Sun, Jun ;

Dong, Jin Song .

22ND IEEE INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING (ISSRE), 2011, :190-199

[6]

Sun J, 2009, LECT NOTES COMPUT SC, V5643, P709, DOI 10.1007/978-3-642-02658-4_59

← 1 →