检索
E-mail
RSS
作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2012, Vol. 38 ›› Issue (13): 286-288.doi: 10.3969/j.issn.1000-3428.2012.13.086

• 开发研究与设计技术 • 上一篇    下一篇

任务网络到时间自动机的等价模型验证

张 磊1 ，马光胜2，修建新1   

  1. (1. 黑龙江东方学院计算机科学与电气工程学部，哈尔滨 150086；2. 哈尔滨工程大学计算机科学与技术学院，哈尔滨 150001)
  • 收稿日期:2011-11-14 出版日期:2012-07-05 发布日期:2012-07-05
  • 作者简介:张 磊(1979－)，女，讲师，主研方向：形式化验证技术，软件工程；马光胜，教授；修建新，讲师
  • 基金项目:
    黑龙江省教育厅科学技术研究基金资助项目(11544037)

Equivalent Model Verification of Task Network to Timed Automata

ZHANG Lei 1, MA Guang-sheng 2, XIU Jian-xin 1   

  1. (1. Department of Computer Science and Electric Engineering, East University of Heilongjiang, Harbin 150086, China; 2. College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China)
  • Received:2011-11-14 Online:2012-07-05 Published:2012-07-05

PDF

591

摘要： 针对实时调度理论模型缺乏形式化语义的问题，提出将结果行为的语义转换成系统模型的形式化方法。结合定时分析技术，基于已有的任务网络形式方法，证明任务网络模型与候选型体系结构(CTA)模型稳态的等效性，将任务网络模型映射到语义相同的CTA模型，并验证该映射的语义等效性。将该方法应用于实例中，结果表明，该方法能代替调度模型，高效地应用于实时调度系统。

关键词: 事件流, 任务网络, 时间自动机, 映射, 模型检测, 任务行为

Abstract: Models used in real-time schedule theory usually lack formal semantics. Aiming at this problem, this paper presents an approach that transfers the semantics of result behavior into the formal method of system model, which can combine with effective timed analysis technology and present the steady-state equivalence of task networks and Candidate Type Architecture(CTA) model based on existing formalism to map task networks model into respective CTA model, and prove the semantic equivalence by theorem. The proposed method is applied to specific instance. Practical examples demonstrate the method can replace the schedule model, and be applied to real-time schedule system effiectively.

Key words: event stream, task network, timed automata, mapping, model checking, task behavior

中图分类号: