Search

Fault detection, isolation and recovery subsystems are accepted to make safety-critical systems resilient against faults and failures. Yet, these subsystems should be devised only for those faults that violate the system's requirements, while providing a correct approach such that requirements are met again. Consequently, the obtained system is minimal, although complete, and robust both with respect to safety and performance requirements. In this paper, we propose a systematic and automated approach based on formal methods that includes (1) the evaluation of the relevance of faults based on quantitative risk assessment, and (2) the validation of system robustness by statistical model checking. We apply this approach on an excerpt of a real-life autonomous robotics case study, and we report on the implementation and results obtained with the S BIP framework. [ABSTRACT FROM AUTHOR]

Recent years have seen a manifest increase in the use of modelling by the embedded systems industry. UML and SysML are two examples of languages used in this context. One of the reasons why the use of models is interesting is the possibility to perform early verification, validation and testing. A lot of work was devoted to developing theoretical results in verification and validation, and interesting results are available. Integrating these results in frameworks that take high-level models as an entry remains a challenging task, for several reasons that include the difficult scalability of the theoretical results. In previous work, we presented OMEGA 2, a framework that takes this challenge. Applying our framework on large industrial models revealed the fact that some features of the UML/SysML semantics which lead to bottlenecks in verification are not actually necessary in the models that we considered, thus leaving place for optimisations. This paper discusses the gap existing between the choices made in the general UML/SysML semantic framework and the actual needs of the users. We illustrate it based on the semantics of ports, for which we give a simplified version of the semantics. This semantics was implemented in our tools and we quantify the optimisation obtained when applying it to a set of case studies. [ABSTRACT FROM AUTHOR]