Over the past few decades, computers have transformed from special-purpose and standalone number-crunching processors to networked devices interacting with the physical world. Realizing the full potential of such cyber-physical systems requires that advances in processing and communication technology are matched by advances in tools for designing such systems in a cost-effective manner. Indeed, none of us would be willing to drive an autonomous car, or use a pacemaker that can be remotely programmed by our physician, if we are not guaranteed safety under all conceivable conditions. The current practice in system design relies primarily on simulation that ensures the system works as intended only on a few scenarios selected by the design team. Formal verification, on the other hand, promises to catch bugs in corner cases by exploring the space of all possible executions of the system.
The verification problem is inherently computationally intractable, and yet researchers have made steady progress in developing methodology, algorithms, and tools for the verification of hardware and software systems. In particular, model checking—a technique for symbolically exploring the space of all reachable states of a system model—is considered a success story for theory in practice, due its adoption in checking correctness of multiprocessor designs and device driver code. In these applications, the model is purely discrete. To analyze a cyber-physical system such as a pacemaker, we need to consider the discrete software controller interacting with the physical world, which is typically modeled by differential equations. Developing effective symbolic verification technology for such mixed discrete-analog models—also called hybrid systems—has proved to be a challenging problem, attracting a lot of research both in formal methods and in control theory communities in recent years. The following paper by Althoff et al. reports a major milestone in this quest.
Since formal verification techniques have high computational costs, they need to be applied with a scalpel rather than with a hammer. The authors show great prudence in choosing their target. The design of charge-pump phase-locked loops is representative of both the technical challenges involved in the verification of hybrid systems, and of potential benefits of formal analysis. While the design has clearly specified requirements for stability and settling time, the discrete switching in the model implies that classical control-theoretic methods cannot ensure these analytically. The variations in initial conditions and parameter choices make it an ideal target for symbolic methods.
The experimental results reported in the following paper are truly significant since the authors demonstrate their method of symbolic simulation is competitive with the industry-standard simulation tools in terms of computational requirements.
Symbolic computation of reachable states of a hybrid system requires choosing a representation for sets of system states so the result of applying a single simulation step can be computed efficiently over this representation. Moreover, the complexity of the representation should grow manageably with the number of simulation steps. The technical strength of the paper is in the finely crafted combination of techniques the authors use to implement this symbolic computation. A key novelty of their method involves over-approximating the result of each simulation step by computing bounds on the range of switching times. This new method is critical in maintaining the simplicity of the symbolic representation across simulation steps, and allows the search to progress deep enough to establish stability.
The experimental results reported in the following paper are truly significant since the authors demonstrate their method of symbolic simulation is competitive with the industry-standard simulation tools in terms of computational requirements. This demonstration of cost-effectiveness is hopefully the key to convince commercial vendors such as Mathworks to invest seriously to explore the transition of verification technology for hybrid systems to industrial practice.
Join the Discussion (0)
Become a Member or Sign In to Post a Comment