Online Execution Control Checking for Autonomous Systems
Félix Ingrand, Frédéric Py · 2002
This paper presents some recents developments of the LAAS architecture for autonomous systems. In particular, we clarify and specify the role of the Execution Control level of our architecture. This level has a fault protection role with respect to the command issued by the decisional level, which are transmitted to the real system (through the functional level). To implement this Execution Control level, we propose an approach and a tool inspired from the model checking domain. We present a new language, used to specify the model of acceptable and required states of the system (valid contexts for requests to functional module and resources usage). The model written in this language is then compiled in an OBDD (Ordered Binary Decision Diagram) like structure which is used online to check in real-time the constraints and the rules specified. Such model checking approach, used in a synchronous context, provides critical dependable properties. Moreover, these approaches can be further used to check off line more complex temporal properties of the system.