Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/35534
Title: Formalizing and verifying software architectures
Authors: ZHANG JIEXIN
Keywords: Software Architecture, Model Checking, Formal Verification, Software Architecture Description Language, Architecture Style, PAT
Issue Date: 17-Aug-2012
Source: ZHANG JIEXIN (2012-08-17). Formalizing and verifying software architectures. ScholarBank@NUS Repository.
Abstract: Software Architecture plays an essential role in the high level description of a system design. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this paper, we present two automated approaches to the modeling and verification of software architecture designs using the Process Analysis Toolkit (PAT). We present the formal syntax of the Monterey Phoenix (MP) and Wright# architecture description languages together with their operational semantics in Labeled Transition System (LTS). Both of the languages are supported by separate module implemented in the PAT verification framework based on the proposed formalism. The modules support verification and simulation of software architecture models. We further improve our work via defining an architecture style library that embodies commonly used architecture patterns to facilitate the modeling process. Finally, different case studies are presented to evaluate the effectiveness and scalability of our approaches.
URI: http://scholarbank.nus.edu.sg/handle/10635/35534
Appears in Collections:Master's Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
ZhangJX.pdf955.31 kBAdobe PDF

OPEN

NoneView/Download

Page view(s)

207
checked on Dec 11, 2017

Download(s)

247
checked on Dec 11, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.