The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results). To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Stochastic Timed Graph Transformation Systems

  • Sven Schneider,
  • Maria Maximova,
  • Holger Giese

摘要

The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results). To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.