论文部分内容阅读
基于时序Petri网对温控系统进行建模和性质描述.利用可达图、Büchi自动机和ω-正则表达式理论三者相结合的方法分析得到温控系统时序Petri网模型变迁引发序列集合的ω-正则表达式,进一步分析证明该ω-正则表达式满足温控系统的功能性需求说明,从形式上验证了温控系统时序Petri网模型与需求说明一致.结果表明,时序Petri网可用来描述和验证具有时序关系和因果关系的并发系统模型,是一种并发系统形式化描述和分析的有效工具。