Title :
Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states
Author_Institution :
Inst. of Inf. Sci., Acad. Sinica, Taipei, Taiwan
Abstract :
A compositional CTL mode-checking algorithm for real-time concurrent systems with a discrete global clock is presented based on a new high-level description model. We implement the algorithm in a system called VERIFAST-2 which has passed the extended General Session Setup Control protocols with concurrency from 5 to 51 threads all in one minute and demonstrated truly scalable performance with respect to the size of concurrency. In this respect, it outperforms HyTech version 1.02 b and VERIFAST-1. Then we discuss how to incorporate R.J. Parikh´s classic work on semilinear expressions to verify software recursions
Keywords :
formal specification; formal verification; performance evaluation; protocols; real-time systems; VERIFAST-2; compositional CTL mode-checking algorithm; discrete global clock; high-level real-time concurrent systems; protocols; scalable compositional verification; software recursions; truly scalable performance; Clocks; Concurrent computing; Control systems; Guidelines; Information science; Protocols; Real time systems; Reliability engineering; Size control; Yarn;
Conference_Titel :
Real-Time Computing Systems and Applications, 1996. Proceedings., Third International Workshop on
Conference_Location :
Seoul
Print_ISBN :
0-8186-7626-4
DOI :
10.1109/RTCSA.1996.554967
