Muthiayen, Darmalingum (2000) Real-time reactive system development : a formal approach based on UML and PVS. PhD thesis, Concordia University.
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 > Faculty of Engineering and Computer Science > Computer Science and Software Engineering|
|Item Type:||Thesis (PhD)|
|Pagination:||xiv, 300 leaves ; 29 cm.|
|Degree Name:||Theses (Ph.D.)|
|Program:||Computer Science and Software Engineering|
|Thesis Supervisor(s):||Alagar, V. S.|
|Deposited By:||Concordia University Libraries|
|Deposited On:||27 Aug 2009 17:15|
|Last Modified:||08 Dec 2010 15:17|
Repository Staff Only: item control page