Towards TCTLhΔ model checking of Time Petri Nets

被引:0
|
作者
Chtourou, Ameni [1 ]
Sbai, Zohra [1 ]
机构
[1] Univ Tunis El Manar, Ecole Natl Ingn Tunis, BP 37 Belvedere, Tunis 1002, Tunisia
关键词
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
At present, the most common method for verifying that a system met its specifications or to detect unexpected behavior and issues is to perform simulations on the model. This approach is limited by the fact that it is of course impossible to be exhaustive and fully test the system. This is why the need to resort to formal methods, and more particularly to model-checking, was felt. In this paper, we are interested by modeling the behavior of real time systems using time Petri nets. Our main objective is to present new model checking algorithms for our new logic called TCTLh Delta new which is the combination of the two extensions of the TCTL logic TCTLh and TCTLh Delta. These algorithms are based on the concept of on the fly verification and are implemented into the model checker Romeo.
引用
收藏
页码:563 / 568
页数:6
相关论文
共 50 条
  • [41] Model Checking Control Flow Petri Nets Using PAT
    Ho, Dung T.
    Bui, Thang H.
    Quan, Tho T.
    [J]. PROCEEDINGS OF THE 2013 13TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE AND ITS APPLICATIONS (ICCSA 2013), 2013, : 124 - 129
  • [42] A compositional model of time Petri nets
    Koutny, M
    [J]. APPLICATION AND THEORY OF PETRI NETS 2000, PROCEEDINGS, 2000, 1825 : 303 - 322
  • [43] Diagnosability of Event Patterns in Safe Labeled Time Petri Nets: A Model-Checking Approach
    Pencole, Yannick
    Subias, Audine
    [J]. IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2022, 19 (02) : 1151 - 1162
  • [44] THE CHECKING OF LIVENESS OF ORDINARY PETRI NETS
    ZAKREVSKII, AD
    [J]. DOKLADY AKADEMII NAUK BELARUSI, 1985, 29 (11): : 1006 - 1009
  • [45] Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets
    Janowska, Agata
    Penczek, Wojciech
    Polrola, Agata
    Zbrzezny, Andrzej
    [J]. TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY VIII, 2013, 8100 : 89 - 105
  • [46] Towards a General Model to Handle Multi-enabledness in Time Petri Nets
    Abdelli, Abdelkrim
    [J]. FORMALISMS FOR REUSE AND SYSTEMS INTEGRATION, 2015, 346 : 103 - 131
  • [47] Consistency's checking of chronicles' set Using Time Petri Nets
    Saddem, Ramla
    Toguyeni, Armand
    Tagina, Moncef
    [J]. 18TH MEDITERRANEAN CONFERENCE ON CONTROL AND AUTOMATION, 2010, : 1520 - 1525
  • [48] Scenario-based timing consistency checking for time Petri nets
    Li Xuandong
    Bu Lei
    Hu Jun
    Zhao Jianhua
    Zhang Tao
    Zheng Guoliang
    [J]. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2006, 2006, 4229 : 388 - 403
  • [49] SMT-Based Reachability Checking for Bounded Time Petri Nets
    Polrola, Agata
    Cybula, Piotr
    Meski, Artur
    [J]. FUNDAMENTA INFORMATICAE, 2014, 135 (04) : 467 - 482
  • [50] Towards a Consistent Semantics for Unsafe Time Petri Nets
    Abdelli, Abdelkrim
    [J]. ADVANCES IN SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 59 : 42 - 49