Recent advances on formal methods for safety and security of cyber-physical systems
- PDF / 562,164 Bytes
- 3 Pages / 595.276 x 790.866 pts Page_size
- 102 Downloads / 167 Views
LETTER
Recent advances on formal methods for safety and security of cyber‑physical systems Xiang Yin1,2 · Shaoyuan Li1,2 Received: 21 September 2020 / Accepted: 21 September 2020 © South China University of Technology, Academy of Mathematics and Systems Science, CAS and Springer-Verlag GmbH Germany, part of Springer Nature 2020
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 * Xiang Yin [email protected] 1
Department of Automation, Shanghai Jiao Tong University, Shanghai 200240, China
Key Laboratory of System Control and Information Processing, Ministry of Education, Shanghai 200240, China
2
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 he
Data Loading...
