A discrete time model for performance evaluation and correctness verification of real time systems

被引:2
|
作者
Bucci, G [1 ]
Sassoli, L [1 ]
Vicario, E [1 ]
机构
[1] Univ Florence, Dipartimento Sistemi & Informat, Florence, Italy
来源
10TH INTERNATIONAL WORKSHOP ON PETRI NETS AND PERFORMANCE MODELS, PROCEEDINGS | 2003年
关键词
D O I
10.1109/PNPM.2003.1231550
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In the development of reactive systems, correctness and performance requirements are often intertwined. An integral approach to both the aspects of the problem requires models and analysis techniques which jointly capture probabilistic and minimum/maximum characterization of time delays. A discrete time extension of Time Petri Nets is introduced, which extends minimum/maximum timing constraints with a discrete probability density As a characterizing trait, the model is interpreted according to a semantics of true concurrency, representing dynamic behavior in terms of the probability, that a set of transitions fires at the current tick of the clock. Behavioral and probabilistic rules in the semantics of the model are soundly captured into an enumerative technique which represents the state space of the model as a transition system labeled with delays and probabilities. This enables both Markovian analysis techniques and inspection algorithms supporting verification of sequencing and minimum/maximum durational properties.
引用
收藏
页码:134 / 143
页数:10
相关论文
共 50 条
  • [31] Discrete time model of sexual systems
    Jamilov, Uygun
    Mukhamedov, Farrukh
    Mukhamedova, Farzona
    HELIYON, 2023, 9 (07)
  • [32] Discrete time approach of time Petri nets for real-time systems analysis
    Roux, OH
    Delfieu, D
    Molinaro, P
    ETFA 2001: 8TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOL 2, PROCEEDINGS, 2001, : 197 - 204
  • [33] Efficient verification of parallel real-time systems
    Yoneda, T
    Schlingloff, BH
    FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) : 187 - 215
  • [34] 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
  • [35] 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
  • [36] Probabilistic model checking: Formalisms and algorithms for discrete and real-time systems
    Courcoubetis, C
    Tripakis, S
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 183 - 219
  • [37] Experiments with parametric verification of real-time systems
    Spelberg, RFL
    de Rooij, RCM
    Toetenel, WJ
    PROCEEDINGS OF THE 11TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS, 1999, : 123 - 130
  • [38] Deductive verification of probabilistic real-time systems
    Yamane, S
    24TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS WORKSHOPS, PROCEEDINGS, 2004, : 622 - 627
  • [39] Efficient verification of parallel real-time systems
    Tokyo Inst of Technology, Tokyo, Japan
    Formal Methods Syst Des, 2 (187-215):
  • [40] Partial orders and verification of real-time systems
    Pagani, F
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1996, 1135 : 327 - 346