Deductive verification of real-time systems using STeP

被引：0
|
作者：
Bjorner, NS [1 ]
Manna, Z [1 ]
Sipma, HB [1 ]
Uribe, TE [1 ]
机构：
[1] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA
来源：
TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT | 1997年 / 1231卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP.
引用
收藏
页码：22 / 43
页数：22
相关论文
共 50 条
  • [1] Deductive verification of real-time systems using STeP
    Bjorner, NS
    Manna, Z
    Sipma, HB
    Uribe, TE
    [J]. THEORETICAL COMPUTER SCIENCE, 2001, 253 (01) : 27 - 60
  • [2] Deductive verification of probabilistic real-time systems
    Yamane, S
    [J]. 24TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS WORKSHOPS, PROCEEDINGS, 2004, : 622 - 627
  • [3] Deductive verification of hybrid systems using STeP
    Manna, Z
    Sipma, HB
    [J]. HYBRID SYSTEMS: COMPUTATION AND CONTROL, 1998, 1386 : 305 - 318
  • [4] Deductive probabilistic verification methods of safety, liveness and nonzenoness for distributed real-time systems
    Yamane, S
    [J]. EMBEDDED SOFTWARE AND SYSTEMS, PROCEEDINGS, 2005, 3820 : 332 - 345
  • [5] Deductive schedulability verification methodology of real-time software using both refinement verification and hybrid automata
    Yamane, S
    [J]. 27TH ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, PROCEEDINGS, 2003, : 527 - 533
  • [6] The verification technique of real-time systems using probabilities
    Yamane, S
    [J]. THIRD INTERNATIONAL WORKSHOP ON REAL-TIME COMPUTING SYSTEMS AND APPLICATIONS, PROCEEDINGS, 1996, : 90 - 97
  • [7] Compositional verification of real-time systems using Ecdar
    Alexandre David
    Kim. G. Larsen
    Axel Legay
    Mikael H. Møller
    Ulrik Nyman
    Anders P. Ravn
    Arne Skou
    Andrzej Wąsowski
    [J]. International Journal on Software Tools for Technology Transfer, 2012, 14 (6) : 703 - 720
  • [8] Improving the Verification of Real-Time Systems Using Time Petri Nets
    del Foyo P.M.G.
    Silva J.R.
    [J]. Journal of Control, Automation and Electrical Systems, 2017, 28 (6) : 774 - 784
  • [9] TEMPORAL VERIFICATION OF REAL-TIME SYSTEMS
    CAMPOS, SV
    CLARKE, EM
    MARRERO, W
    MINEA, M
    HIRAISHI, H
    [J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1995, E78D (07) : 796 - 801
  • [10] Verification of real-time systems design
    Emilia Cambronero, M.
    Valero, Valentin
    Diaz, Gregorio
    [J]. SOFTWARE TESTING VERIFICATION & RELIABILITY, 2010, 20 (01): : 3 - 37
12345