Arne Nordmann

Arut Prakash Kaleeswaran, Arne Nordmann, Thomas Vogel et al.

Context: Safety is of paramount importance for cyber-physical systems in domains such as automotive, robotics, and avionics. Formal methods such as model checking are one way to ensure the safety of cyber-physical systems. However, adoption of formal methods in industry is hindered by usability issues, particularly the difficulty of understanding model checking results. Objective: We want to provide an overview of the state of the art for counterexample explanation by investigating the contexts, techniques, and evaluation of research approaches in this field. This overview shall provide an understanding of current and guide future research. Method: To provide this overview, we conducted a systematic literature review. The survey comprises 116 publications that address counterexample explanations for model checking. Results: Most primary studies provide counterexample explanations graphically or as traces, minimize counterexamples to reduce complexity, localize errors in the models expressed in the input formats of model checkers, support linear temporal logic or computation tree logic specifications, and use model checkers of the Symbolic Model Verifier family. Several studies evaluate their approaches in safety-critical domains with industrial applications. Conclusion: We notably see a lack of research on counterexample explanation that targets probabilistic and real-time systems, leverages the explanations to domain-specific models, and evaluates approaches in user studies. We conclude by discussing the adequacy of different types of explanations for users with varying domain and formal methods expertise, showing the need to support laypersons in understanding model checking results to increase adoption of formal methods in industry.

Arut Prakash Kaleeswaran, Arne Nordmann, Thomas Vogel et al.

Context: The complexity of modern safety-critical systems in industries keep on increasing due to the rising number of features and functionalities. This calls for formal methods in order to entrust confidence in such systems. Nevertheless, using formal methods in industry is demanding because of usability issues, e.g., the difficulty of understanding model checking results. Thus the hypothesis is, presenting the result of model checker results in a user-friendly manner could promote formal methods usage in industries. Objective: We aim to evaluate the acceptance of formal methods by engineers if the complexity of understanding verification results is made easy. Method: We perform two different exploratory studies. First, we conduct an online survey to explore challenges in identifying inconsistent specifications and using formal methods from engineers. Second, we perform a one group pretest and posttest experiment to collect impressions from engineers using formal methods if understanding verification results is eased. Limitations: The main limitation of this study is the generalization because the survey focuses on a particular target group and it uses a pre-experimental design.

Simon Greiner, Peter Munk, Arne Nordmann

In the paper Compositionality of Component Fault Trees, we present a discussion of the compositionality of correctness of component fault trees. In this technical report, we present the formal proof of the central theorem of the aforementioned publication.

Arne Nordmann, Sebastian Wrede

Model-driven software development is a promising way to cope with the complexity of system integration in advanced robotics, as it already demonstrated its benefits in domains with comparably challenging system integration requirements. This paper reports on work in progress in this area which aims to improve the research and experimentation process in a collaborative research project developing motor skill architectures for compliant robots. Our goal is to establish a model-driven development process throughout the project around a domain-specific language (DSL) facilitating the compact description of adaptive modular architectures for rich motor skills. Incorporating further languages for other aspects (e.g. mapping to a technical component architecture) the approach allows not only the formal description of motor skill architectures but also automated code-generation for experimentation on technical robot platforms. This paper reports on a first case study exemplifying how the developed AMARSi DSL helps to conceptualize different architectural approaches and to identify their similarities and differences.