Search

International audience; Faults in spacecraft systems are an important problem, mainly because of the cost of downtime, and because their remoteness makes maintenance more difficult. This is why automated handling of faults can greatly enhance the system overall performance. This automated fault management relies on dedicated functions for fault detection, identification, and recovery (FDIR), that are often interleaved with the system, which makes it difficult to guarantee tolerance with respect to a particular anomaly, and makes the system difficult to maintain as well. On the other hand, several advanced computational tools exist that are known to support the tasks of FDIR. In this paper, starting from the current state of affairs in spacecraft system development, we develop and test several options for enhancing the quality of FDIR functions. First, we use software validation and verification tools to prove that the FDIR functions meet some functional quality goals. A second option we explore is to re-implement FDIR functions by Model-Based Reasoning algorithms, that are guaranteed to produce exact results with respect to a model of the system’s behaviour. In each option, we use and compare several software tools, we compare the effort required to adapt, integrate and use them, and estimate the overall benefits theyprovide.

Cet article vise à décrire une architecture de sécurité de systèmes autonomes à l’aide de la méthode formelle Event-B. Le formalisme Event-B supporte une conception rigoureuse de ces systèmes. La technique de raffinement permet une modélisation progressive en vérifiant la correction et la pertinence des modèles par décharge de preuves. L’application de la méthode Event-B présente un intérêt dans la formalisation des relations entre couches qui assurent la cohérence d’un fonctionnement sûr ainsi que le respect des exigences de sécurité concernées par notre analyse. Par conséquent, la modélisation autour de ces relations fait apparaître en permanence un comportement nominal associé à des comportements en présence de fautes sous l’hypothèse d’une architecture intégrant des mécanismes de tolérance aux fautes.

Cet article présente une partie de l'étude d'architectures de sécurité de systèmes autonomes s'appuyant sur l'utilisation de la méthode formelle Event-B. Le formalisme Event-B supporte bien la conception rigoureuse de ces systèmes qui combinent diverses activités que l'on peut structurer en couches. Sa technique de raffinement permet une modélisation progressive en vérifiant la correction et la pertinence des modèles par décharge de preuves. L'application de la méthode Event-B dans le cadre de la spécification d'architectures en couches garantit l'émergence de propriétés globales attendues, telles que les propriétés de sécurité, lorsque l'on s'assure du respect de propriétés au niveau des relations entre les couches. Cet article se situe au début de cette nouvelle étude. Il présente les principes de la modélisation Event-B d'un système de contrôle de drone simplifié. Il caractérise le concept d'architecture en couches utilisée pour cette modélisation. Il décrit ensuite une première modélisation d'une couche avant de conclure sur l'intérêt de cette modélisation pour la validation de systèmes autonomes par rapport aux objectifs de sécurité fixés.

This paper aims at describing safety architectures of autonomous systems by using Event-B formal method. The autonomous systems combine various activities which can be organised in layers. The Event-B formalism well supports the rigorous design of this kind of systems. Its refinement mechanism allows a progressive modelling by checking the correctness and the relevance of the models by discharging proof obligations. The application of the Event-B method within the framework of layered architecture specification enables the emergence of desired global properties with relation to layer interactions. The safety objectives are derived in each layer and they involve static and dynamic properties such as an independence property, a redundant property or a sequential property. The originality of our approach is to consider a refinement process between two layers in which the abstract model is the model of the lower layer. In our modelling, we distinguish nominal behaviour and abnormal behaviour in order to well establish failure propagation in our architecture.

This paper presents a method to analyse the operational safety of complex systems and the application of this method to an Unmanned Aerial Vehicle (UAV). The method relies on the complementary use of AltaRica and Event-B models. On the one hand, the AltaRica failure propagation models well support the safety analysis of complex systems. On the other hand, Event-B formalism well supports the design of system, from abstract specification to software development. Thus, the relationship between AltaRica and Event-B enables a better understanding for such a safety analysis.Accordingly, this paper focuses on the association of these two formalisms in the safety analysis of an UAV control system. This association is applied for an architecture which is structured in three hierarchical layers: operational layer, functional layer and physical equipment layer. But only the first two layers are dealt with in this paper.

La recherche de la sûreté de fonctionnement des systèmes complexes impose une démarche de conception rigoureuse. Les travaux de cette thèse s’inscrivent dans le cadre la modélisation formelle des systèmes de contrôle autonomes tolérants aux fautes. Le premier objectif a été de proposer une formalisation d’une architecture générique en couches fonctionnelles qui couvre toutes les activités essentielles du système de contrôle et qui intègre des mécanismes de sécurité. Le second objectif a été de fournir une méthode et des outils pour évaluer qualitativement les exigences de sécurité. Le cadre formel de modélisation et d’évaluation repose sur le formalisme Event-B. La modélisation Event-B proposée tire son originalité d’une prise en compte par raffinements successifs des échanges et des relations entre les couches de l’architecture étudiée. Par ailleurs, les exigences de sécurité sont spécifiées à l’aide d’invariants et de théorèmes. Le respect de ces exigences dépend de propriétés intrinsèques au système décrites sous forme d’axiomes. Les preuves que le principe d’architecture proposé satisfait bien les exigences de sécurité attendue ont été réalisées avec les outils de preuve de la plateforme Rodin. L’ensemble des propriétés fonctionnelles et des propriétés relatives aux mécanismes de tolérance aux fautes, ainsi modélisées en Event-B, renforce la pertinence de la modélisation adoptée pour une analyse de sécurité. Cette approche est par la suite mise en œuvre sur un cas d’étude d’un drone ONERA. The study of complex system safety requires a rigorous design process. The context of this work is the formal modeling of fault tolerant autonomous control systems. The first objective has been to provide a formal specification of a generic layered architecture that covers all the main activities of control system and implement safety mechanisms. The second objective has been to provide tools and a method to qualitatively assess safety requirements. The formal framework of modeling and assessment relies on Event-B formalism. The proposed Event-B modeling is original because it takes into account exchanges and relations between architecture layers by means of refinement. Safety requirements are first specified with invariants and theorems. The meeting of these requirements depends on intrinsic properties described with axioms. The proofs that the concept of the proposed architecture meets the specified safety requirements were discharged with the proof tools of the Rodin platform. All the functional properties and the properties relating to fault tolerant mechanisms improve the relevance of the adopted Event-B modeling for safety analysis. Then, this approach is implemented on a study case of ONERA UAV.

Dans cette étude, nous nous intéressons à la résolution des "Problèmes de Satisfaction de Contraintes valués" (CSP valués). Cette modélisation extrêmement simple, intuitive et riche s’adapte facilement à une grande variété de problèmes d'optimisation. De nombreux travaux ont par ailleurs fourni toute une bibliothèque d'algorithmes de résolution. Dans le cadre classique de la satisfaction des CSP, l'efficacité de ces méthodes n’est plus à démontrer et leur domaine d'application est assez bien connu. L'introduction d'une valuation des contraintes dans le modèle CSP, qui donne naissance aux CSP valués, est cependant trop récente pour que les possibilités et les limites d'efficacité soient clairement identifiées. L'ordonnancement des satellites d'observation de la Terre fait partie des CSP valués à la frontière des compétences actuelles en matière d'optimisation. Cette application est pour nous un prétexte au développement d’outils de résolution nouveaux étendant le champ des CSP valués accessibles. Notre travail est centré sur la notion de "contrainte induite", largement utilisée dans le cadre classique, et dont l'extension difficile aux CSP valués limite actuellement l'amélioration des algorithmes de recherche complets. Afin de dépasser ces difficultés, directement liées à la non idempotence de l'agrégation des valuations des contraintes, nous proposons un formalisme minimal pour les contraintes induites. Nous montrons ensuite comment il peut être mis en œuvre pour étendre l'essentiel des algorithmes développés dans le cadre classique. Enfin, l'utilité de ces nouveaux outils est illustré sur les problèmes d'ordonnancement du satellite SPOT 5. In this study, we are interested in “Valued Constraint Satisfaction Problems”(Valued CSPs) solving. This model which is extremely genuine, intuitive and rich matches easily most of optimization problems. Many works have produced a full library of solving algorithms. In the CSP framework, the efficiency of these methods is admitted and their limits well known. The adjunction of a valuation to the constraints in the CSP model that brought Valued CSPs is quite recent and the possibilities and the solving limits are not well identified. Earth observation satellite scheduling is a problem that is on the border of the optimization abilities at the present time. For us, this application is a pretense to extend the field of accessible Valued CSPs. Our work focuses on the concept of “induced constraint" that is widely used in the classical CSP framework but is hard to extend to the Valued CSP framework. So that the improvement of the complete solving tools is limited for the present. In order to overcome these difficulties, directly linked to the non idempotency of the aggregation of the constraints valuations, we propose a minimal formalism for induced constraints. Then, we show how to extend the main algorithms developped in the classical CSP framework. At last, the usefullness of these new tools is illustrated on the satellite SPOT 5 scheduling problems.