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

Modeling and verification of a temperature control system based on temporal Petri nets

作　　者：李文翔 LI Wen xiang(Department of Information Engineering,Fujian Business University,Fuzhou 350012,China)

机构地区：[1]福建商学院信息工程系,福建福州350012

出　　处：《山东理工大学学报（自然科学版）》2018年第6期24-28,共5页Journal of Shandong University of Technology:Natural Science Edition

基　　金：福建省教育厅中青年教师教育科研项目(科技类)(JAT160786;JAT171020)

摘　　要：基于时序Petri网对温控系统进行建模和性质描述.利用可达图、Büchi自动机和ω-正则表达式理论三者相结合的方法分析得到温控系统时序Petri网模型变迁引发序列集合的ω-正则表达式,进一步分析证明该ω-正则表达式满足温控系统的功能性需求说明,从形式上验证了温控系统时序Petri网模型与需求说明一致.结果表明,时序Petri网可用来描述和验证具有时序关系和因果关系的并发系统模型,是一种并发系统形式化描述和分析的有效工具.In the paper,a temperature control system is modeled and described by temporal Petri nets.In the temporal Petri nets model of the given temperature control system,an Omega regular expressions of the firing sequence is obtained by using the reachability graph,Büchi automaton and Omega regular expression theory.Further analysis proves that this Omega regular expressions satisfies the functional requirements of temperature control system,and the consistency between the temporal Petri nets model of the given temperature control system and the requirement specification is formally verified.As a result,the concurrent system model with the causal and temporal relationships can be described and verified by using temporal Petri nets,and it is an effective tool for formal description and analysis of the concurrent systems.

关 键 词：时序PETRI网 ω-正则表达式 模型检测 形式化建模 形式化分析 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]