Chaudemar, Jean-Charles and Bensana, Eric and Seguin, Christel Model based safety analysis for an Unmanned Aerial System. (2010) In: DRHE 2010 - Dependable Robots in Human Environments, 16-17 June 2010, Toulouse, France .
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
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.
|Item Type:||Conference or Workshop Item (Paper)|
|Audience (conference):||International conference proceedings|
|Institution:|| Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE|
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA
|Deposited By:||jc Chaudemar|
Repository Staff Only: item control page