Toward online hybrid systems model checking of cyber-physical systems' time-bounded short-run behavior

2011 ◽  
Vol 8 (2) ◽  
pp. 7-10 ◽  
Author(s):  
Lei Bu ◽  
Qixin Wang ◽  
Xin Chen ◽  
Linzhang Wang ◽  
Tian Zhang ◽  
...  
Keyword(s):  
Model Checking ◽  
Hybrid Systems ◽  
Cyber Physical Systems ◽  
Physical Systems ◽  
Systems Model ◽  
Short Run

scholarly journals Towards a Verification-Driven Iterative Development of Software for Safety-Critical Cyber-Physical Systems

2021 ◽  
Vol 12 (1) ◽  
Author(s):  
Marjan Sirjani ◽  
Luciana Provenzano ◽  
Sara Abbaspour Asadollah ◽  
Mahshid Helali Moghadam ◽  
Mehrdad Saadatmand
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Reactive Systems ◽  
Cyber Physical Systems ◽  
Software Systems ◽  
Behavioral Models ◽  
Physical Systems ◽  
Model Driven ◽  
Systems Model ◽  
Executable Code

AbstractSoftware systems are complicated, and the scientific and engineering methodologies for software development are relatively young. Cyber-physical systems are now in every corner of our lives, and we need robust methods for handling the ever-increasing complexity of their software systems. Model-Driven Development is a promising approach to tackle the complexity of systems through the concept of abstraction, enabling analysis at earlier phases of development. In this paper, we propose a model-driven approach with a focus on guaranteeing safety using formal verification. Cyber-physical systems are distributed, concurrent, asynchronous and event-based reactive systems with timing constraints. The actor-based textual modeling language, Rebeca, with model checking support is used for formal verification. Starting from structured requirements and system architecture design the behavioral models, including Rebeca models, are built. Properties of interest are also derived from the structured requirements, and then model checking is used to formally verify the properties. This process can be performed in iterations until satisfaction of desired properties are ensured, and possible ambiguities and inconsistencies in requirements are resolved. The formally verified models can then be used to develop the executable code. The Rebeca models include the details of the signals and messages that are passed at the network level including the timing, and this facilitates the generation of executable code. The natural mappings among the models for requirements, the formal models, and the executable code improve the effectiveness and efficiency of the approach.

A Novel Cyber Physical Systems Model

2010 ◽  
Vol 44-47 ◽  
pp. 4058-4062
Author(s):  
Xiao Wu Liu ◽  
Zhong He Gao ◽  
Ji Guo Yu
Keyword(s):  
Cyber Physical Systems ◽  
Research Field ◽  
Cross Layer ◽  
Information Technology Industry ◽  
Physical Systems ◽  
New Science ◽  
Technology Industry ◽  
Systems Model ◽  
New Research ◽  
Future Work

Cyber Physical Systems (CPS) is a new science to joint physical and computation together and it can be used in information technology, industry process control and other fields. But its model remains a new research field that needs to be explored. In this paper, we put forward a novel CPS model based on Cognitive Network (CN) and accomplished the combination of CPS and CN. The model was composed of four layers included physical layer, network layer, user layer and cross layer. We discussed every layer in our model in which the functions such as control, communication and so on were described. We also presented the feedback circle in cross layer detailedly. Finally, we explained the suggestion and future work briefly.

scholarly journals Real Analysis for Complex Systems

10.29007/ksvj ◽  
2018 ◽  
Author(s):  
Andrè Platzer
Keyword(s):  
Differential Equations ◽  
Hybrid Systems ◽  
Traffic Control ◽  
Theoretical Perspective ◽  
Practical Interest ◽  
Theorem Prover ◽  
Physical Systems ◽  
Systems Model ◽  
Model Complex ◽  
Verification Techniques

Formal verification techniques are used routinely in finite-state digital circuits. Theorem proving is also used successfully for infinite-state discrete systems. But many safety-critical computers are actually embedded in physical systems. Hybrid systems model complex physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. There is a well-understood theory for proving programs. But what about complex physical systems? How can we prove that a hybrid system works as expected, e.g., an aircraft does not crash into another one?This talk illustrates the complexities and pitfalls of hybrid systems verification. It describes a theoretical and practical foundation for deductive verification of hybrid systems called differential dynamic logic. The proof calculus for this logic is interesting from a theoretical perspective, because it is a complete axiomatization of hybrid systems relative to differential equations. The approach is of considerable practical interest too. Its implementation in the theorem prover KeYmaera has been used successfully to verify collision avoidance properties in the European Train Control System and air traffic control systems. The number of dimensions and nonlinearities in they hybrid dynamics of these systems is surprisingly tricky such that they are still out of scope for other verification tools.

scholarly journals Structured Proofs for Adversarial Cyber-Physical Systems

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Brandon Bohrer ◽  
André Platzer
Keyword(s):  
Hybrid Systems ◽  
Differential Game ◽  
Programming Language ◽  
First Language ◽  
Cyber Physical Systems ◽  
Proof Checking ◽  
Game Logic ◽  
Physical Systems ◽  
Safety Critical ◽  
High Level

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.

Sign in / Sign up

Export Citation Format

Share Document