A formal method for analyzing software architecture models in SAM

The software architecture model (SAM) is a general software architecture model based on a dual formalism combining Petri nets and temporal logic. A SAM model contains a hierarchical set of compositions, each of which consists of a set of components, a set of connectors, and a set of constraints. Thi...

Full description

Saved in:
Bibliographic Details
Main Authors: Yu, Huiqun, He, Xudong, Deng, Yi, Mo, Lian
Format: Conference Proceeding
Language:English
Subjects:
Applied sciences
Computer science
Computer science
control theory
systems
Connectors
Costs
Electronic commerce
Exact sciences and technology
Helium
Logic
NASA
Petri nets
Software
Software architecture
Software engineering
Space technology
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The software architecture model (SAM) is a general software architecture model based on a dual formalism combining Petri nets and temporal logic. A SAM model contains a hierarchical set of compositions, each of which consists of a set of components, a set of connectors, and a set of constraints. This paper proposes a formal method for analyzing SAM models in both element (either component or connector) level and composition level. The basic idea is to simulate Petri net behaviors in terms of fair transition systems. The properties of individual components and connectors are verified either by deductive reasoning or model checking. The properties of the entire system is inferred from the properties of its constituents. A detailed case study of an electronic commerce system shows our approach to formally modeling, refining and analyzing software architecture models.
ISSN:0730-3157
DOI:10.1109/CMPSAC.2002.1045076