{'fraction_non_alphanumeric': 0.03724696356275304, 'fraction_numerical': 0.010526315789473684, 'mean_word_length': 5.029268292682927, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Property-driven functional healing : Playing against undesired behavior

In this paper, we show how to use GEAR, a game-based model checker, for property-driven functional healing of high-assurance systems. Designers and engineers can interactively investigate the winning strategies resulting from the games. These reveal in-depth information about the connection between the property, the system, and the proof, both as explanation in case of a successful proof, and as detailed, fine-granular error diagnostics in the case of failure. This results in an interactive use of the tool where debugging and redesign are carried out by playing against undesired behavior. The benefits of the approach are illustrated on a case study that concerns the design of the task-level control part of the processes of the ExoMars Rover [Kap05], which was designed as part of a European Space Agency (ESA) project. 1 This work has been partially supported by the European Union Specific Targeted Research Project SHADOWS (IST-2006-35157), exploring a Self-Healing Approach to Designing cOmplex softWare Systems. The project’s web page is at https://sysrun.haifa.ibm.com/shadows. 2 Marco Bakera, Tiziana Margaria, Clemens D. Renner, Bernhard Steffen