Extracting Hybrid Automata from Control Code

Abstract

Formal methods—and abstract interpretation in particular—can assist in the development of correct control code. However, current approaches to deploying formal methods do not always match the way practicing engineers develop real control code. Engineers tend to think in code first—not formal models. Standard practice is for engineers to develop their control code and then build a model like a hybrid automaton from which to verify properties. Since the construction of this model is manual, it leaves open the possibility of error. Existing formal approaches, on the other hand, tend to focus on synthesizing control code from a verified formal model. We propose a method for synthesizing a hybrid automaton from the control code directly. Specifically, we use abstract interpretation to create an abstract state transition system, and from this we systematically extract a hybrid automaton. Not only does this eliminate the introduction of error into the model based on the code, it fits with common practice in engineering cyberphysical systems. We test the technique on a couple examples—control code for a thermostat and a nuclear reactor. We then pass the generated automata to the HyTech model-checker to verify safety and liveness properties.