Title :
Towards a mechanical verification of real-time reactive systems modeled in UML
Author :
Alagar, V.S. ; Muthiayen, D.
Author_Institution :
Dept. of Comput. Sci., Concordia Univ., Montreal, Que., Canada
Abstract :
This paper provides a verification methodology for UML-based real-time reactive system models. The verification process can be mechanized in PVS (Prototype Verification System). The motivation for this work comes from the wide acceptance of UML in industry, as a unified notation applicable to the development of object-based systems in a broad spectrum of domains, and the use of PVS for design analysis in large-scale safety-critical applications
Keywords :
formal specification; object-oriented programming; program verification; real-time systems; specification languages; PVS; Prototype Verification System; UML; Unified Modeling Language; design analysis; mechanical verification; notation; object-based systems; real-time reactive systems; safety-critical applications; Aerospace electronics; Computer architecture; Computer science; Large-scale systems; Object oriented modeling; Process control; Prototypes; Real time systems; Time factors; Unified modeling language;
Conference_Titel :
Real-Time Computing Systems and Applications, 2000. Proceedings. Seventh International Conference on
Conference_Location :
Cheju Island
Print_ISBN :
0-7695-0930-4
DOI :
10.1109/RTCSA.2000.896398
