Beyond Model Checking: Parameters Everywhere
Étienne André, Benoît Delahaye, Peter Habermehl, Claude Jard, Didier Lime, Laure Petrucci, Olivier Henri Roux, Tayssir Touili · 2014
Beyond Model Checking. . . After many years of academic research on model checking, its impact in industry is mostly limited to critical embedded systems, and thus is somewhat disappointing w.r.t. the expectations. Two major reasons are the binary response to properties satisfaction, which is not informative enough, and the insufficient abstraction to cater for tuning and scalability of systems. A major challenge is to overcome these limitations by providing parametric formal methods for the verification and automated analysis of systems behaviour. . . . are Parameters The challenge is clearly to obtain guarantees on the quality of the systems in operation, quality being evaluated during the design phase. For any given level of abstraction, we want to maintain the formal description of the behaviour of the system together with its expected properties. The current verification techniques ensure that the properties are true for all possible behaviours of a given instance and environment of the system. Hence the utmost importance of a characterisation of the conditions under which the properties are guaranteed to hold, in particular since systems are often incompletely specified or with an environment unknown a priori. In order to broaden the applicability of formal modelling methods within the wide range of digital world that is being built, a key point is the control of abstraction in the models. A main challenge is to develop the theory and implementation of the verification of parametrised models. This area of research is still in its infancy and a significant advance should be performed, by a coordinated study of several types of parameters: discrete (e.g. number of threads, size of counters), timed (deadlines, periods), continuous costs (energy, memory), and probabilistic (redundancy, reliability). Being able to treat these parametrised models constitutes a scientific breakthrough in two ways: