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

Equivalent Model Verification of Task Network to Timed Automata

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

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.