Title :
Scalable compositional reachability analysis of real-time concurrent systems
Author_Institution :
Inst. of Inf. Sci., Acad. Sinica, Taipei, Taiwan
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;
Conference_Titel :
Real-Time Technology and Applications Symposium, 1996. Proceedings., 1996 IEEE
Conference_Location :
Brookline, MA
Print_ISBN :
0-8186-7448-2
DOI :
10.1109/RTTAS.1996.509535
