文档介绍：Automatic V eri cation of Real{m unicating Systems b y
Constrain t{Solving
W ang Yi, P aul P ettersson and Mats Daniels
Departmen t puter Systems, Uppsala Univ ersit y ,Bo x 325, S751 05, Uppsala,
Sw eden. Email: f yi,paup et,matsd g ***@do
In this pap er, an algebra of timed pro cesses with real{v alued clo c ks is presen ted, whic h
serv es as a formal description language for real{m unicating systems. W e sho w
that requiremen ts suc h as \a pro cess will nev er reac h an undesired state" can b e v eri ed
b y solving a simple class of constrain t systems on the clo c k{v ariables. plete metho d
for reac habilit y analysis asso ciated with the language is dev elop ed, and impleme n ted as an
automatic v eri cation to ol based on constrain t{solving tec hniques. Finally as examples,
w e study and v erify the safet y{prop erties of Fisc her's m utual exclusion proto col and a
railw a y crossing con troller.
1. INTR ODUCTION
Correct timing pla ys an imp ortan t role in ensuring the correct op eration of real{time
systems. Since suc h systems are often em b edded in safet y{critical en vironmen ts, it is
imp ortan t to formally v erify that certain crucial requiremen ts are alw a ys met b y the
systems. This creates a need for formalisms to describ e the abstract b eha vior of timed
systems . mo deling and to c hec k logical prop erties of the abstract descriptions .
v eri cation . During the past few y ears, researc hers ha v e dev elop ed v arious formal tec h-
niques for mo deling and v erifying real{time systems, . automaton based, [1{3, 14]
and pro cess algebra based [24, 7, 9, 15, 22, 17, 13, 20, 29]. One of the most essful
approac hes is time d automata due to Alur and Dill [3], whic h are the classical nite-state
automata extended with v ariables mo deling system clo c ks.
In this pap er, w e study real-m unicating systems. Suc h a system ma y consist
ofan um b er p onen ts with their o wn or shared clo c ks.