Logotype Mälardalenn University

MRTC publications



Automatic Verification of Real-Time Communicating Systems by Constraint Solving

Full text:  
Authors: Wang Yi (external), Paul Pettersson, Mats Daniels (Uppsala University)
Source: the 7th International Conference on Formal Description Techniques, p 223-238, Berne, Switzerland
 

Abstract

In this paper, an algebra of timed processes with real{valued clocks is presented, which serves as a formal description language for real{time communicating systems. We show that requirements such as \a process will never reach an undesired state" can be veri ed by solving a simple class of constraint systems on the clock{variables. A complete method for reachability analysis associated with the language is developed, and implemented as an automatic veri cation tool based on constraint{solving techniques. Finally as examples, we study and verify the safety{properties of Fischer's mutual exclusion protocol and a railway crossing controller.
 

BibTeX entry

@inproceedings{Yi_2867:1994,
   author = {Wang Yi and Paul Pettersson and Mats Daniels},
   title = {Automatic Verification of Real-Time Communicating Systems by Constraint Solving},
   booktitle = {the 7th International Conference on Formal Description Techniques},
   month = {October},
   year = {1994},
   pages = {223-238},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=2867},
}

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2012.08.24