Automatic Effective Verification Method for Distributed and Concurrent Systems Using Timed Language Inclusion

Abstract

In distributed and concurrent systems, the notions of fairness and time are important as follows:(1) Fairness is a mathematical abstraction in distributed and concurrent systems. Fairness abstracts the details of fair schedulers and the speeds of independent processors. (2) The distributed and concurrent systems have to meet certain hard real-time constraints, and the correctness of them depends on the actual values of the delays.

In this paper, we propose the specification and verification method of fairness and time in distributed and concurrent systems as follows: (1) 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. (2) In order to effectively verify distributed and concurrent systems, we restrict timing constrains of timed automaton such that in cycles we must specify timing constrains about the clock variables after they are reset to zero.