scholarly journals Structured Proofs for Adversarial Cyber-Physical Systems

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Brandon Bohrer ◽  
André Platzer

Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model’s correctness specification always holds. Constructive Differential Game Logic ( CdGL ) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proof-checking tool. We introduce Kaisar , the first language and tool for CdGL proofs, which until now could only be written by hand with a low-level proof calculus. Kaisar’s structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and high-level stateful reasoning. Kaisar exploits CdGL ’s constructivity and refinement relations to build proofs around models of game strategies. The evaluation reproduces and extends existing case studies on 1D and 2D driving. Proof metrics are compared and reported experiences are discussed for the original studies and their reproductions.


Author(s):  
Guru Prasad Bhandari ◽  
Ratneshwer Gupta

Cyber-physical systems (CPSs) are co-engineered integrating with physical and computational components networks. Additionally, a CPS is a mechanism controlled or monitored by computer-based algorithms, tightly interacting with the internet and its users. This chapter presents the definitions relating to dependability, safety-critical and fault-tolerance of CPSs. These definitions are supplemented by other definitions like reliability, availability, safety, maintainability, integrity. Threats to dependability and security like faults, errors, failures are also discussed. Taxonomy of different faults and attacks in CPSs are also presented in this chapter. The main objective of this chapter is to give the general information about secure CPS to the learners for the further enhancement in the field of CPSs.



2020 ◽  
Vol 10 (9) ◽  
pp. 3125
Author(s):  
Saad Mubeen ◽  
Elena Lisova ◽  
Aneta Vulgarakis Feljan

Cyber Physical Systems (CPSs) are systems that are developed by seamlessly integrating computational algorithms and physical components, and they are a result of the technological advancement in the embedded systems and distributed systems domains, as well as the availability of sophisticated networking technology. Many industrial CPSs are subject to timing predictability, security and functional safety requirements, due to which the developers of these systems are required to verify these requirements during the their development. This position paper starts by exploring the state of the art with respect to developing timing predictable and secure embedded systems. Thereafter, the paper extends the discussion to time-critical and secure CPSs and highlights the key issues that are faced when verifying the timing predictability requirements during the development of these systems. In this context, the paper takes the position to advocate paramount importance of security as a prerequisite for timing predictability, as well as both security and timing predictability as prerequisites for functional safety. Moreover, the paper identifies the gaps in the existing frameworks and techniques for the development of time- and safety-critical CPSs and describes our viewpoint on ensuring timing predictability and security in these systems. Finally, the paper emphasises the opportunities that artificial intelligence can provide in the development of these systems.



2019 ◽  
Vol 1 (2) ◽  
pp. 19-37
Author(s):  
K. Sridhar Patnaik ◽  
Itu Snigdh

Cyber-physical systems (CPS) is an exciting emerging research area that has drawn the attention of many researchers. However, the difficulties of computing and physical paradigm introduce a lot of trials while developing CPS, such as incorporation of heterogeneous physical entities, system verification, security assurance, and so on. A common or unified architecture plays an important role in the process of CPS design. This article introduces the architectural modeling representation of CPS. The layers of models are integrated from high level to lower level to get the general Meta model. Architecture captures the essential attributes of a CPS. Despite the rapid growth in IoT and CPS a general principled modeling approach for the systematic development of these new engineering systems is still missing. System modeling is one of the important aspects of developing abstract models of a system wherein, each model represents a different view or perspective of that system. With Unified Modeling Language (UML), the graphical analogy of such complex systems can be successfully presented.



2011 ◽  
Vol 22 (1) ◽  
pp. 101-119 ◽  
Author(s):  
Patrick Martin ◽  
Magnus B. Egerstedt


2019 ◽  
Vol 32 (2) ◽  
Author(s):  
Atif Mashkoor ◽  
Johannes Sametinger ◽  
Miklós Biro ◽  
Alexander Egyed


Sign in / Sign up

Export Citation Format

Share Document