Timeout Order Abstraction for Time-Parametric Verification of Loosely Synchronized Real-Time Distributed Systems

Abstract

We present timeout order abstraction (TO-abstraction), a technique to systematically abstract a given loosely synchronized real-time distributed system (LSRTDS) into an untimed model. We define the subclass of LSRTDS’s that we can apply TO-abstraction using a syntax template that represents a restriction to Tempo, the primary modeling language of TIOA [7]. The untimed model obtained from the abstraction is a classical finite state machine, and thus one can automatically verify temporal properties of the model using a conventional model-checker. We prove the soundness of the abstraction using simulation relation. From this result, we guarantee that any untimed safety property of the untimed model also holds for the original TIOA model. We have applied TO-abstraction to a resource-sharing protocol and the DHCP Failover protocol. We verified untimed abstractions of them by bounded model-checking up to depth 20. We have also experimented with effectiveness of bug-finding using our technique by mutating particular parts of the original code. From this experiment, we found a complex bad execution that would have been very difficult to find by human or simulations.