Hybrid systems tightly integrate software-based discrete control systems and continuous physical phenomena. Better methods and tools for design, modeling, and analysis are necessary as these systems become more complex, powerful, and prevalent in our daily life. There are two main approaches to model hybrid systems. One is to discretize them into fully discrete systems. We focus on two discrete models: a network of communicating FSMs (NCFSM) and event-condition-action (ECA) rules. In this dissertation, we make several contributions to verifying discrete systems. First, for an NCFSM, we symbolically encode and verify the properties of livelocks, strong connectedness, and dead transitions. We also design a symbolic equivalence checker to automatically generate test cases for fault-based testing. Second, for ECA rules, we verify both termination and confluence properties and then provide the first practical experimental results for the confluence property.
The second modeling method is to keep the continuous dynamics by using hybrid automata or block diagrams. Most verification problems for hybrid automata are undecidable even under severe limitations. However, using block diagrams, such as Simulink, researchers model a hybrid system as an input-output signals mapping box. This approach has been widely adopted by industry due to its scalability. Combining simulation and temporal logic, the validation technique is able to check whether the temporal behavior of the system meets a set of requirements. One significant challenge to the formal validation is that system requirements are often imprecise, non-modular, evolving, or even simply unknown. In this dissertation, we make the following contributions to tackle the requirement defects. First, we compare the performance of the two existing falsification engines. Second, we design a requirement mining framework, an instance of counterexample-guided inductive synthesis, which is able to mine formal requirements from a closed-loop model. Third, we observe the importance of the monotonicity of formulas for synthesis and use a satisfiability modulo theories (SMT) solver to prove this property. Fourth, we propose weighted temporal logics to improve the performance of this mining framework. This framework has the following two applications: mined requirements can be used to validate future modifications of the model and enhance understanding of legacy models; the framework can also guide the process of bug-finding through simulations. We present two case studies for requirement mining: a simple automobile transmission controller and an industrial airpath control engine.
