Formal specification and verification method of concurrent and distributed systems by restricted timed automata

In this paper, we propose the specification and verification method of distributed systems. We can easily specify fairness and timing constraints, and can effectively verify distributed systems by our proposed method. In order to specify fairness, an enable condition and a performed condition are attached to a finite set of states in our proposed specification method. In order to effectively verify distributed systems, we restrict timing constraints of timed automaton such that in cycles we must specify timing constraints about the clock variables after they are reset to zero.We have developed the verification systems based on our proposed method, and have shown it effective by timed Alternating Bit Protocol.