摘要
嵌入式实时系统多数应用在安全性要求较高的场合,因此需要保证系统的正确性。复杂性不断增加的实时系统迫切需要在系统开发早期引入形式化分析技术来验证系统的期望性质。时间Petri网是有严格数学基础的图形表达工具,适合对实时系统建模;时间自动机(Timed Automata,TA)有成熟的验证工具,被广泛用于实时系统的模型检验和验证。本文提出一种基于着色时间Petri网(Colored Time Petri Net,CTPN)的实时系统的验证方法,用CTPN对带有控制流和数据流的实时系统建模,通过转换规则将CTPN模型转换成语义等价的TA模型,利用模型检验工具UPPAAL验证系统的性质。最后,用实例证明此方法有效。
Most Real-time Embedded Systems have been used in safety-critical situation, which is necessary to ensure the correctness of systems. The growing complexity of real-time embedded systems makes it imperative to apply formal analysis techniques at early stages of system development. Time Petri Net is a graphical formal method based on strict mathematics, which is suitable to model real-time systems. Timed Automata （TA）, which has mature validation tools, has been widely used to verify and model check of real-time systems. This paper considers a verification method of real-time systems based on Colored Time Petri Nets （CTPN）, using CTPN to accurately describe the systems both with control flow and data flow, the mapping rules from CTPN to TA that preserves the behavioral semantics （timed bisimilarity） of the initial CTPN is given, on the base of this, the dynamic behavior of system is analyzed by UPPAAL. Finally,an example is provided to demonstrate the modeling process and formal verification.
出处
《计算机科学》
CSCD
北大核心
2008年第7期257-260,共4页
Computer Science
基金
国家自然科学基金(No.60373000)
国家863高技术研究发展计划(Nos.863-317-01-04-99,2001AA115126)基金资助
