Model-based mDignosis for Formal Temporal Descriptions

With globalization and the resulting worldwide competition, high quality systems have crystallized as one way to compete with business rivals. Using a formal temporal language to state the behavioral specification of a protocol, component, or entire system, is a first step towards a high quality product and an efficient development process: It makes subtle questions explicit that otherwise might be hidden in the ambiguity of natural language, and it enables automatic tools. Obviously, a formal notation is not enough to ensure the quality of a specification. Current research, however, mainly focuses on the verification phase, where for example a chip design is verified against its behavioral specification, and not on assisting the designer when writing the specification itself. This is somewhat surprising, as industrial data show that about 50 percent of product defects and about 80 percent of rework efforts can be traced back to flawed specifications. With this project, we face the challenge to provide diagnostic information in the process of developing or verifying formal temporal specifications. Specifically, we will tackle the question of why a specific trace is a counterexample or witness, that of what is wrong with a specification if a specific behavior is unexpectedly contained (or not contained) in the specification, and also that of how to properly explain (complex) formal temporal properties. For this purpose, we will integrate the concept of model-based diagnosis from the artificial intelligence community with ideas and techniques that are well-known in the context of temporal logics and verification, like model- checking. Model-based diagnosis will allow us to diagnose the cause of encountered problems during formal specification development, so that we will be able to meet important needs of involved scientists and designers. A general aim of ours will be to provide the scientist or designer with information directly related to the specification, rather than information related to a derived automaton. In order to offer an attractive platform, we will consider the well-known Linear Temporal Logic (LTL) and also extensions suggested by newer languages like the Property Specification Language (PSL). Although LTL and PSL have their origin in the design of programs and electronic hardware, LTL has, for instance, also been used in other applications like the maintenance of knowledge-bases. Thus we will provide a solution that is usable in any application that draws from formal temporal specifications. With our focus on providing diagnostic information which eases the development, maintenance, and application of formal temporal specifications, as well as increases their quality, we expect this project to leverage the incorporation of formal temporal descriptions in industry and also scientific projects. In our vision, we expect that our integration of ideas and technologies from multiple research communities will provide new stimuli for future research.

Each and everyone of us has been occasionally experiencing problems caused by misunderstandings in our communications. For development teams, the use of dedicated description languages can help to avoid such issues and automated verification techniques then allow designers to verify their development steps (or the final products) against developed specifications. Our research was motivated by the question: What if a specification does not exactly catch the designers intent, or contains faults for some other reason? How can we identify corresponding faults based on erroneous behavior? The context we investigated was that of a systems functional and temporal behavior where we consider and evaluate a systems reactions to received inputs, like an execution of some software program or digital hardware. For Amir Pnuelis temporal logic of programs (LTL) that is often also used for digital hardware specifications, we showed how to efficiently diagnose corresponding specifications for unexpected behavior via constructing and solving specific satisfiability problems. Our diagnoses tell a designer which parts of a specification (or which combinations) might be responsible for the encountered problem. We offer also a more elaborate diagnosis approach that indeed provides also corresponding solutions/repairs via consideration of fault models that we developed for this purpose. Starting with LTL, we have been investigating corresponding diagnosis solutions also for more complex and other temporal description formats like program control graphs (derived from service oriented architectures) and reasoning-bases of robots. The motivation behind our reasoning used for deriving our specification diagnoses is very close to reasoning about how to best explain a specification, specifically when considering the task of exploring what is and what is not allowed (or specified) by a given specification. Thus we have been investigating also ways to identify sets of example behavior for characterizing a specification and in turn used this knowledge to derive test suites that with a high probability allow us to unveil faults in a specification via triggering unexpected behavior (then to be diagnosed) for the input stimuli provided by the test suite.A specific focus of our research was also optimizing our diagnosis process, where we investigated both, general (domain-independent) optimizations of the underlying algorithms and diagnosis theory, as well as domain-dependent optimization. In this direction we showed how to exploit a specifications structure and could also improve on established diagnosis algorithms in theoretical aspects. A library with corresponding implementations is publicly available.