Login | Register

Real-time reactive system development : a formal approach based on UML and PVS


Real-time reactive system development : a formal approach based on UML and PVS

Muthiayen, Darmalingum (2000) Real-time reactive system development : a formal approach based on UML and PVS. PhD thesis, Concordia University.

Text (application/pdf)


The notion of real-time reactive behavior encompasses concurrency, communication through sensors and actuators, and relations between input and output over time. Real-time reactive systems are inherently complex, and often used in safety-critical contexts. Application domains include control systems for nuclear reactors, air traffic, railroad crossing, telecommunications, and medical devices. Applying formal methods in the development process is seen as a means for dealing with the complexity, and for quality assurance. One of the goals is to formally verify time-dependent safety properties in the design. The scope of this thesis encompasses three major components. We develop a visual technique for object-oriented modeling of real-time reactive systems, based on a minimal set of extensions to UML, along with a set of well-formedness rules for the real-time models. We then present a formalization of the Real-Time rules of UML metamodel, and provide formal denotational and operational semantics for RTUML. Finally, we introduce a methodology for mechanized verification of time-dependent properties in the RTUML design of real-time reactive systems, within the PVS verification environment. The formal semantics of RTUML provides a foundation for the verification methodology, and for rigorous analysis and validation techniques. The novelty of the development methodology for real-time systems lies in the mechanized verification approach superimposed on the object-oriented modeling technique.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (PhD)
Authors:Muthiayen, Darmalingum
Pagination:xiv, 300 leaves ; 29 cm.
Institution:Concordia University
Degree Name:Ph. D.
Program:Computer Science and Software Engineering
Thesis Supervisor(s):Alagar, V. S.
ID Code:958
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:15
Last Modified:18 Jan 2018 17:15
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Back to top Back to top