TiMo@PAT: A Model Checker for TiMo Systems

  • Download

    • Download TiMo@PAT here.
    • Click here for an online manual of TiMo@PAT.
    • Download technical report for TiMo@PAT here.

  • Introduction

    • TiMo is a calculus for mobile systems in which it is possible to use timers for controlling process mobility and interaction. Despite the fact it is simple, TiMo is able to describe complex systems. Several properties of these systems could be verified by using Process Analysis Toolkit (PAT), a software platform implementing various model-checking techniques for various properties such as deadlock-freeness, divergence-freeness and reachability. We implement a TiMo module in PAT, called TiMo@PAT, and verify automatically several properties of the distributed systems with migrating and communicating processes described in TiMo. The properties TiMo@PAT supports including process migration, bounded liveness and optimal reachability, etc.

  • Case Study - Travel Shop System

    • Download TiMo model here.

    In this system, clients buy tickets from some travel agents, attempting either to pay as little as possible or as fast as possible to get a ticket to a predefined destination. The scenario involves five locations and six processes. The role of each of the processes is as follows:
    1. client is a process that initially resides in the home location, has initially an amount of 130 cash, and intends to pay for a flight after comparing two offers (standard and special) provided by the travel shop. After entering the travelshop location, the client receives the location of the standard offer and. He moves to the standard location and obtains the standard offer, and also the location where a special offer can be obtained. Then it moves to the special location to receive the special offer. Finally, the client moves to the bank and pays for the cheaper offer, and returns to the home location.
    2. agent is a process that initially resides in the travelshop location, has initially an amount of 100 cash, and informs the client where to look for the standard offer. It then moves to the bank in order to collect the money from the till. After that agent returns to the travelshop.
    3. flightinfo communicates the standard offer (110 cash) to clients as well as the location (special) of the special offer.
    4. saleinfo communicates the special offer (90 cash) to clients together with the location (bank) of the bank. It can also accept an update of the special offer coming from the travelshop location.
    5. update migrates from the travelshop to special location in order to update the special offer to the amount of 60 cash.
    6. till resides at the bank location, has an initial amount of 10 cash, and can either receive e-money paid in by the clients, or transfer the accumulated e-money to the agent.

    This page is maintained by Dr. Gabriel Ciobanu and Manchun Zheng.