Model Checking MASL Specification of Distributed Real-Time Systems

被引：0
|
作者：
Bugaichenko, D. Yu.
机构：
来源：
VESTNIK ST PETERSBURG UNIVERSITY-MATHEMATICS | 2007年 / 40卷 / 03期
关键词：
D O I：
10.3103/S1063454107030065
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
We present model checking algorithms for MASL specification of distributed real-time systems. The proposed algorithms use symbolic model checking approach by analogy with model checking algorithms for branching-time temporal logic CTL and alternating-time temporal logic ATL. For the fixed environment case, the algorithm is polynomial-time in the specification length and sizes of the sets of system states and actions. For the dynamic environment case, the algorithm is polynomial-time in the model size, but it is exponential-time in the structure of environment specification.
引用
收藏
页码：201 / 208
页数：8
相关论文
共 50 条
  • [21] Model-checking distributed real-time systems with states, events, and multiple fairness assumptions
    Wang, F
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 553 - 567
  • [22] Verifying distributed real-time properties of embedded systems via graph transformations and model checking
    Gabor Madl
    Sherif Abdelwahed
    Douglas C. Schmidt
    Real-Time Systems, 2006, 33 : 77 - 100
  • [23] Verifying distributed real-time properties of embedded systems via graph transformations and model checking
    Gabor, MU
    Sherif, AU
    Schmidt, DC
    REAL-TIME SYSTEMS, 2006, 33 (1-3) : 77 - 100
  • [24] Aspect-oriented specification architectures for distributed real-time systems
    Katara, M
    Mikkonen, T
    SEVENTH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2001, : 180 - 190
  • [25] A general time model for the specification and design of embedded real-time systems
    Münzenberger, R
    Dörfel, M
    Hofmann, R
    Slomka, F
    MICROELECTRONICS JOURNAL, 2003, 34 (11) : 989 - 1000
  • [26] On-the-fly symbolic model checking for real-time systems
    Bouajjani, A
    Tripakis, S
    Yovine, S
    18TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1997, : 25 - 34
  • [27] Comparing model checking and logical reasoning for real-time systems
    Dierks, H
    FORMAL ASPECTS OF COMPUTING, 2004, 16 (02) : 104 - 120
  • [28] A parametric model checking approach for real-time systems design
    Sathawornwichit, C
    Katayama, T
    12th Asia-Pacific Software Engineering Conference, Proceedings, 2005, : 584 - 591
  • [29] Model Checking of Real-Time Systems Using Rewriting Logic
    Bendiaf, Messaoud
    Bourahla, Mustapha
    Boudia, Malika
    Rehab, Seidali
    PROCEEDINGS OF 2017 INTERNATIONAL CONFERENCE ON ELECTRICAL AND INFORMATION TECHNOLOGIES (ICEIT 2017), 2017,
  • [30] Model Checking the Information Flow Security of Real-Time Systems
    Gerking, Christopher
    Schubert, David
    Bodden, Eric
    ENGINEERING SECURE SOFTWARE AND SYSTEMS, ESSOS 2018, 2018, 10953 : 27 - 43
12345