Login | Register

Animation and formal verification of real-time reactive systems in an object-oriented environment

Title:

Animation and formal verification of real-time reactive systems in an object-oriented environment

Muthiayen, Darmalingum (1996) Animation and formal verification of real-time reactive systems in an object-oriented environment. Masters thesis, Concordia University.

[thumbnail of MQ26017.pdf]
Preview
Text (application/pdf)
MQ26017.pdf
5MB

Abstract

Real-time reactive systems are characterized by their continuous interaction with their environment through stimulus-response behavior. The safety-critical nature of their domain and their inherent complexity advocate the use of formal methods in the software development process. TROMLAB development environment supports a process model adequate for dealing with the complexity of reactive systems. The foundation of the TROMLAB environment is the Timed Reactive Object Model (TROM), which combines object-oriented and real-time technologies. Simulation is essential in the behavioral analysis of real-time reactive systems; animation allows a visualization of the simulation process. A rigorous trace analysis of simulation scenarios provides insight into the behavior of the collaborating entities in the configuration. This supports validation of systems designed incrementally and iteratively in the software development life-cycle. Moreover, safety-critical systems need to be verified for adherence to stringent safety and liveness properties. The scope of this thesis is two-fold. We first present an animation tool supporting simulation of reactive systems described in the TROM formalism. We include formal specifications of the functionalities of the simulator in VDM specification language. We then introduce a methodology for formal verification of TROM subsystems. The novelty of the methodology lies in the formal verification approach embedded within an object-oriented framework. The simulator and the verification methodology conform respectively to the operational and logical semantics of TROMs.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (Masters)
Authors:Muthiayen, Darmalingum
Pagination:xi, 147 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M. Comp. Sc.
Program:Computer Science and Software Engineering
Date:1996
Thesis Supervisor(s):Alagar, V. S.
Identification Number:QA 76.54 M88 1996
ID Code:198
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:10
Last Modified:13 Jul 2020 19:46
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

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top