Presenter
Richárd Szabó
BME, Budapest
Authors
Richárd Szabó
Abstract
The formal verification of safety-critical systems requires not only a model of the system under design but also a set of environmental assumptions, i.e., a description of what the environment of the system can and cannot do. In engineering practice, however, these assumptions typically remain implicit "mental" models of the engineers, and as a result, model checking an otherwise correct design against an unconstrained environment often yields violation traces that are deemed unrealistic by engineers. Making these assumptions explicit is therefore an essential part of the verification process, which is usually done by manually creating environment models.
Our approach builds on the coordination automata formalism, which describes the scheduling and the interaction of the components of a distributed system. In addition, the coordination automata can also express what is assumed of the environment and what is asserted of the executed component at each step, which makes modeling environmental assumptions possible. However, it remains the task of the engineer to formulate these assumptions, which is a challenging problem in itself: an assumption that is too strong potentially hides the very failures the system is designed to tolerate, whereas one that is too weak may not be sufficient to guarantee the assertion.
In this talk, we present a symbolic adaptation of the environment assumption synthesis of Chatterjee, Henzinger and Jobstmann (CONCUR 2008) for synthesizing parts of the environment model from LTL formulas describing what is assumed of the environment and asserted from the executed component. We demonstrate the applicability of our approach on the Road Wheel Actuator (RWA) of a steer-by-wire system.
Slides
TBA