OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Beyond Formal Methods for Critical Interactive Systems: Dealing with Faults at Runtime

Fayollas, Camille and Martinie De Almeida, Celia and Palanque, Philippe and Deleris, Yannick Beyond Formal Methods for Critical Interactive Systems: Dealing with Faults at Runtime. (2015) In: Workshop on Formal Methods in Human Computer Interaction (FoMHCI 2015), 23 June 2015 - 23 June 2015 (Duisburg, Germany).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://publications.rwth-aachen.de/record/479353/files/FoMHCI2015proceedings.pdf


Formal methods provide support for validation and verification of interactive systems by means of complete and unambiguous description of the envisioned system. They can also be used (for instance in the requirements/needs identification phase) to define precisely what the system should do and how it should meet user needs. If the entire development process in supported by formal methods (for instance as required by DO 178C [7] and its supplement 333 [8]) then classical formal method engineers would argue that the resulting software is defect free. However, events that are beyond the envelope of the specification may occur and trigger unexpected behaviors from the formally specified system resulting in failures. Sources of such failures can be permanent or transient hardware failures, due to (when such systems are deployed in the high atmosphere e.g. aircrafts or spacecrafts) natural faults triggered by alpha-particles from radioactive contaminants in the chips or neutron from cosmic radiation. This position paper proposes a complementary view to formal approaches first by presenting an overview of causes of unexpected events on the system side as well as on the human side and then by discussing approaches that could provide support for taking into account system faults and human errors at design time.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Licence Creative Commons : CC-BY-NC-ND. The definitive version is available at : https://publications.rwth-aachen.de/record/479353/files/FoMHCI2015proceedings.pdf
HAL Id:hal-01334722
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Other partners > Airbus (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Institut National des Sciences Appliquées de Toulouse - INSA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:06 Jun 2016 15:37

Repository Staff Only: item control page