FWF - MoDiaForTeD - Model-based Diagnosis for Formal Temporal Descriptions (MoDiaForTed)

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 questions of why a specific trace is a counterexample or witness, and that of what is wrong with a specification if a specific behavior should or should not have been contained by it, 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.