Login | Register

Automatic verification of behavioral specifications in software intensive systems


Automatic verification of behavioral specifications in software intensive systems

Soeanu Caval, Andrei (2007) Automatic verification of behavioral specifications in software intensive systems. Masters thesis, Concordia University.

[thumbnail of MR34650.pdf]
Text (application/pdf)
MR34650.pdf - Accepted Version


Modern systems tend to exhibit an ever increasing complexity especially due to their software design components and programmable aspects which are nowadays ubiquitous. Consequently, in order to assure reliable and dependable systems, sustained efforts are required in the process of system verification and validation. However, conventional verification and validation techniques that are primarily based on testing and simulation, while being helpful and useful, may lack in many cases the desired level of rigor and completeness and are generally costly, laborious and time consuming. In contrast, using verification techniques that are based on formal foundations, such as model-checking and program analysis in a complementary manner to the traditional verification techniques can provide an increased level of reliability and dependability. In this context, applying such techniques for verifying the correctness and validity of the engineered systems early in the design phase can greatly improve the quality and performance of the design. Moreover, using such a verification methodology can alleviate the high cost of maintaining the systems later in their development phases. Presently, modern system design can benefit from a wide range of development paradigms including those that are using techniques traditionally employed in software engineering such as the object oriented design paradigm. In order to standardize the process of system design and development, several modeling languages emerged in order to provide the means for capturing and modeling various system specifications and requirements. The Unified Modeling Language (UML) 2.0 and more recently the Systems Modeling Languages (SysML) represent the most prominent standardized modeling languages for software and systems engineering. In this setting, the research initiative that this work addresses, is introducing a unified paradigm for the verification and validation of software intensive systems engineering design models by using formal verification techniques that can be applied in order to assess different behavioral diagrams belonging to the aforementioned modeling languages.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Soeanu Caval, Andrei
Pagination:ix, 104 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Debbabi, M
Identification Number:LE 3 C66E44M 2007 S64
ID Code:975383
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 16:07
Last Modified:13 Jul 2020 20:07
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