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 条
  • [41] Runtime verification of embedded real-time systems
    Reinbacher, Thomas
    Fuegger, Matthias
    Brauer, Joerg
    FORMAL METHODS IN SYSTEM DESIGN, 2014, 44 (03) : 203 - 239
  • [42] An engineering process for the verification of real-time systems
    Burns, A.
    Lin, T. -M.
    FORMAL ASPECTS OF COMPUTING, 2007, 19 (01) : 111 - 136
  • [43] Compositional verification of embedded real-time systems
    Foughali, Mohammed
    Hladik, Pierre-Emmanuel
    Zuepke, Alexander
    JOURNAL OF SYSTEMS ARCHITECTURE, 2023, 142
  • [44] Runtime verification of embedded real-time systems
    Thomas Reinbacher
    Matthias Függer
    Jörg Brauer
    Formal Methods in System Design, 2014, 44 : 203 - 239
  • [45] On Improved Verification of Reconfigurable Real-Time Systems
    Hafidi, Yousra
    Kahloul, Laid
    Khalgui, Mohamed
    Ramdani, Mohamed
    PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING (ENASE), 2019, : 394 - 401
  • [46] Kronos: A verification tool for real-time systems
    Yovine, Sergio
    International Journal on Software Tools for Technology Transfer, 1997, 1 (1-2): : 123 - 133
  • [47] Predicate diagrams for the verification of real-time systems
    Kang, Eun-Young
    Merz, Stephan
    FORMAL ASPECTS OF COMPUTING, 2007, 19 (03) : 401 - 413
  • [48] A method for modeling and verification of real-time systems
    Scott, JM
    PROCEEDINGS IEEE SOUTHEASTCON '98: ENGINEERING FOR A NEW ERA, 1998, : 53 - 56
  • [49] An incremental verification algorithm for real-time systems
    Sahay, A
    Tsai, JJP
    Sistla, AP
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 1999, 9 (02) : 203 - 216
  • [50] Iterative approach to verification of real-time systems
    Univ of California, Berkeley, United States
    Formal Methods Syst Des, 1 (67-95):