Formal verification provides strong safety guarantees but only for models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe future circumstances. Formal verification then ensures that the controllers correctly identify and provably avoid unsafe future situations under a certain model of physics. But any model of physics necessarily deviates from reality and, moreover, any observation with real sensors and manipulation with real actuators is subject to uncertainty. This makes runtime validation a crucial step to monitor whether the model assumptions hold for the real system implementation. The key question is what property needs to be runtime-monitored and what a satisfied runtime monitor entails about the safety of the system: the observations of a runtime monitor only relate back to the safety of the system if they are themselves accompanied by a proof of correctness! For an unbroken chain of correctness guarantees, we, thus, synthesize runtime monitors in a provably correct way from provably safe hybrid system models. This paper addresses the inevitable challenge of making the synthesized monitoring conditions robust to partial observability of sensor uncertainty and partial controllability due to actuator disturbance. We show that the monitoring conditions result in provable safety guarantees with fallback controllers that react to monitor violation at runtime.
Specification mining techniques for LTL can be adapted to monitor for safety violations @cite_24 and intervene ahead of time, assuming that the is available to the monitor. In cyber-physical systems, this is feasible only when the next input can be prevented from becoming actuated, which is the rationale behind our controller monitors @cite_20 safeguarding untrusted control. When the next input is measured through sensors after the fact it may already present a (unpreventable) safety violation; counteracting these requires additional assumptions on the nature of the violation @cite_20 and, as presented in this paper, means to detect gradual deviation from the model that accumulates to violation over time.
@cite_24 @cite_20
2086359741 4564113 2151958719 2956034981
As the complexity of cyber-physical systems increases, so does the number of ways an adversary can disrupt them. This necessitates automated anomaly detection methods to detect possible threats. In this paper, we extend our recent results in the field of inference via formal methods to develop an unsupervised learning algorithm. Our procedure constructs from data a signal temporal logic (STL) formula that describes normal system behavior. Trajectories that do not satisfy the learned formula are flagged as anomalous. STL can be used to formulate properties such as “If the train brakes within 500 m of the platform at a speed of 50 km hr, then it will stop in at least 30 s and at most 50 s.” STL gives a more human-readable representation of behavior than classifiers represented as surfaces in high-dimensional feature spaces. STL formulae can also be used for early detection via online monitoring and for anomaly mitigation via formal synthesis. We demonstrate the power of our method with a physical model of a train's brake system. To our knowledge, this paper is the first instance of formal methods being applied to anomaly detection. Abstract : In this report, we study tolerance of semantic faults, one of the crucial Issues In the Simplex(TM) architecture. In particular, we examine semantic faults that cause the controlled device to be unsafe (i.e., unable to carry out its normal operation) and eventually cause the device to become damaged. We also consider fault detection as a safety check. For the class of control systems operating around an equilibrium, the objective of maintaining the safety of the controlled device is formulated as a stabilization problem, and the safety of the controlled device is tested against the stability region of the device under the safety control. To establish the stability region, we apply the Lyapunov stability theory and linear matrix inequality (LMI) methodologies. It is shown that the stability region for a given safety controller as well as a safety control law can be systematically derived by LMI based approaches. We conclude the report with a summary of the procedure for deriving the safety check and safety controller for a given application. This paper provides a framework to automatically generate a hybrid controller that guarantees that the robot can achieve its task when a robot model, a class of admissible environments, and a high-level task or behavior for the robot are provided. The desired task specifications, which are expressed in a fragment of linear temporal logic (LTL), can capture complex robot behaviors such as search and rescue, coverage, and collision avoidance. In addition, our framework explicitly captures sensor specifications that depend on the environment with which the robot is interacting, which results in a novel paradigm for sensor-based temporal-logic-motion planning. As one robot is part of the environment of another robot, our sensor-based framework very naturally captures multirobot specifications in a decentralized manner. Our computational approach is based on first creating discrete controllers satisfying specific LTL formulas. If feasible, the discrete controller is then used to guide the sensor-based composition of continuous controllers, which results in a hybrid controller satisfying the high-level specification but only if the environment is admissible. Formal verification of a control system can be performed by checking if a model of its dynamical behavior conforms to temporal requirements. Unfortunately, adoption of formal verification in an industrial setting is a formidable challenge as design requirements are often vague, nonmodular, evolving, or sometimes simply unknown. We propose a framework to mine requirements from a closed-loop model of an industrial-scale control system, such as one specified in Simulink. The input to our algorithm is a requirement template expressed in parametric signal temporal logic: a logical formula in which concrete signal or time values are replaced with parameters. Given a set of simulation traces of the model, our method infers values for the template parameters to obtain the strongest candidate requirement satisfied by the traces. It then tries to falsify the candidate requirement using a falsification tool. If a counterexample is found, it is added to the existing set of traces and these steps are repeated; otherwise, it terminates with the synthesized requirement. Requirement mining has several usage scenarios: mined requirements can be used to formally validate future modifications of the model, they can be used to gain better understanding of legacy models or code, and can also help enhancing the process of bug finding through simulations. We demonstrate the scalability and utility of our technique on three complex case studies in the domain of automotive powertrain systems: a simple automatic transmission controller, an air-fuel controller with a mean-value model of the engine dynamics, and an industrial-size prototype airpath controller for a diesel engine. We include results on a bug found in the prototype controller by our method.