温控系统的π-演算的描述与验证  

Description and Verification of Temperature Control System Based on π-Calculus

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

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

出　　处：《安庆师范大学学报（自然科学版）》2018年第3期65-68,共4页Journal of Anqing Normal University(Natural Science Edition)

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

摘　　要：根据温控系统的特征以及需求说明,利用π-演算构建了该系统动态行为的交互模型,依据π-演算的反应规则仿真描述模型的行为交互过程,使用μ-演算和移动工作平台(MWB)工具分析和验证了该交互模型具有温度控制和阈值修改功能,从形式上证明了温控系统的需求说明及其π-演算模型的一致性。结果表明,π-演算能够清楚地描述和分析并发系统的行为交互,而μ-演算可以证明模型的有效性和正确性。According to the characteristics of temperature control system and the requirement,this paper constructs the interactive model of the dynamic behavior in the system based onπ-calculus,and then simulates the interactions of this model by the transition rules inπ-calculus.Finally,usingμ-calculus and MWB tools,we analyzed and verified that the interaction model has temperature control and threshold modification.The consistency between the requirements specifications of the temperature control system and itsπ-calculus model is proved formally.The results show that theπ-calculus can clearly describe and analyze the behavior interaction of concurrent systems,and theμ-calculus can prove the validity and correctness of the model.

关 键 词：Π-演算 μ-演算 形式化建模 模型检测 温控系统 

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