Deductive verification of real-time systems using STeP

被引：16
作者：
Bjorner, NS [1 ]
Manna, Z [1 ]
Sipma, HB [1 ]
Uribe, TE [1 ]
机构：
[1] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA
来源：
THEORETICAL COMPUTER SCIENCE | 2001年 / 253卷 / 01期
基金：
美国国家航空航天局; 美国国家科学基金会;
关键词：
real-time systems; temporal verification; modularity; receptiveness;
D O I：
10.1016/S0304-3975(00)00088-8
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logic. We show how deductive verification rules, verification diagrams, and automatic invariant generation can be used to establish properties of real-time systems in this framework. We also discuss global and modular proofs of the branching-time property of non-Zenoness. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP. (C) 2001 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：27 / 60
页数：34
相关论文
共 52 条
[1]  
ABADI M, 1992, LECT NOTES COMPUT SC, V600, P1, DOI 10.1007/BFb0031985
[2]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[3]  
Alur R, 1997, LECT NOTES COMPUT SC, V1243, P74
[4]  
ALUR R, 1996, LECT NOTES COMPUTER, V1066
[5]  
ALUR R, 1996, LECT NOTES COMPUTER, V1102
[6]  
[Anonymous], LNCS
[7]   Specification and verification of reactive system behaviour: The railroad crossing example [J].
Armstrong, J ;
Barroca, L .
REAL-TIME SYSTEMS, 1996, 10 (02) :143-178
[8]  
BENGTSSON J, 1996, LNCS, V1066, P232
[9]  
BENSALEM S, 1996, LECT NOTES COMPUTER, V1102, P323
[10]  
BJOORNER NS, 1998, THESIS STANFORD U
123456