Verifying Real-time Systems using Untimed Model Checking Tools

In this paper we study a way to verify real-time systems using untimed model checking tools through an industrial case study with standard SPIN. We introduce a class of DC whose formulas correspond to regular expressions over the set of special symbols, each of which is a state occurrence for one time unit or for less than one time unit. The length of a string reects a time constraints. These regular expressions can easily be translated into untimed automata or a SPIN model. Then, we can verify real-time systems in the same way as for untimed system with standard SPIN. The case study used in this paper is the well-known Bi-phase Mark Protocol. Kim Yong Chun is a resercher from the Institute of Mathematics, Academy of Sciences, DPR of Korea. He stays with UNU/IIST from February 2001 to October 2001 and from September 2003 to June 2004 as a fellow. His current research interests include Natural Language Processing, Expert System, Formal Methods and Real-Time Systems. E-mail: kyc@iist.unu.edu