温控系统的时序Petri网建模与验证

• 作者: 李文翔
• 来源期刊: 山东理工大学学报（自然科学版）
• 学科: 工学
• 关键词: 时序Petri网 ω-正则表达式 模型检测 形式化建模 形式化分析
• 年，卷（期）: 2018,（6）
• 页码范围: 24-28
• 页数: 5页
• 分类号: TP311.5
• 字数: 3637字
• 语种: 中文
• DOI: 10.3969/j.issn.1672-6197.2018.06.006

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李文翔	福建商学院信息工程系	5	6	1.0	2.0