Specification and verification of reactive system behaviour: The railroad crossing example

被引：21

作者：

Armstrong, J ^{[1
]}

Barroca, L ^{[1
]}

机构：

[1] OPEN UNIV, DEPT COMP, MILTON KEYNES MK7 6AA, BUCKS, ENGLAND

来源：

REAL-TIME SYSTEMS | 1996年 / 10卷 / 02期

关键词：

temporal behaviour specification; reactive systems; rigorous proof; automated proof; safety properties; utility properties; Timed Statecharts; Real Time Logic; Proofpower HOL;

D O I：

10.1007/BF00360339

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper we present an approach to the specification and verification of reactive systems. The approach uses Timed Statecharts and Real Time Logic for the specification of temporal behaviour, and theorem proving techniques for the verification of safety and utility properties. Formal verification is achieved through the automation of semi-formal (rigorous) proofs using a theorem prover (Proofpower HOL). To illustrate the approach, we use the Railroad Crossing Problem, which has been proposed, along with a set of criteria for assessment, as a benchmark for the comparison of real-time formalisms. We conclude with our assessment of the approach against the proposed criteria.

引用

页码：143 / 178

页数：36

共 13 条

[1] BARROCA L, 1993, 13 P C SOC BRAS COMP
[2] BARROCA L, 1992, DCSCTR927 U YORK NEW
[3] CLEMENTS P, 1992, 6935 NAV RES LAB RPT
[4] FITZGERALD JS, 1993, DCSCTR933 U YORK NEW
[5] HEITMEYER CL, 1993, P 10 IEEE WORKSH REA
[6] SAFETY ANALYSIS OF TIMING PROPERTIES IN REAL-TIME SYSTEMS
JAHANIAN, F
MOK, AK
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1986, 12 (09) : 890 - 904
[7] JAHANIAN F, 1988, 9TH P REAL TIM SYST, P12
[8] JAHANIAN F, 1988, TR8825 U TEX AUST DE
[9] JAHANIAN F, 1988, 21ST P HAW INT C SYS, P479
[10] KESTEN Y, 1991, LECT NOTES COMPUT SC, V571, P591

← 1 2 →