Automatic Analysis of TiMo Systems in PAT
Gabriel Ciobanu, Manchun Zheng · 2013
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 analyzing some properties of a distributed system.