PRECISE Seminar: Making Formal Methods Work in Industrial Practice

Industrial-scale embedded control systems are often developed in the model-based development (MBD) paradigm. The design process typically involves capturing a 'plant model' to describe the physical processes to be controlled, and a 'controller model,' which is usually a block-diagram-based representation of the controller software. In practice, plant models and controller models are highly complex; typical plant models feature highly nonlinear and hybrid differential and algebraic equations, while controller models feature large look-up tables storing pre-computed values, several levels of design-hierarchy, and design-blocks scheduled at different rates. Design validation in the industry involves thorough testing on platforms such in-vehicle testing, hardware-in-the-loop simulations, and software/model-in-the-loop simulations. The Simulink modeling framework (from the MathWorks), which is the de facto standard across the industry for describing closed-loop plant + controller models, offers a high-fidelity simulation tool routinely used by designers for validation. The current situation has led to two disparate communities: the industrial community with access to scalable methods to perform extensive (but not exhaustive) simulations of a system, and an academic research community that has focused on developing formal techniques that provide exhaustive but conservative results. We consider the question: 'What can we "formally" accomplish if all we have is the ability to simulate a system?'  As a tentative answer to this question, we suggest the paradigm of Simulation-guided Formal Analysis, and present some recent work that we have done within this framework.