基于着色时间Petri网的实时系统的形式验证

计算机科学 ›› 2008, Vol. 35 ›› Issue (7): 257-260.

基于着色时间Petri网的实时系统的形式验证

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金（No.60373000）、国家863高技术研究发展计划（Nos.863-317-01-04-99,2001AA115126）基金资助.

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 嵌入式实时系统多数应用在安全性要求较高的场合，因此需要保证系统的正确性。复杂性不断增加的实时系统迫切需要在系统开发早期引入形式化分析技术来验证系统的期望性质。时间Petri网是有严格数学基础的图形表达工具，适合对实时系统建模；时间自动机（Timed Automata，TA）有成熟的验证工具，被广泛用于实时系统的模型检验和验证。本文提出一种基于着色时间Petri网（Colored Time PetriNet，CTPN）的实时系统的验证方法，用CTPN对带有控制流和数据流的实时系统建模，通过转换规则将CTPN

关键词: 着色时间Petri网时间自动机转换算法模型检验

Abstract: 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 sta

Key words: Colored time petri net,Timed automata,CTPN-to-TA, Model checking

. 基于着色时间Petri网的实时系统的形式验证[J]. 计算机科学, 2008, 35(7): 257-260. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed