Experiments with parametric verification of real-time systems

被引:0
|
作者
Spelberg, RFL [1 ]
de Rooij, RCM [1 ]
Toetenel, WJ [1 ]
机构
[1] Delft Univ Technol, Fac Informat Technol & Syst, NL-2600 AJ Delft, Netherlands
关键词
D O I
10.1109/EMRTS.1999.777458
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
The paper addresses experiments with parametric verification of real-time systems based on model-checking of models f these systems. We apply a model checking algorithm that implements the partition refinement approach. The models itself are based on the timed automata model of Alur and Dill [3]. The model specification language XTG enables the specification of constant parameters, which are given a valuation during the verification process. The outcome of the verification is presented as relations over the parameters within the specification. This feature adds a substantial power to the model-checking approach to verification. We demonstrate the usefullness of parametric verification by means of two small examples.
引用
收藏
页码:123 / 130
页数:8
相关论文
共 50 条
  • [1] TEMPORAL VERIFICATION OF REAL-TIME SYSTEMS
    CAMPOS, SV
    CLARKE, EM
    MARRERO, W
    MINEA, M
    HIRAISHI, H
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1995, E78D (07) : 796 - 801
  • [2] Verification of real-time systems design
    Emilia Cambronero, M.
    Valero, Valentin
    Diaz, Gregorio
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2010, 20 (01): : 3 - 37
  • [3] Efficient verification of parallel real-time systems
    Yoneda, T
    Schlingloff, BH
    FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) : 187 - 215
  • [4] Consistency verification in modeling of real-time systems
    Deng, Y
    Wang, JC
    Zhou, MC
    IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, 2004, 20 (01): : 136 - 142
  • [5] Modelling and Verification of Real-Time Systems with Alvis
    Szpyrka, Marcin
    Podolski, Lukasz
    Wypych, Michal
    TOWARDS A SYNERGISTIC COMBINATION OF RESEARCH AND PRACTICE IN SOFTWARE ENGINEERING, 2018, 733 : 165 - 178
  • [6] Parametric optimization of open real-time systems
    Wang, F
    Yen, HC
    STATIC ANALYSIS, PROCEEDINGS, 2001, 2126 : 299 - 318
  • [7] Deductive verification of probabilistic real-time systems
    Yamane, S
    24TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS WORKSHOPS, PROCEEDINGS, 2004, : 622 - 627
  • [8] Efficient verification of parallel real-time systems
    Tokyo Inst of Technology, Tokyo, Japan
    Formal Methods Syst Des, 2 (187-215):
  • [9] Partial orders and verification of real-time systems
    Pagani, F
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1996, 1135 : 327 - 346
  • [10] Runtime verification of embedded real-time systems
    Reinbacher, Thomas
    Fuegger, Matthias
    Brauer, Joerg
    FORMAL METHODS IN SYSTEM DESIGN, 2014, 44 (03) : 203 - 239