Scalable compositional reachability analysis of real-time concurrent systems

Author

Wang, Farn

Author_Institution

Inst. of Inf. Sci., Acad. Sinica, Taipei, Taiwan

fYear

1996

fDate

10-12 Jun 1996

Firstpage

182

Lastpage

191

Abstract

A description model for high level behavior of a real time concurrent system is presented. A verification algorithm is then devised to take advantage of interaction locality and symmetry and internal operation concealment in the model. A system called VERIFAST implements the algorithm. Experiments show that VERIFAST runs fast and exhibits time complexity linear to the size of concurrency in a benchmark

Keywords

computational complexity; parallel programming; program diagnostics; program verification; reachability analysis; real-time systems; VERIFAST; description model; high level behavior; interaction locality; internal operation concealment; real time concurrent systems; scalable compositional reachability analysis; time complexity; verification algorithm; Automatic control; Communication system control; Concurrent computing; Control systems; Information science; Production facilities; Reachability analysis; Real time systems; Size control; Yarn;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time Technology and Applications Symposium, 1996. Proceedings., 1996 IEEE

Conference_Location

Brookline, MA

Print_ISBN

0-8186-7448-2

Type

conf

DOI

10.1109/RTTAS.1996.509535

Filename

509535

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2194480