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.