Abstract— This paper presents some recent developments of the LAAS architecture for autonomous mobile robots. In particular, we specify the role of the Execution Control level of this architecture. This level has a fault protection role with respect to the commands issued by the decisional level, which are transmitted to the real system (through the functional level). We introduce a new approach and a new tool inspired from the model checking domain. We present a new language to specify the model of acceptable and required states of the system (valid contexts for requests to functional module and resources usage). This language is compiled in an OBDD (Ordered Binary Decision Diagram) like structure which is then used online to check the specified constraints in real-time. Such model checking approach could be extended to check off line more complex temporal properties of the system.