A formal method for analyzing software architecture models in SAM

被引：2

作者：

Yu, HQ ^{[1
]}

He, XD ^{[1
]}

Yi, D ^{[1
]}

Lian, M ^{[1
]}

机构：

[1] Florida Int Univ, Sch Comp Sci, Miami, FL 33199 USA

来源：

26TH ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, PROCEEDINGS | 2002年

关键词：

Software architecture; SAM; Petri net; temporal logic; verification;

D O I：

10.1109/CMPSAC.2002.1045076

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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 neither 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.

引用

页码：645 / 652

页数：4

共 14 条

[1]

[Anonymous], LECT NOTES COMPUTER

[2]

APT KR, 1991, VERIFICATION SEQUENT

[3] Deductive verification of real-time systems using STeP [J].

Bjorner, NS ;

Manna, Z ;

Sipma, HB ;

Uribe, TE .

THEORETICAL COMPUTER SCIENCE, 2001, 253 (01) :27-60

[4] Formal methods: State of the art and future directions [J].

Clarke, EM ;

Wing, JM .

ACM COMPUTING SURVEYS, 1996, 28 (04) :626-643

[5] SYSTEM MODELING WITH HIGH-LEVEL PETRI NETS [J].

GENRICH, HJ ;

LAUTENBACH, K .

THEORETICAL COMPUTER SCIENCE, 1981, 13 (01) :109-136

[6]

GOMMA H, 2000, DESIGN CONCURRENT DI

[7]

HE X, 2002, IN PRESS COMPUTER J

[8]

Manna Z., 1992, TEMPORAL LOGIC REACT, DOI DOI 10.1007/978-1-4612-0931-7

[9]

Manna Z, 1995, TEMPORAL VERIFICATIO

[10]

MANNA Z, 1994, STANCSTR941518 STANF

← 1 2 →