Title :
A verifier for distributed real-time systems with bounded integer variables
Author :
Wang, Farn ; Mok, Aloysius K.
Author_Institution :
Dept. of Comput. Sci., Texas Univ., Austin, TX, USA
Abstract :
The authors propose asynchronous register temporal logic (ARTL), which is suitable for the specification and verification of distributed real-time software systems. ARTL adopts a multiclock model that has no explicit reference to global time and, unlike other propositional temporal logics, has a built-in capability for reasoning about bounded integer variables, called registers, together with a freezing modal operator for fixing register contents. The implementation and experimentation of a verifier for ARTL based on the tableau method are described. The tableau method for ARTL is discussed. The verifier was tested against several benchmarks with good results. Since the satisfiability problem for ARTL is EXPSPACE-hard, several strategies for improving the efficiency of the tableau method have been implemented and are considered
Keywords :
distributed processing; formal specification; parallel programming; program verification; real-time systems; temporal logic; ARTL; EXPSPACE-hard; asynchronous register temporal logic; bounded integer variables; distributed real-time software systems; distributed real-time systems; freezing modal operator; multiclock model; propositional temporal logics; satisfiability problem; tableau method; verifier; Application software; Arithmetic; Binary decision diagrams; Clocks; Digital circuits; Logic circuits; Real time systems; Registers; Software systems; Timing;
Conference_Titel :
Computer Assurance, 1993. COMPASS '93, Practical Paths to Assurance. Proceedings of the Eighth Annual Conference on
Conference_Location :
Gaithersburg, MD
Print_ISBN :
0-7803-1251-1
DOI :
10.1109/CMPASS.1993.288850
