A formal method for analyzing software architecture models in SAM

Author

Yu, Huiqun ; He, Xudong ; Deng, Yi ; Mo, Lian

Author_Institution

Sch. of Comput. Sci., Florida Int. Univ., Miami, FL, USA

fYear

2002

fDate

2002

Firstpage

645

Lastpage

652

Abstract

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.

Keywords

Petri nets; electronic commerce; formal verification; inference mechanisms; software architecture; temporal logic; Petri net; deductive reasoning; electronic commerce; formal method; formal verification; model checking; software architecture model; temporal logic; Computer science; Connectors; Costs; Electronic commerce; Helium; Logic; NASA; Petri nets; Software architecture; Space technology;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 2002. COMPSAC 2002. Proceedings. 26th Annual International

ISSN

0730-3157

Print_ISBN

0-7695-1727-7

Type

conf

DOI

10.1109/CMPSAC.2002.1045076

Filename

1045076