D’une approche modulaire à une approche orientée

composant pour le développement de systèmes

autonomes : Défis et principes
Matthieu Gallien† , Fahmi Gargouri† , Imen Kahloul∗ , Moez Krichen∗ , Thanh-Hung Nguyen†
Saddek Bensalem† , Félix Ingrand∗
∗ LAAS/CNRS, Université Toulouse
† Verimag Laboratory, Université Grenoble I, CNRS

Abstract— Les systèmes autonomes sont des systèmes com- garantir des propriétés essentielles (temporelles et de sûreté).
plexes qui reposent sur la coopération/interaction entre différents Pour faire face à la complexité de cette tâche, ces tech-
composants logiciels. Ces logiciels sont de types assez variés, avec niques sont appliquées à une description orientée composant
des contraintes de fonctionnement temporelles assez diverses.
L’ensemble doit cependant respecter les spécifications du concep- du système dont les propriétés globales sont satisfaites par
teur et garantir des contraintes de sûreté. Pour y parvenir, nous construction ou peuvent être déduites des propriétés de ses
proposons l’utilisation d’une approche orientée composants basée composants. De surcroı̂t, la description componentisée fournit
sur l’outil BIP, pour, dans un premier temps, le développement de une base pour la reconfiguration et l’évolutivité.
la couche fonctionnelle de systèmes autonomes (robots, satellites, Dans cet article, nous proposons l’utilisation d’une ap-
etc.), et plus tard, envisager d’étendre cette méthodologie vers
la couche décisionnelle. Cette approche vient naturellement proche orientée composants basée sur l’outil BIP [2], pour
compléter l’approche modulaire de GenoM jusqu’alors utilisée le développement de la couche fonctionnelle de systèmes
pour développer la couche fonctionnelle de l’architecture LAAS. autonomes (robots, satellites, etc.) en prenant comme exemple
Elle permet de mettre en place des systèmes robustes et sûrs en la couche fonctionnelle de l’architecture du LAAS[1]. Au delà
produisant un contrôleur d’exécution correct par construction, et de cette première étape, nous envisageons de propager cette
en fournissant un modèle formel qui peut être utilisé avec divers
outils de vérification et de validation. méthodologie vers la couche décisionnelle.
Cette approche vient naturellement compléter l’approche
I. I NTRODUCTION modulaire de GenoM jusqu’alors utilisée pour développer la
L’ingénierie système repose sur l’idée qu’un système com- couche fonctionnelle de l’architecture LAAS. Elle permet de
plexe est construit en assemblant des composants. D’où le mettre en place des systèmes robustes et sûrs en produisant
principe de la conception orientée composant qui prévoit que un contrôleur d’exécution correct par construction, et en
les grands systèmes sont conçus à partir de systèmes plus fournissant un model formel qui peut être utilisé avec divers
simples. Cette approche confère, entre autres, des avantages outils de vérification et de validation.
de réutilisation, d’analyse et validation modulaires, reconfigu- Dans la suite, nous allons commencer par une présentation
rabilité, contrôlabilité, etc. sommaire de l’architecture robotique déployée au LAAS (dans
Les systèmes autonomes sont des systèmes complexes qui la Section II) et de l’outil de développement de systèmes temps
reposent sur la coopération/interaction entre différents compo- réel BIP conçu à VERIMAG (dans la Section III). Ensuite,
sants logiciels. Ces logiciels sont de types assez variés, avec nous allons présenter le principe d’intégration GenoM / BIP
des contraintes de fonctionnement temporelles assez diverses. qui fera l’objet de la Section IV, et enfin, vérifier ces résultats
L’ensemble doit cependant respecter les spécifications du dans la Section V.
concepteur et garantir des contraintes de sûreté.
II. L’A RCHITECTURE DU LAAS
Une des principales limites de l’état de l’art actuel est
l’absence d’un paradigme (modèle) unifié pour la description A. Présentation
et l’analyse des flux d’information entre les composants. Un Une architecture spécialement dédiée au développement de
tel paradigme permettrait aux concepteurs et développeurs systèmes pour robots autonomes a été développée au LAAS. Il
système de formuler des solutions basées sur des concepts s’agit d’une architecture générale (cf. Figure 1) permettant de
tangibles, bien fondés et organisés plutôt que d’utiliser des décomposer un système en trois niveaux ayant des propriétés
mécanismes de coordination dispersés tels que les sémaphores, temporelles et des représentations différentes. Ces niveaux sont
les moniteurs, l’envoi de messages, les appels à distance, les organisés comme suit :
protocoles, etc. Le niveau décisionnel : À ce niveau, sont déployés des
Les concepteurs de systèmes complexes, tels que les robots outils de supervision, en l’occurrence open-PRS [7], et de
autonomes, ont besoin de techniques d’analyse évolutives pour planification, comme le planificateur symbolique IXTET
 Decisionnal level fonctionnalité en question du robot. Chaque module propose
Procedural Planner and un ensemble de services actionnables par une requête client
executive temporal executive
(open-PRS) (IxTeT) (ordre émanent de la couche décisionnelle).

Execution control level

Request
Execution controller (R2C)
Services Interface
Functionnal level Report

Antenna control
NDD Speed Control Task
poster

Platine

Posters interface
Aspect Obs
Functional
Control IDS
Science IDS

Laser
Camera Im. RFLEX Pos Scan
RF Execution Tasks
functional
poster

activities

Simulator
GAZEBO Fig. 2. Schéma générique d’un module GenoM.

OR Cette dernière sera interceptée par la tâche de contrôle qui,

selon le type de requête, va effectuer une lecture écriture
de données stockées en interne, ou lancer une activité dans
Module Pos
X Functional Module Y Poster la tâche d’exécution correspondante. Une tâche d’exécution
contient une ou plusieurs activités, dont une activité perma-
nente qui s’exécute pendant toute la durée de vie du module.
Fig. 1. Instance de l’architecture LAAS pour le robot DALA. Elle est particulièrement utile pour les modules qui veulent
toujours faire un traitement au début de chaque cycle de
la tâche d’exécution avant de passer aux autres activités à
qui inclut depuis [8] le contrôle temporel de l’exécution exécuter.
de plan. Ces composants permettent de produire un plan Figure 3 décrit le comportement d’une activité inspiré du
d’action et d’en superviser l’exécution tout en restant cycle de vie d’un thread. Initialement dans l’état ETHER,
réceptifs et réactifs aux événements émanants de la indiquant ainsi une absence d’activité du service, l’automate
couche inférieure. passe à l’état START à la réception de la requête (avec
Le niveau fonctionnel : Inclut les fonctions sensorimo- la transition "request" ). Si aucune incompatibilité ou
trices, les fonctions de traitement ainsi que les boucles problème de paramétrage ne sont notés, l’automate démarre
de contrôle du robot. Chacune d’elles étant encapsulées l’exécution du codel relatif à l’activité en passant à l’état
dans un module contrôlable et communicatif généré par EXEC ("started" ), état pendant lequel il alterne avec
GenoM (pour générateur de modules) [5]. Chaque module l’état interne IDLE afin de permettre l’exécution des autres
offre des services activables via des requêtes par la activités de la tâche d’exécution.
couche décisionnelle et utilise des posters pour stocker Si, lors de sa fin nominale, l’activité s’exécute correcte-
les données produites à l’usage des autres modules ou de ment, elle bascule dans l’état END avec envoi du bilan de
la couche décisionnelle. succès ("OK" ). Sinon, en cas de problème détecté pendant
Le contrôle d’exécution : Représente l’interface entre les l’exécution, l’activité bascule de l’état EXEC à l’état FAIL
deux niveaux précédents. Il s’assure du respect des en libérant les ressources, accompagné d’un bilan expliquant
contraintes de sûreté en garantissant la cohérence du les causes du problème. Il est aussi possible que l’activité soit
système. Dans les dernières années, le contrôleur utilisé interrompue à tout moment (sous demande explicite du client
était le R2C [9]. Il est à noter que ce contrôleur garantit ou lors du lancement d’un service incompatible), auquel cas,
la bonne exécution des services des modules fonctionnels l’automate bascule dans l’état INTER, libère les ressources et
et l’interaction entre ces derniers, mais n’assure en aucun envoie un bilan final d’interruption ("interrupted" ).
cas le contrôle d’exécution interne du module lui même. Dans ces trois cas de fin d’activité ( succès, échec ou
interruption), l’automate retourne ensuite à l’état ETHER.
B. GenoM Il est à noter que, dans l’automate : schéma générique d’une
Tous les modules GenoM sont construits selon un modèle activité, le contrôle (effectué par une tierce entité) intervient
générique, décrit dans Figure 2, qui sera instancié selon la à différents moments. Par exemple, lors du lancement (de
ETHER à START) ou lors de l’interruption (de EXEC à Ce découpage(séparation) confère l’avantage de séparation
INTER). Ce chevauchement peut prêter à confusion. Dans cet entre le comportement proprement dit du composant, et la
article, nous proposons de séparer, à partir du niveau le plus fin structure globale du système.
(à savoir le service d’un module), le contrôle de l’exécution. L’idée de base de BIP est qu’un système complexe n’est autre
Ce fera l’objet de la Section IV-A. que la composition de sous-systèmes plus simples. Dans ce
même ordre d’idées, BIP permet la composition hiérarchisée
START
des composants, et ce en partant des composants dits ato-
request(arg)/_ _/started miques qu’on assemble par des connecteurs et des priorités
abort/_
sur ces derniers.
Les éléments de base de BIP relatifs aux différentes couches
_/failed
ETHER FAIL EXEC IDLE précédemment évoquées sont les suivants :
_/interrupted abort/_
A. Composant atomique et “Behavior”
INTER
_/OK(ret)

abort/_
Un composant atomique (exemple : Figure 4) contient un
events :
input / output ensemble d’états de contrôle et des transitions entre eux. Ces
END
dernières définissent le comportement du composant et sont
Fig. 3. Execution automaton of an activity.
franchissables par des ports utilisés pour la synchronisation in-
ter composants. Il est possible de définir une garde (condition)
1) Exemple illustratif de couche fonctionnelle: La sur la transition ( x>0 dans l’exemple) ainsi qu’un traitement
méthodologie GenoM veut que chaque fonctionnalité du (du code C/C++ comme y := f(x)) à faire si la transition est
robot soit encapsulée dans un module. Toutefois, certaines franchie.
fonctionnalités, telle la navigation, sont assez complexes au
point d’être assurées par un ensemble de modules.
%&'#($
Comme exemple d’exécution, nous nous somme intéressés à
DALA, un iRobot ATRV, et plus précisément aux modules
$$+,$
impliqués dans la navigation tel qu’illustré plus haut dans

!"#$
+,$ !"#$
Figure 1. -./01$
Le module sick : Il s’agit du module qui gère le capteur (23)405$
laser. Il produit entre autres des mesures cartésiennes
relatives au repère du robot ou au repère d’origine cor-
respondant aux segments perçus. )"**$
Le module aspect : Il utilise le poster de sick pour dresser
une carte des obstacles avoisinant le robot.
Fig. 4. Exemple de composant atomique
Le module ndd : Ce module se charge d’assurer la naviga-
tion en évitant les obstacles pour atteindre une position
but. Pour ce faire, il récupère la position actuelle dans
B. Connecteurs et “Interaction”
le poster Pos de pom ainsi que la carte d’obstacle le
poster Obs d’aspect . En sortie, il fournit le poster Speed Si l’on considère les composants (atomiques ou composés)
contenant une consigne en vitesse. comme des blocs, les connecteurs permettent de les assembler
Le module rflex : C’est le module qui assure la locomotion afin d’obtenir un système entier. Un connecteur est un en-
du robot en asservissant les roues sur la consigne en vi- semble de ports des composants pouvant interagir. Une interac-
tesse produite par ndd . En sortie, il donne une indication tion (d’un connecteur) est, quant à elle, un sous ensemble des
de position relative au déplacement du robot (position ports de ce premier. On peut la considérer comme une instance
odométrique améliorée par la mesure du gyroscope). du connecteur. Un mécanisme de typage des ports est utilisé
essentiellement pour distinguer deux types de synchronisation
III. L’ OUTIL DE VERIMAG : BIP comme illustré dans Figure 5. À savoir, la synchronisation
BIP [2] (Behavior, Interaction and Priorities) est une plate- forte dite rendez-vous (cf. Figure 5-a), et la synchronisation
forme logicielle pour la modélisation de composants temps faible dite broadcast (cf. Figure 5-b) identifiée par un triangle
réel hétérogènes. BIP considère le modèle d’un compo- sur le port complet.
sant comme une superposition de trois couches. La couche
inférieure modélise le comportement (B pour behavior) du C. Politique d’ordonnancement et “Priority”
composant sous forme d’un ensemble de transitions. Au Dans le cas où, sur un port, plusieurs connecteurs sont
dessus, s’ajoute la description des interactions (I) entre ces définis et qu’il se trouve que plus qu’une interaction est
transitions via des connecteurs. Enfin, la couche supérieure possible, ce conflit est traité par la définition de priorités
correspond à un ensemble de règles de priorités (P) traduisant affectées aux connecteurs. Ainsi, il est possible de filtrer les
la politique d’ordonnancement des interactions. interactions à exécuter parmi celles possibles.
 !"# !%# !'# !"# !%# !'# contrôle, de l’exécution en les gérant dans des sous com-
posants séparés (cf Figure 7) appelés respectivement Service
$"# &"# &%# $"# &"# &%# Controler (à gauche de la figure) et Activity (à sa droite).
Nous avons essayé de faire en sorte que le modèle BIP de
service soit le plus fidèle possible à l’automate générique de
(#)#*+,-+./0123# 4#/#561(-7(3!# GenoM. Cette démarche de dissociation nous permet d’appli-
quer la nouvelle structure et la lier à celle de GenoM, entre
Fig. 5. les connecteurs et les deux types de synchronisations. autres, via les bibliothèques de codels existants (cf. II-B).
Il est à noter que les transitions ”control”, ”error”, ”start”,
”end”, ”fail” et ”inter” du Service Controler s’accompagnent
IV. I NT ÉGRATION GenoM / BIP d’une modification de la variable interne ”status” et d’infor-
mations sur l’état d’exécution de l’activité.
A. Componentisation de la partie générique et structurelle
d’un module GenoM 27831# 134@@63# @61(121?0# 01231# 65;# <24=# 45163# 6:6>#

Nous avons vu, dans la Section II-B, que la couche fonc- >85138=# 27831# 134@@63# @61(121?0# 01231# 65;# <24=# 45163# 6:6>#
0121?0#
tionnelle de l’architecture du LAAS respecte une approche @61(121?0# 63383# @61(121?0# >85138=#
01231# 6:6>#
modulaire telle qu’un module correspond au schéma générique 134@@63#
01231# 01231#
$%&$'# (%)'%# 65;# 65;# 65;#
décrit dans Figure 2. Dans cette approche de componenti- $%&$'# (.$$/#
!"## <24=# <24=#
sation, nous présentons dans Figure 6 le modèle BIP d’un <24=# $0121?0%&'&()# !"#<24=#
45163# 01231# 45163# 45163#
module GenoM, suivant ce formalisme de décomposition de la 65;# 45163# 2783196:#
2783196:# 2783196:# )*+'%#
couche fonctionnelle : )*+'%# 27831# $,$-#

@61(121?0#
Functional level : := (Module)+ 2783196:#
@61(121?0#
Module : := (Service)+ . (Execution Task)+ . (Pos-
ter)+
Service : := (Service Controler) . (Activity) Fig. 7. Modèle BIP d’un service GenoM.
Execution Task : := (Timer)+ . (Scheduler Activity)
Où le ”+” veut dire que le composant contient au moins
une sinon plusieurs occurrences du sous-composant, et le ”.” B. Componentisation de NDD
traduit la composition de plusieurs sous-composants. Nous avons modélisé en BIP le module ndd responsable
Par ailleurs, le Scheduleur Activity va ordonnancer le lan- de la navigation. Comme le montre Figure 8, il contient
cement des Activities des services relatifs à la task Execution une tâche d’exécution qui gère cinq services dont un ser-
en question. Dans un service, nous avons voulu séparer le vice Permanent et des posters (représentés par un composant
générique poster). La tâche d’exécution (cf Figure 9) se
réveille périodiquement synchronisée par un sous composant
Timer. À chaque période, elle déclenche le service Permanent
!"#$%&"'()*+#),"#' !"#$%&"'()*+#),"#' et elle permet aux services de s’exécuter grâce à leurs inter-
actions.
Grâce au formalisme BIP, il est possible de modéliser
-&.$%+/' -&.$%+/' des relations assez complexes à définir. À titre d’exemple,
le déclenchement du service Stop provoque l’interruption du
!"#$%&"' !"#$%&"'
déplacement qui se traduit par le "abort" du service
GoTo si ce dernier est en court d’exécution. Cette opération
0)1+"#' correspond à connecteur de type broadcast entre la tâche
5%8"#' !&9":4,"#'-&.$%+/' d’exécution et le port (notation port :service) trigger :Stop,
23"&4.)*'5617' et un autre connecteur de type broadcast entre ce premier
0)1+"#' connecteur et le port abort :Goto.
Par ailleurs, une autre propriété doit toujours être vérifiée, à
5%8"#' !&9":4,"#'-&.$%+/' savoir qu’un déplacement ne doit se faire que s’il est précédé
0)1+"#' par un SetParams et un SetSpeed qui initialisent cor-
23"&4.)*'5617'
rectement le module, d’où le connecteur entre trigger :GoTo,
getStatus :SetParams et getStatus :SetSpeed.
À partir de ce modèle, la chaı̂ne d’outil de BIP génère le
code que ”BIP Engine” pourra exécuter. Ce code contient des
appels aux codels contenus dans des bibliothèques initialement
Fig. 6. La componentisation d’un module GenoM développées pour GenoM afin d’exécuter les activités du robot.
 SetParams Init SetSpeed GoTo Stop
NDD

trigger getStatus abort trigger getStatus abort

SetParams SetSpeed
trigger getStatus abort
start exec end fail inter start exec end fail inter
Stop
start exec end fail inter

trigger getStatus abort

Init
start exec end fail inter

trigger getStatus abort

a b c d GoTo
e
Execution Task start exec end fail inter
f
g

write trigger getStatus abort

Poster Permanent
read start exec end fail inter

Poster

Fig. 8. Modèle BIP de ndd .

a b c d
Control Task
!"#$%&'()*+,-)
e
a b c d
trigger
a b e

trigger c
f
f

trigger d
g
g g
f e
Timer

Fig. 9. Modèle BIP de l’Execution Task.

Le code généré pour ndd a été intégré et exécuté dans l’envi- à utiliser les invariants générés automatiquement pour prouver
ronnement du robot DALA du LAAS. Il convient de souligner la non-satisfiabilité des prédicats caractérisant les blocages
que cette simulation, ayant pour particularité l’hétérogénéité de globaux. Deux types d’invariants sont générés : (i) Les inva-
la couche fonctionnelle (des modules GenoM et BIP), met en riants de composants qui sur-approximent l’ensemble d’états
évidence la compatibilité GenoM/BIP ainsi que la compatibilité atteignables de ces derniers, et (ii) les invariants d’interaction
module BIP/couche décisionnelle. Cela renforce l’objectif de qui sont les contraintes sur les états des composants liées aux
l’approche qui cherche s’adjoindre et compléter l’approche interactions.
GenoM. Les invariants d’interaction sont obtenus par le calcul des
“traps”, des abstractions des états finis du système vérifié. La
V. V ÉRIFICATION méthode est implémentée dans l’outil D-Finder[3], qui prend
Les Outils de BIP, ainsi que d’autres outils de vérification comme entrées des programmes BIP et applique les stratégies
génériques, permettent, outre l’exploration exhaustive de l’es- prouvées pour éliminer des blocages potentiels par calcul
pace des états du système, la détection des deadlocks potentiels d’invariants de plus en plus forts. Au cour de la vérification du
et la vérification de certaines propriétés dans le modèle du système modélisé par cet outil, aucun blocage n’a été trouvé,
robot. d’où ce système est deadlock-free.

A. Absence de blocage (Deadlock freedom) B. Propriétés de sûreté

Il s’agit d’une propriété d’exactitude essentielle car elle Une propriété de sûreté garantit qu’un événement non
caractérise la capacité du système à exécuter certaines activités prévu n’aura jamais lieu. Pour ce faire, nous utilisons des
au cours de sa durée de vie. Les outils de BIP permettent méthodes basées sur “le model checking”. Ce dernier consiste
la détection de blocages potentiels par analyse statique des à construire un modèle fini du système analysé et à vérifier les
connecteurs dans le modèle BIP [6]. Cette méthode consiste propriétés souhaitées de ce modèle. La vérification s’applique
sur une exploration complète ou partielle du modèle. Les
avantages principaux de cette technique sont :
– La possibilité de rendre l’exploration du modèle automa-
tique.
– La facilité de production de contre-exemples, lorsque la
propriété est violée.
Le modèle considéré dans le cas d’utilisation d’un outil
de “model checking” est un système de transitions étiquetées
(STE). Il existe plusieurs outils utilisant cette technique de
vérification. Dans le paragraphe qui suit, nous décrivons la
vérification avec l’outil Aldébaran.
1) Vérification avec l’outil Aldébaran: Aldébaran [4] est
un outil qui vérifie les systèmes communicants représentés
sous forme de systèmes de transitions étiquetées (STE). Il
permet de minimiser et de comparer ces systèmes par rapport
à des relations d’équivalences (exp., bisimulation, équivalence Fig. 10. Le modèle à vérifier.
d’observabilité, etc.).
Dans notre cas, nous utilisons la fonction de minimisation.
Cette dernière permet de générer le plus petit graphe équivalent
à un STE par rapport à la relation d’équivalence de sûreté cette propriété. Cet observateur est représenté sous la forme
(safety) [10]. d’un automate qui contrôle le comportement du système et
Il s’agit d’appliquer cette fonction à un STE. Le graphe signale une erreur si P est violée. La Figure 11 montre
minimisé obtenu sera utilisé pour vérifier manuellement des l’observateur que nous avons utilisé pour vérifier notre pro-
propriétés que le système original doit satisfaire. priété de fraı̂cheur. Il contient une variable c qui représente
Dans ce qui suit, nous considérons une propriété de le compteur déclenché après une écriture. Si une action de
fraı̂cheur de données entre les modules ndd et aspect . Ce lecture se fait lorsque la variable c a déjà dépassé la valeur
dernier génère périodiquement une carte locale décrivant les 2, alors l’observateur va passer dans son état “ERROR” qui
obstacles dans le voisinage du robot. Cette carte est produite signifie que la propriété est violée. Durant l’exploration des
par le service ASPECTFromPosterConfig (AFPC) de aspect et états globaux du système, si un état global contenant l’état
est stockée dans son poster Obs . Ensuite elle est lue depuis “ERROR” de l’observateur est atteint, alors la propriété n’est
ce poster par ndd pour être utilisée par le service Goto. pas satisfaite.
La propriété de fraı̂cheur entre ndd et aspect consiste Le résultat de l’application de cette méthode sur notre
à imposer le fait que la carte produite par aspect soit modèle est négatif. Le graphe d’exploration de notre système
suffisamment “fraı̂che” avant d’être lue par le module ndd . contient l’état “ERROR”. L’observateur a donc détecté une
Nous imposons donc la contrainte temporelle suivante : violation de la propriété. Cette violation aurait pu être vu
autrement. En effet, avec les périodes fixées pour chaque
date lecture - date ecriture ≤ a modules, nous remarquons bien que il est possible de s’écouler
où “a” est un paramètre que l’on a choisi (arbitrairement) égale jusqu’à 39 ms entre une écriture et la prochaine lecture. Or,
à 2 unités de temps système (tick). Cette contrainte consiste si la contrainte est au maximum 20 ms, alors il est probable
à fixer un délai maximal de 2 ticks pour lire la dernière carte que la propriété peut être violée.
écrite. Une éventuelle solution de ce problème consiste à choisir
La Figure 10 montre le modèle adopté pour la vérification de soigneusement les périodes des deux modules.
cette propriété. Notre objectif est de l’imposer par construction
VI. C ONCLUSION
en fixant les périodes de chaque module dans le Timer de sa
tâche d’exécution. La synchronisation entre les deux modules L’essor de la robotique de service, et le déploiement de
est réalisée par le connecteur entre les deux Timers. L’action robots d’exploration coûteux et loin de l’homme sont deux
de lecture est chargée lors de l’exécution du service Goto. moteurs qui poussent la robotique autonome vers une plus
Les périodes des modules GenoM aspect et ndd sont grande sûreté, en particulier, de l’ensemble des logiciels.
respectivement 4 et 10 ticks, soit 40 et 100 ms. La vérification Jusqu’à ce jour, les robots autonomes sont développés avec des
avec Aldébaran n’est pas possible. En effet, l’outil ne peut méthodologies et des approches “classiques” essentiellement
pas générer le graphe lorsque le modèle est assez grand. Nous inspirées du “génie logiciel” (modularisation, hiérarchisation,
avons choisi donc d’utiliser les observateurs pour vérifier la organisation en couches). Toutefois, la complexité des fonc-
propriété. tions mises en oeuvre sur ces robots, et l’utilisation d’ap-
2) Vérification en utilisant les observateurs: Pour vérifier proches décisionnelles en font des objets logiciels parti-
une propriété P dans un système représenté sous forme de culièrement difficiles à valider ou à vérifier. Nous proposons
graphe, on peut construire un observateur (“Observer”) pour une approche originale de développement de ces logiciels qui
 [9] F. Py and F. Ingrand, ‘Dependable execution control for autonomous
robots’, in IROS, Sendai, Japan, (2004).
[10] C. Rodriguez, Spécification et validation de systèmes en XESAR, Ph.D.
dissertation, Institut National Polytechnique de Grenoble, 1988.

Fig. 11. Observateur.

s’appuie sur une architecture (LAAS) et des outils préexistants

de la robotique (GenoM) en y adjoignant une approche
de modélisation par componentisation (BIP) qui permet la
synthèse de contrôleurs sûrs par construction, et la vérification
de propriétés critiques pour le déploiement de systèmes temps
réel. Nous avons montré comment des modules fonctionnels
d’un robot mobile peuvent être modélisés en BIP à travers un
processus évolutif à partir des modules existants. On obtient
ainsi une couche fonctionnelle dont le contrôleur garantit des
propriétés fortes, liées à l’application elle-même (séquence
d’initialisation correcte, évitement d’interactions dangereuses,
etc). De plus, le modèle obtenu peut être vérifié avec divers
outils afin de garantir des propriétés critiques (absence de
blocage fatal, propriétés temporelles, etc). Notre objectif est
de poursuivre, vers les couches décisionnelles, le déploiement
de cette approche afin de bénéficier de contrôleurs et d’outils
formels sur l’ensemble des logiciels du robot autonome.
R EFERENCES
[1] R. Alami, R. Chatila, S. Fleury, M. Ghallab, and F. Ingrand, ‘An archi-
tecture for autonomy’, IJRR, Special Issue on Integrated Architectures
for Robot Control and Programming, 17(4), (1998).
[2] A. Basu, M. Bozga, and J. Sifakis, ‘Modeling heterogeneous real-time
components in BIP’, in SEFM, Pune, India, (2006).
[3] S. Bensalem, M. Bozga, T.H. Nguyen, and J. Sifakis, ‘Compositional
verification for component-based systems and application’, Technical
Report TR-2008-8, Verimag, (2008).
[4] M. Bozga, J-C. Fernandez, A. Kerbrat, and [Link], ‘Protocol veri-
fication with the aldebaran toolset’, in Software Tools for Technology
Transfer 1, pp. 166–183, (1997).
[5] S. Fleury, M. Herrb, and R. Chatila, ‘GenoM : A tool for the specification
and the implementation of operating modules in a distributed robot
architecture’, in IROS, Grenoble, France, (1997).
[6] G. Goessler and J. Sifakis, ‘Component-based construction of deadlock-
free systems’, in FSTTCS, Bombay, India, (2003).
[7] F.F. Ingrand, R. Chatila, R. Alami, and F. Robert, ‘PRS : A High Level
Supervision and Control Language for Autonomous Mobile Robots’, in
IEEE International Conference on Robotics and Automation, Mineapo-
lis, USA, (1996).
[8] S. Lemai, IxTeT-eXeC : planning, plan repair and execution control
with time and resource management, Ph.D. dissertation, Institut National
Polytechnique de Toulouse, 2004.