A FORMAL FRAMEWORK FOR ASTRAL INTRALEVEL PROOF OBLIGATIONS

被引：8

作者：

COENPORISINI, A ^{[1
]}

KEMMERER, RA ^{[1
]}

MANDRIOLI, D ^{[1
]}

机构：

[1] UNIV CALIF SANTA BARBARA,DEPT COMP SCI,SOFTWARE GRP,SANTA BARBARA,CA 93106

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1994年 / 20卷 / 08期

基金：

美国国家科学基金会;

关键词：

FORMAL METHODS; FORMAL SPECIFICATION AND VERIFICATION; REAL-TIME SYSTEMS; TIMING REQUIREMENTS; STATE MACHINES; ASLAN; TRIO;

D O I：

10.1109/32.310665

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL specifications. ASTRAL is provided with structuring mechanisms that allow one to build modularized specifications of complex systems with layering. In this paper, further details of the ASTRAL environment components and the critical requirements components, which were not fully developed in previous papers, are presented. Formal proofs in ASTRAL can be divided into two categories: interlevel proofs and intralevel proofs. The former deal with proving that the specification of level i + 1 is consistent with the specification of level i, and the latter deal with proving that the specification of level i is consistent and satisfies the stated critical requirements. This paper concentrates on intralevel proofs.

引用

页码：548 / 561

页数：14

共 13 条

[1]

ALUR A, 1990, 5TH IEEE LICS 90, P414

[2]

Chang C. K., 1990, InfoJapan '90: Information Technology Harmonizing with Society, P307

[3]

COENPORISINI A, 1993, TRCS9304 U CAL DEP C

[4]

COENPORISINI A, 1992, TRCS9222 U CAL DEP C

[5] PROVING PROPERTIES OF REAL-TIME SYSTEMS THROUGH LOGICAL SPECIFICATIONS AND PETRI-NET MODELS [J].

FELDER, M ;

MANDRIOLI, D ;

MORZENTI, A .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1994, 20 (02) :127-141

[6]

GABRIELIAN A, 1991, COMMUN ACM, V34, P51

[7] A LAYERED APPROACH TO AUTOMATING THE VERIFICATION OF REAL-TIME SYSTEMS [J].

GERBER, R ;

LEE, I .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1992, 18 (09) :768-784

[8]

Ghezzi C, 1991, P TAV, P112

[9]

GHEZZI C, 1991, 3RD P EUR SOFTW ENG, P122

[10]

OSTROFF JS, 1989, TEMPORAL LOGIC REAL, V1

← 1 2 →