Login | Register

Transforming architectural descriptions of component-based systems for formal analysis

Title:

Transforming architectural descriptions of component-based systems for formal analysis

Ibrahim, Naseem Ismail (2008) Transforming architectural descriptions of component-based systems for formal analysis. Masters thesis, Concordia University.

[img]
Preview
Text (application/pdf)
MR63331.pdf - Accepted Version
5MB

Abstract

Design time analysis is an important step in the process of developing software systems, with the goal of ensuring that the system design conforms to the design constraints that are stated as part of the functional and non-functional requirements. The well-known techniques for formally analyzing a design are model checking, axiom-based formal verification, and real-time schedulability analysis that takes into account resource constraints. In this thesis, model checking and real-time schedulability are the techniques used to verify that the system under development is both safe and secure. The architecture of a trustworthy system, formally described in Trustworthy Architectural Description Language (TADL), is taken as the input for the analysis stage. Instead of developing new tools to perform the analyses, the thesis has developed transformation techniques to transform TADL descriptions into behaviour protocols used by existing verification tools. The transformation rules are described independently of the transformation process, thus allowing both reuse and easy extendability. A tool based on such techniques has been designed and implemented which automatically generates two types of models from a TADL description. One is the UPPAAL model, on which the security and safety properties of the system under design are formally verified. The second output is the TIMES model, on which real-time schedulability analysis is performed. The techniques and tools are applied to The Common Component Modelling Example (CoCoME), a case study defined by the component development community, to demonstrate that TADL is expressive enough to formally describe component-based systems.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (Masters)
Authors:Ibrahim, Naseem Ismail
Pagination:xii, 174 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M. Comp. Sc.
Program:Computer Science and Software Engineering
Date:2008
Thesis Supervisor(s):Alagar, Vangalur
ID Code:976324
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 16:23
Last Modified:18 Jan 2018 17:42
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