Search

This is an extended version (including the Minnie RMP440 experiment) of a paper currently under review; Validation and Verification (V&V) of autonomous robotics system software is becoming a critical issue. Among the V&V techniques at our disposal, formal approaches are among the most rigorous and trustworthy ones. Yet, the level of skills and knowledge required to use and deploy formal methods is usually quite high and rare. In this paper, we describe an approach that starts from a regular, but rigorous, framework to specify and deploy robotics software components, which can also automatically synthesize a formal model of these components. The fact that this formal model is behaviourally equivalent to the implementation of the component is very promising. We show how we can use this formal model to prove properties both offline, for model-checking (e.g., schedulability, worst-case time, exclusivity). We also describe our approach to execute this formal model, in place of a traditional implementation, and show how this provides the opportunity to add powerful monitoring and runtime verification capabilities to the system (e.g., prevent robot damage, force landing). We believe that having a consistent workflow, from an initial specification of our system, down to a formal, executable specification is a major advance in robotics and open the way for verification of functional components of autonomous robots and beyond. We illustrate this claim by describing a complete example based on a genuine drone flight controller.

Nous pouvons retenir neuf sites attribuables à La Tène finale parmi les cinquante-neuf sites fortifiés de hauteur répertoriés en Basse-Normandie. Parmi eux, six sont considérés comme des oppida avec des dimensions comprises entre 20 et 167 hectares. Les trois derniers semblent correspondre à de petites agglomérations dont la superficie ne dépasse pas 7 hectares. Les informations, souvent modestes, concernant ces sites, restent généralement cantonnées à l’étude du système défensif. Les travaux archéologiques entrepris récemment, notamment dans le cadre d’un PCR, comble progressivement les lacunes de nos connaissances sur ces premiers sites urbains. Of the fifty nine hillforts presently identified in Lower-Normandy, nine are known to belong to the Late La Tene period. These include only six which are considered as oppida, their sizes ranging between 20 and 167 hectares. The remaining three sites are smaller agglomerations, covering no more than 7 hectares. The scant information available on these sites mainly concerns their fortification systems. Recent archaeological work, particularly that undertaken for a Collective Research Programme, has allowed gaps in our knowledge of these early urban sites to be filled.

GenoM is an approach to develop robotic software components, which can be controlled, and assembled to build complex applications. Its latest version GenoM3, provides a template mechanism which is versatile enough to deploy components for different middleware without any change in the specification and user code. But this same template mechanism also enables us to automatically synthesize formal models (for two Validation and Verification frameworks) of the final components. We illustrate our approach on a real deployed example of a drone flight controller for which we prove offline real-time properties, and an outdoor robot for which we synthesize a controller to perform runtime verification.

National audience; This paper presents recent developments of the LAAS architecture for autonomous systems: the GenoM3 component generator for functional components design. The GenoM tool was originally designed for autonomous and terrestrial mobile robots. This tool remains fairly general and is supported by a consistently integrated set of tools and methodologies, in order to properly design, integrate, test and validate a complex autonomous system. GenoM3 intends to grant middleware independance to robotic software components so that a clear separation of concerns is achieved between highly reusable algorithmic parts and integration frameworks. Such a decoupling let middlewares be used interchangeably, while fully benefitting from their specific, individual features.

Cet ouvrage est la publication des actes du 33e colloque international de l’AFEAF, qui s’est tenu à Caen, du 20 au 24 mai 2009. De même que le colloque, il comprend deux parties. La première, qui contient dix-sept contributions, traite de l’actualité des recherches sur l’Âge du fer en Basse-Normandie, une région qui a connu un renouvellement important de la documentation permettant d’appréhender les dynamiques d’occupation et les formes d’organisation territoriale durant la Protohistoire. Plusieurs bilans synthétiques concernant l’habitat rural, les sites fortifiés et la culture matérielle, sont, entre autres, proposés ici. La seconde partie de l’ouvrage traite du thème de la mort et des pratiques funéraires durant la période Ve-Ier siècles avant J.-C. ; elle contient vingt-deux contributions. Ce sujet a été abordé en privilégiant quelques axes de réflexion, de façon à faciliter les comparaisons entre régions. À travers des bilans synthétiques, le thème spécialisé du colloque est traité à l’échelle de la Gaule, avec les éclairages de plusieurs régions de l’Europe celtique. This is the publication of the proceedings of the 33rd AFEAF symposium held in Caen from the 20th to the 24th of May 2009. Like the symposium, this book is divided in two parts. The first part, with its 17 contributions, deals with the current knowledge about the Iron Age in Lower Normandy. An important renewal of the documentation concerning this region allows a better understanding of the occupational processes and territorial organization existing throughout Protohistory. This first part also includes several summary reports on rural settlements, fortified sites as well as finds. The second part of the book, with 22 contributions, deals with the subject of death and funerary practices during the 5th to 1st centuries BC. The subject was discussed focussing on a chosen number of thoughts as to make it easier to compare between different regions. Various summary reports allow an overview of this specialized topic throughout Gaul with perspectives from other regions of Celtic Europe.

This thesis focuses on the problem of localizing an autonomous mobile robot in natural environments. The first part of the manuscript presents the problem in a functional aspect and explores algorithmic methods that produce an estimate of the rover position. A classification of such methods is suggested and three main classes are proposed. The first class is called "local". Algorithms of this class work directly on raw data perceived by the robot and usually run at high frequency; the rover position is computed incrementally, by summing elementary displacements. It is for instance the case of odometry, the first method developed in the manuscript and to which a chapter is devoted. An original visual motion estimation method is then proposed: it uses stereo-vision and pixel tracking in video-image sequences. This method helps to palliate odometry drawbacks, notably on uneven terrains. However, positions computed by local methods enventually drift. It is thus necessary, for long term navigation, to use methods of the second class which we call "global": such methods (such as landmark based approaches) reduce the drifts of the local methods. A method based on local digital elevation maps --- incrementally built --- is proposed in the third chapter. Digital elevation maps allow to refine the position estimate by minimizing a distance between a local 3D image and the environment's model. Furthermore, thanks to an original map structure, the rover's trajectory is memorized: this allow to back-propagate modifications on previous position estimates (corrected by landmark based algorithms for instance) and thus guarantee a better spatial coherence of the global model. The last class of algorithms is called "absolute" and concerns localization methods that work on high level data, issued of a fusion and an interpretation of local data. However, such methods are not presented in this document. The next chapter of the manuscript presents localization from the "integr ation" point of view and analyzes the problems raised by integrating several localization algorithms together. To obtain real autonomy, the rover must be able to use a large panel of functionalities (even redundant ones). Integrating these methods has been done in the LAAS architecture context (an architecture for autonomous systems). This architecture gives a mean to use modular functionalities and allows them to cooperate. It has been necessary to precise how localization functionalities had to be integrated. In particular, time-stamps, data tagging and data fusion problems have been addressed.; Cette thèse aborde le problème de la localisation d'un robot mobile autonome en environnements naturels. La première partie du mémoire s'intéresse aux méthodes algorithmiques pouvant fournir une estimation de position et une classification de ces différentes méthodes en trois grandes catégories est proposée. La première classe présentée est dite " locale ". Elle repose sur un niveau d'abstraction très faible et utilise des données " brutes " ; la position du robot est calculée de façon incrémentale, par cumul de déplacements élémentaires. L'odométrie appartient à cette classe et ce document présente une analyse de ses performances. Une méthode originale d'estimation visuelle des déplacements est également proposée. Elle utilise la stéreo-vision et effectue le suivi de pixels dans une séquence d'images vidéo pour en déduire des déplacements élémentaires. Cette méthode permet de pallier certains inconvénients de l'odométrie, notamment en terrains accidentés. Les positions produites par les méthodes locales sont cependant sujettes à des dérives inexorables. Il est donc nécessaire d'utiliser des méthodes de la seconde classe --- dite " globale ". Celles-ci permettent, dans certaines circonstances, de réduire la dérive des méthodes locales (on trouve notamment dans cette catégorie les méthodes de localisation sur amers). Une méthode basée sur des cartes d'élévations est présentée. Cette représentation permet un recalage en position par minimisation d'une distance entre une image 3D locale et le modèle. De plus, grâce à une technique particulière de construction, une mémorisation de la trajectoire du robot permet de rétro-propager des modifications sur certaines positions et de garantir ainsi une (meilleure) cohérence spatiale du modèle. La dernière catégorie, regroupant les méthodes de localisation par rapport à un modèle initial ou les méthodes " absolues ", ne sont pas abordées dans ce document. La deuxième partie du mémoire analyse les problèmes posés par l'intégration des diverses méthodes à bord d'un robot dans le but de doter celui-ci d'un éventail de fonctionnalités, éventuellement redondantes. Une démonstration de navigation, réalisée grâce au robot Lama du groupe RIA du LAAS, est détaillée. L'intégration a été réalisée à travers le formalisme défini dans l'architecture LAAS (architecture pour les systèmes autonomes) et a abouti à la précision, au sein de cette architecture, du cadre nécessaire aux fonctionnalités de localisation. Notamment, les problèmes du datage des données et de fusion des informations de position sont pris en compte et une réflexion sur les transferts de données est proposée.