Breadcrumb

 
 

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.

[img]
Preview
PDF
4Mb

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 > Faculty 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:Theses (M.Comp.Sc.)
Program:Computer Science and Software Engineering
Date:1996
Thesis Supervisor(s):Alagar, V. S.
ID Code:198
Deposited By:Concordia University Libraries
Deposited On:27 Aug 2009 13:10
Last Modified:08 Dec 2010 10:13
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

Document Downloads

More statistics for this item...

Concordia University - Footer