Formal verification and testing of protocols

被引：5

作者：

Avresky, DR ^{[1
]}

机构：

[1] Boston Univ, Dept Elect Engn, Brookline, MA 02146 USA

来源：

COMPUTER COMMUNICATIONS | 1999年 / 22卷 / 07期

关键词：

protocols; reachability analysis; execution tree; formal verification;

D O I：

10.1016/S0140-3664(99)00011-0

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We adopt a formalism to describe protocols that is close to the human way of thinking and can be easily used to perform reachability analysis of the described protocol in a state-transition format. This formalism allows for an execution tree (ET) to be generated from a set of assertions such that all paths from the root to the leaves are well-defined formulas. We then extend the formalism with regards to real-time properties. Finally, we present a software verification tool, that implements the aforementioned features in the analysis of protocols. (C) 1999 Elsevier Science B.V. All rights reserved.

引用

页码：681 / 690

页数：10

共 13 条

[1] Fault injection for formal testing of fault tolerance [J].

Avresky, D ;

Arlat, J ;

Laprie, JC ;

Crouzet, Y .

IEEE TRANSACTIONS ON RELIABILITY, 1996, 45 (03) :443-455

[2]

AVRESKY DR, 1994, INT J RELIABILITY QU, V1, P197

[3]

AVRESKY DR, 1992, P 22 INT S FAULT TOL, P345

[4] AN INTERACTIVE TOOL FOR DESIGN, SIMULATION, VERIFICATION, AND SYNTHESIS OF PROTOCOLS [J].

CHAO, DY ;

WANG, DT .

SOFTWARE-PRACTICE & EXPERIENCE, 1994, 24 (08) :747-783

[5]

Clarke E. M., 1992, CMUCS92206

[6]

Clarke E. M., 1981, LECTURE NOTES COMPUT, V131, P52, DOI DOI 10.1007/BFB0025774

[7] SOMETIMES AND NOT NEVER REVISITED - ON BRANCHING VERSUS LINEAR TIME TEMPORAL LOGIC [J].

EMERSON, EA ;

HALPERN, JY .

JOURNAL OF THE ACM, 1986, 33 (01) :151-178

[8] COMPILING REAL-TIME PROGRAMS WITH TIMING CONSTRAINT REFINEMENT AND STRUCTURAL CODE MOTION [J].

GERBER, R ;

HONG, SS .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1995, 21 (05) :389-404

[9]

MCMILLAN KL, 1991, P 1991 INT S SHAR ME

[10] HIERARCHICAL REACHABILITY GRAPH OF BOUNDED PETRI NETS FOR CONCURRENT-SOFTWARE ANALYSIS [J].

NOTOMI, M ;

MURATA, T .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1994, 20 (05) :325-336

← 1 2 →