DocumentCode
1740278
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
fYear
2000
fDate
2000
Firstpage
245
Lastpage
254
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Computing Systems and Applications, 2000. Proceedings. Seventh International Conference on
Conference_Location
Cheju Island
ISSN
1530-1427
Print_ISBN
0-7695-0930-4
Type
conf
DOI
10.1109/RTCSA.2000.896398
Filename
896398
Link To Document