Formal Verification of Hybrid System
Formal Verification of Hybrid System
复制标题
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
B. Le
中科院分区：
文献类型：
--
作者：
B. Le
混合系统是实时嵌入式系统的非常重要的子类。混合系统的行为与离散的控制模式转换和连续的实时行为纠缠在一起，因此非常复杂且难以控制。AS Hybrid System在安全临界区域广泛使用像行业，国防和运输系统一样，有效分析和理解系统以确保系统的安全操作非常重要。诸如测试和仿真之类的技术只能观察系统的行为在给定的输入下。由于它们无法耗尽所有可能的输入和场景，它们还不足以保证系统的安全性。与基于测试的技术形成鲜明对比，正式方法可以回答诸如系统是否永远不会通过跨越某些规范来违反某些规范系统的完整状态空间。因此，追求正式验证安全 - 关键混合系统的方向非常重要。形式方法包括正式规范和正式验证。本文回顾了对混合系统的语言和规范进行建模，以及模型检查和定理中的技术。此外，它讨论了相关领域的潜在未来方向。
Hybrid System is a very important subclass of real time embedded system.The behavior of hybrid system is tangled with discrete control mode transformation and continuous real time behavior,therefore very complex and difficult to control.As hybrid system is widely used in safety-critical areas like industry,defense and transportation system,it is very important to analyze and understand the system effectively to guarantee the safe operation of the system.Ordinary techniques like testing and simulation can only observe the behavior of the system under given input.As they cannot exhaust all the possible inputs and scenarios,they are not enough to guarantee the safety of the system.In contrast to testing based techniques,formal method can answer questions like if the system will never violate certain specification by traversing the complete state space of the system.Therefore,it is very important to pursue the direction of formal verification of safety-critical hybrid system.Formal method consists of formal specification and formal verification.This paper reviews the modeling language and specification of hybrid system as well as techniques in model checking and theorem proving.In addition,it discusses the potential future directions in the related area.