Simulation-based Testing and Validation of MBD Systems
Università di Udine
Model-based development (MBD) is a design approach where diagrams are used instead of code. MBD significantly simplifies the design process, but the verification and debug of models remains a challenging task. Simulink from MathWorks is an MBD tool for systems design and simulation that has become a de facto standard in automotive industry. Its lack of a formal semantics makes it difficult, if not impossible, to check whether a model satisfies a specification. In this talk we will consider the following problem: given a Simulink model, an input space, and a property expressed in terms of a Signal Temporal Logic (STL) formula, find a sequence of input under which the model does not satisfy the property. We propose a simulation based technique inspired by the Rapidly Exploring Random Tree algorithm (RRT) originally created for robot path planning. In our context we try to generate traces that maximize the coverage of the state space of the model and possibly falsify the formula. Experimental results obtained by applying our technique to industrial automotive models are encouraging. This work has been done in collaboration with the Toyota Model-Based Development research group in Los Angeles, California.
Join work with: T. Dang (Verimag), A. Donzé (Berkeley), J. V. Deshmukh, X. Jin, J. Kapinski (Toyota Technical Center)