Invited Talks
Design of complex cyber-physical systems such as automobiles, airplanes, and satellites is a multifaceted task. Model-based design (MBD) has gained much popularity by providing visual abstractions for controller design and useful functionalities such as automatic synthesis of high quality embedded code. In model-based design environments, models serve the same purpose as C/ C++ code has served in the past. With numerical simulations and formal analysis techniques based on simulation, MBD tools such as Simulink and Stateflow provide valuable early verification, leading to their widespread use in the embedded systems industry. While simulation remains a useful tool, formal verification techniques have shown their advantage in their exhaustive nature and the soundness of the results they produce. In this talk we will discuss Simulink Design Verifier, a formal verification tool seamlessly integrated with the Simuilnk/Stateflow modeling environment. We will first discuss the design principle of Simulink Design Verifier and present a few workflows for using formal verification in numerical simulation software. Then we will take some time to explore several different workflows for using Simulink Design Verifier: design error detection for common misuses and runtime exceptions, test generation for design understanding, and property proving for guaranteeing correctness of safety properties. We will also discuss the formal verification technologies used by Simulink Design Verifier and how they are integrated to provide a fully automated verification tool. The talk will conclude with a few remarks on future investments based on feedback from lead industry adopters of formal verification tools.
Out-of-bounds array accesses, also known as buffer overflows, account for nearly 50% of all software vulnerabilities reported by CERT and constitute a major source of non-determinism in embedded programs. This class of errors is extremely difficult to eliminate by standard testing procedures because of its near total absence of effects on the observable behavior of programs. It is an ideal target for static analysis and, since pointer arithmetic is prevalent in C programs, numerical domains have a major role to play. In this talk, we will present the lessons and learning from a decade of work trying to effectively carry out static array-bound checking on real C code, from the mission control software of Mars Exploration Rovers to OpenSSH to auto-coded flight controllers. We will describe our efforts trying to push the scalability limits of convex polyhedra or use numerical domains that are unable to express theproperties needed when applied out of the box. Despite the number of numerical domains available in the literature, we had to devise a new abstraction forlinear inequalities, the gauge domain, which offers a better trade-off among expressiveness, accuracy and scalability for the purposes of array-bound checking. The story doesn't end here though and there is still plenty of research lying ahead before practical solutions for real-size programs emerge.
Numerical software that controls a physical plant can not be analyzed in isolation.
It has to be verified within the larger context in which it is used.
Hybrid systems allow modeling and analysis of the composition of the numerical software component and the physical plant model.
The safety verification problem for hybrid systems asks if a hybrid system can ever reach an undesirable state.
There are at least three different approaches that have been studied for solving this problem: (a) reach set computation by applying abstract interpretation on the hybrid dynamics (b) abstraction of the hybrid system and model checking the abstract system (c) direct proof of safety by demonstrating existence of an inductive invariant.
In this talk, we will briefly describe the different verification approaches, and then describe in detail the verification techniques underlying the HybridSal verification tool.
HybridSal can be used to verify continuous-time, as well as, sampled control systems.
We will also discuss extension of the verification techniques to synthesis for hybrid systems.
Formal verification of hybrid systems is a long-standing difficult problem. To begin with, reachability analysis is undecidable for most relevant continuous dynamics so that only approximate methods can be used. Departing from the dominant approach based on sophisticated set integration methods, the toolbox Breach was initially implemented to investigate a most naive idea, dubbed Barbaric reachability by one of its authors, to infer reachable sets from sets of "simple" simulations. Over time, the method grew more civilized by the use of sensitivity analysis to estimate reachable tubes around trajectories, and more recently by the support of formal specifications beyond simple reachability properties. These specifications are expressed in Signal Temporal Logics (STL), a logic adapted to write properties constraining real-valued, dense-time signals. In Breach, STL formulas are interpreted (monitored) with a quantitative, or robust, semantics which provides a numerical margin by which a simulation trace satisfies or violates it. This satisfaction degree can be used to get confidence that a property is verified despite numerical error in the computation of a trace but also as a valuable information to characterize the behaviors of the system. By combining this information with different parameters exploration strategies, we get an efficient methodology to investigate which properties are satisfied by a model (specification mining), how robustly these properties are satisfied and how to find parameters values which guarantee a robust satisfaction. I will describe this methodology and the Breach toolbox, along with different application examples, including a large-scale Simulink model from the automative industry and complex nonlinear models from systems biology.