...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Applied mathematics and computation >Model checking time-dependent system specifications using Time Stream Petri Nets and Uppaal
【24h】

Model checking time-dependent system specifications using Time Stream Petri Nets and Uppaal

机译：使用时间流Petri网和Uppaal对与时间相关的系统规格进行模型检查

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper describes an approach to modeling and analysis of time-dependent system specifications which is based on the Time Stream Petri Nets (TSPNs) formalism. The work argues that although TSPNs were originally proposed for modeling multimedia/hypermedia systems, they are well suited for expressing timing constraints in general time-dependent systems. The approach is assisted by some developed tools based on model checking in terms of Uppaal timed automata, which permit behavioural analysis and in particular schedulability analysis of task executions in real-time specifications. Property analysis rests on the construction of a (hopefully finite) zone state graph of a TSPN model and its efficient traversal by Uppaal verifier, which in turn represents an effective approach for dealing with infinite computations in a compact way. The paper introduces the TSPN formalism and focuses on the implemented structural translation onto Uppaal which is assisted by a library of reusable template processes. The modeling/analysis techniques are demonstrated by two examples. The first example deals with project management, i.e. the exhaustive analysis of general CPM/PERT project models where an activity duration is expressed by a time interval. The second example is related to a thoroughly analysis of the temporal behaviour of a complex embedded real-time system with timing constraints. An indication of on-going and future work is, finally, given in the conclusions. Soundness of the structural translation is shown by a formal proof reported in appendix.
机译：本文介绍了一种基于时间流Petri网（TSPNs）形式主义的，与时间相关的系统规范的建模和分析方法。这项工作认为，尽管TSPN最初是为建模多媒体/超媒体系统而提出的，但它们非常适合在一般的时间相关系统中表达时序约束。该方法得到了一些开发的工具的支持，这些工具基于Uppaal定时自动机，基于模型检查，可以进行行为分析，尤其是实时规范中任务执行的可调度性分析。属性分析基于TSPN模型的（希望有限）区域状态图的构建及其Uppaal验证程序的有效遍历，这反过来又代表了一种以紧凑方式处理无限计算的有效方法。本文介绍了TSPN形式主义，并着重于在Uppaal上进行的结构化翻译，并借助可重复使用的模板过程库进行了翻译。通过两个示例演示了建模/分析技术。第一个示例涉及项目管理，即对一般CPM / PERT项目模型的详尽分析，其中活动持续时间用时间间隔表示。第二个示例涉及对具有时序约束的复杂嵌入式实时系统的时间行为的全面分析。结论中最后给出了正在进行的和将来的工作的指示。附录中的正式证明显示了结构翻译的正确性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号