Kronos: A verification tool for real-time systems

被引:152
|
作者
Yovine S. [1 ,2 ]
机构
[1] Verimag, Centre Equation, 2 Ave. de Vignate
[2] California PATH, University of California at Berkeley, Richmond Field Station Bldg. 452, 1301 S. 46th St
关键词
Bisimulation; Real-time systems; Specification; Timed automata; Timed temporal logics; Verification;
D O I
10.1007/s100090050009
中图分类号
学科分类号
摘要
The main purpose of this paper is to explain how to use Kronos, a tool for formally checking whether a real-time system meets its requirements. Kronos is founded on the theory of timed automata and timed temporal logics. © 1997 Springer-Verlag.
引用
收藏
页码:123 / 133
页数:10
相关论文
共 50 条
  • [1] Kronos: A model-checking tool for real-time systems
    Bozga, M
    Daws, C
    Maler, O
    Olivero, A
    Tripakis, S
    Yovine, S
    [J]. COMPUTER AIDED VERIFICATION, 1998, 1427 : 546 - 550
  • [2] Simulation and verification tool for hierarchical real-time systems
    Sebestyénovà, J
    [J]. 11TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOP ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 2004, : 255 - 261
  • [3] Kronos: A model-checking tool for real-time systems (Tool-presentation for FTRTFT '98)
    Bozga, M
    Daws, C
    Maler, O
    Olivero, A
    Tripakis, S
    Yovine, S
    [J]. FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1998, 1486 : 298 - 302
  • [4] TAXYS: A tool for the development and verification of real-time embedded systems
    Closse, E
    Poize, M
    Pulou, J
    Sifakis, J
    Venter, P
    Weil, D
    Yovine, S
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2001, 2102 : 391 - 395
  • [5] Oris: A tool for modeling, verification and evaluation of real-time systems
    Bucci G.
    Carnevali L.
    Ridi L.
    Vicario E.
    [J]. International Journal on Software Tools for Technology Transfer, 2010, 12 (5) : 391 - 403
  • [6] How to make a simple tool for verification of real-time systems
    Konnov I.V.
    Podymov V.V.
    Volkanov D.Y.
    Zakharov V.A.
    Zorin D.A.
    [J]. Automatic Control and Computer Sciences, 2014, 48 (7) : 534 - 542
  • [7] Moby/RT: a tool for specification and verification of real-time systems
    Olderog, ER
    Dierks, H
    [J]. JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2003, 9 (02) : 88 - 105
  • [8] TAXYS equals ESTEREL plus KRONOS - A tool for verifying real-time properties of embedded systems
    Bertin, V
    Closse, E
    Poize, M
    Pulou, J
    Sifakis, J
    Venier, P
    Weil, D
    Yovine, S
    [J]. PROCEEDINGS OF THE 40TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-5, 2001, : 2875 - 2880
  • [9] The Verus tool: A quantitative approach to the formal verification of real-time systems
    Campos, S
    Clarke, E
    Minea, M
    [J]. COMPUTER AIDED VERIFICATION, 1997, 1254 : 452 - 455
  • [10] Rabbit: A tool for BDD-based verification of real-time systems
    Beyer, D
    Lewerentz, C
    Noack, A
    [J]. COMPUTER AIDED VERIFICATION, 2003, 2725 : 122 - 125