Formal Techniques for Verification and Testing of Cyber-Physical Systems
Formal Techniques for Verification and Testing of Cyber-Physical Systems
复制标题
DOI：
10.1007/978-3-030-13050-3_4
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Jyotirmoy V. Deshmukh;S. Sankaranarayanan
中科院分区：
文献类型：
--
作者：
Jyotirmoy V. Deshmukh;S. Sankaranarayanan
现代信息物理系统（CPS）通常采用基于模型的开发（MBD）范式。MBD范例涉及不同种类的模型的构造：（1）封装系统的物理组件的工厂模型（例如，机械、电气、化学组件），（2）封装系统的嵌入式软件组件的控制器模型，以及（3）封装CPS应用的外部环境上的物理假设的环境模型。为了推理CPS应用程序的正确性，我们通常会提出以下问题：对于所有可能的环境场景，由工厂和控制器组成的闭环系统是否表现出期望的行为？典型地，期望的行为用指定闭环系统的不安全行为的属性来表示。通常，这种行为使用实时时态逻辑的变体来表达。在本章中，我们将研究基于有界时间可达性分析的形式化方法，仿真引导的可达性分析，基于安全不变量的演绎技术，以及形式化的需求驱动测试技术。我们将回顾文献中的关键结果，并讨论这种系统在各种学术和工业环境中的可扩展性和适用性。我们通过讨论使用基于AI的软件组件的新CPS应用程序对正式验证和测试技术提出的挑战来结束本章。
Modern cyber-physical systems (CPS) are often developed in a model-based development (MBD) paradigm. The MBD paradigm involves the construction of different kinds of models: (1) a plant model that encapsulates the physical components of the system (e.g., mechanical, electrical, chemical components) using representations based on differential and algebraic equations, (2) a controller model that encapsulates the embedded software components of the system, and (3) an environment model that encapsulates physical assumptions on the external environment of the CPS application. In order to reason about the correctness of CPS applications, we typically pose the following question:For all possible environment scenarios, does the closed-loop system consisting of the plant and the controller exhibit the desired behavior?Typically, the desired behavior is expressed in terms of properties that specify unsafe behaviors of the closed-loop system. Often, such behaviors are expressed using variants of real-time temporal logics. In this chapter, we will examine formal methods based on bounded-time reachability analysis, simulation-guided reachability analysis, deductive techniques based on safety invariants, and formal, requirement-driven testing techniques. We will review key results in the literature, and discuss the scalability and applicability of such systems to various academic and industrial contexts. We conclude this chapter by discussing the challenge to formal verification and testing techniques posed by newer CPS applications that use AI-based software components.