摘要： 针对实时调度理论模型缺乏形式化语义的问题，提出将结果行为的语义转换成系统模型的形式化方法。结合定时分析技术，基于已有的任务网络形式方法，证明任务网络模型与候选型体系结构(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

中图分类号: 

• N945.12