基于形式化方法的混成系统验证  

The Verification of Hybrid Systems Based on Formal Methods

作　　者：唐敏[1] 吴熊 李平 唐晨 杨国荣 TANG Min;WU Xiong;LI Ping;TANG Chen;YANG Guo-rong(Guangxi Key Laboratory of Cryptography and Information Security,Guilin University of Electrical Technology,Guilin 541004,China;Gongan County Self-discipline Junior High School,Jingzhou 434300,China)

机构地区：[1]桂林电子科技大学广西密码学与信息安全重点实验室,广西桂林541004 [2]公安县自强初级中学,湖北荆州434300

出　　处：《软件导刊》2018年第4期39-41,44,共4页Software Guide

基　　金：广西密码学与信息安全重点实验室研究课题项目(GCIS201615);2016年自治区级大学生创新训练计划项目(C66JWA 24QX18)

摘　　要：对混成系统进行安全性验证是计算机领域具有重要意义和挑战性的课题,传统的测试仿真技术不足以确保系统的绝对安全性和完备性。基于形式化方法是根据混成系统的形式规范与属性,使用数学方法证明其正确性或非正确性。对温控系统实现了抽象算法的形式化,首先对线性混成系统的状态空间进行分割,然后将其转化为图的可达性问题,利用图算法求解,最终对系统进行了安全性验证。实验结果表明,采用形式化方法对混成系统进行安全性验证具有较高的可靠性与可信性。The safety verification of hybrid systems is an important and challenging subject in the computer field.The traditional test and simulation technology is not enough to ensure the absolute security and completeness of the system.The formal verification method is based on the formal specification of hybrid systems and properties,using mathematical method to testify its correctness.We implement the formalization of the abstraction algorithm to verify the safety of temperature control systems.We first divide the state space of a linear hybrid system into several parts,and then transform it to the reachability problem of a graph,finally we use graph algorithm to verify the safety of this system.Compared with the simulation and testing methods,the formal method has higher reliability and credibility.

关 键 词：形式化方法 抽象算法 混成系统 温控系统 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]