Equivalent Model Verification of Task Network to Timed Automata
Xiu Jian-xin · Jisuanji gongcheng · 2012
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.