| 摘要: |
| Cyber-physical systems (CPSs) are engineering systems with both computational and physical components [1]. Typical CPSs include energy systems, transportation systems, autonomous vehicles, etc. CPSs are usually hybrid involving complex interactions of continuous dynamics with discrete logics. The development of controller design and verification algorithms for such complex systems are crucial and challenging tasks. Ever-increasing demands for safety and security of CPSs put stringent constraints on their analysis and design, and necessitate the use of formal model-based approaches. In recent years, we have witnessed a substantial increase in the use of formal techniques for the verification and design of safety–critical and security-sensitive CPSs [2].
Due to the complex functionalities of safety–critical CPSs, ensuring safety is extremely challenging. In particular, since CPSs involve both continuous and discrete dynamics, safety not only requires that the low-level physical trajectory is within constrained regions, e.g., the value of the state should never exceed a threshold, but also requires that the high-level behavior of the system satisfies some desired specifications, e.g., executing a set of tasks in a right order. However, existing control theory mainly focuses on simple low-level specifications such as stability. To describe functional safety of the high-level behaviors of CPSs, more rich specification languages, such as regular languages and linear temporal logics (LTL), are needed. Also, security-related attacks are increasingly becoming pervasive in safety–critical cyber-physical systems; such security vulnerabilities related to information leaks in CPSs are extremely difficult to discover and mitigate as the interaction between the embedded control software and the physical environment exposes numerous attack surfaces for malicious exploitation.
To enforce complex specifications for safety–critical cyber-physical systems, one of the most popular approaches developed in the past 50 years is the abstraction-based approach, which consists of the following steps: 1) abstract the original infinite continuous system as a finite symbolic system; 2) synthesize a supervisory controller based on the symbolic model to enforce desired specifications; 3) refine the symbolic controller synthesized to control the original system. To construct the symbolic model, a typical approach is to discretize the state-space to induce a finite quotient system. The key here is to establish certain relationship between the original system and its abstraction. In the seminal work of [3], the notion of approximate bi-simulation relation was proposed to capture the equivalence of two models with guaranteed abstraction error; this idea was further extended to the notion of alternating bi-simulation relation for the purpose of control [4]. Recently in [5], a more unified relation called feedback refinement relation was proposed. Compositional approaches have also been developed to compute finite abstractions for large-scale interconnected CPSs [6].... |
| 关键词: |
| DOI：https://doi.org/10.1007/s11768-020-00008-w |
|
| 基金项目: |
|
| Recent advances on formal methods for safety and security of cyber-physical systems |
| Xiang Yin,Shaoyuan Li |
| () |
| Abstract: |
| Cyber-physical systems (CPSs) are engineering systems with both computational and physical components [1]. Typical CPSs include energy systems, transportation systems, autonomous vehicles, etc. CPSs are usually hybrid involving complex interactions of continuous dynamics with discrete logics. The development of controller design and verification algorithms for such complex systems are crucial and challenging tasks. Ever-increasing demands for safety and security of CPSs put stringent constraints on their analysis and design, and necessitate the use of formal model-based approaches. In recent years, we have witnessed a substantial increase in the use of formal techniques for the verification and design of safety–critical and security-sensitive CPSs [2].
Due to the complex functionalities of safety–critical CPSs, ensuring safety is extremely challenging. In particular, since CPSs involve both continuous and discrete dynamics, safety not only requires that the low-level physical trajectory is within constrained regions, e.g., the value of the state should never exceed a threshold, but also requires that the high-level behavior of the system satisfies some desired specifications, e.g., executing a set of tasks in a right order. However, existing control theory mainly focuses on simple low-level specifications such as stability. To describe functional safety of the high-level behaviors of CPSs, more rich specification languages, such as regular languages and linear temporal logics (LTL), are needed. Also, security-related attacks are increasingly becoming pervasive in safety–critical cyber-physical systems; such security vulnerabilities related to information leaks in CPSs are extremely difficult to discover and mitigate as the interaction between the embedded control software and the physical environment exposes numerous attack surfaces for malicious exploitation.
To enforce complex specifications for safety–critical cyber-physical systems, one of the most popular approaches developed in the past 50 years is the abstraction-based approach, which consists of the following steps: 1) abstract the original infinite continuous system as a finite symbolic system; 2) synthesize a supervisory controller based on the symbolic model to enforce desired specifications; 3) refine the symbolic controller synthesized to control the original system. To construct the symbolic model, a typical approach is to discretize the state-space to induce a finite quotient system. The key here is to establish certain relationship between the original system and its abstraction. In the seminal work of [3], the notion of approximate bi-simulation relation was proposed to capture the equivalence of two models with guaranteed abstraction error; this idea was further extended to the notion of alternating bi-simulation relation for the purpose of control [4]. Recently in [5], a more unified relation called feedback refinement relation was proposed. Compositional approaches have also been developed to compute finite abstractions for large-scale interconnected CPSs [6].... |
| Key words: |
