Publications

Ensuring pedestrian-safety is paramount to the acceptance and success of autonomous cars. The scenario-based training and testing of such self-driving vehicles in virtual driving simulation environments has increasingly gained attention in the past years. A key challenge is the automated generation of critical traffic scenarios which usually are rare in real-world traffic, while computing and testing all possible scenarios is infeasible in practice. In this paper, we present a formal method-based approach CriSGen for an automated and complete generation of critical traffic scenarios for virtual training of self-driving cars. These scenarios are determined as close variants of given but uncritical and formally ab- stracted scenarios via reasoning on their non-linear arithmetic constraint formulas, such that the original maneuver of the self-driving car in them will not be pedestrian-safe anymore, enforcing it to further adapt the behavior during training.

About a decade ago, the fourth industrial revolution, also known as Industrie 4.0, has been ushered by the introduction of the Internet of Things and Services into the manufacturing environment. Since production and manufacturing control systems are increasingly networked and connected, the complexity of modern distributed cyber-physical production systems (CPPS) requires new tools for monitoring, failure detection and analysis. In this paper, we present a framework for semantic fault analysis of CPPS which combines semantic sensor data stream analysis for fault detection and diagnosis through reasoning on given domain model and belief network with fault prognosis through formal behavior analysis with timed hybrid automata. As CPPS are envisioned to not only cooperate with each other but also with humans on a new level of sociotechnical interaction, we use agentbased 3D visualisation tools to provide human users with support when repairing occurring faults. We illustrate the approach using the example of a smart factory case study.

In den letzten Jahren ist zunehmend die Tendenz zu erkennen, das Design von komplexen Anlagen aus einer kompositionalen und somit nicht-monolithischer Perspektive zu betrachten. Gleiches gilt seit jüngerer Zeit für die IT-Sicherheit. In diesem Papier stellen wir das KIARA-Sicherheitsmodell vor, wie es im Rahmen des FIWARE-Programms der EU entworfen und implementiert wurde. Im obigen Sinne agiert KIARA lokal auf den Knoten eines Netzwerks und nicht auf einer zentralisierten Sicherheitskomponente. Globale Sicherheitseigenschaften ergeben sich aus dem über feste Regeln definierten Zusammenspiel der einzelnen lokalen Sicherheitsbedürfnisse und Garantien

In this paper, we present a collaborative, web-based framework to create 3D scenarios for product design, simulation and training assisted by animated avatars. To support correct design and anticipate critical design decisions we employ a verification approach to check for safety and reachability properties. By animating the 3D model based on prover results (trace witnesses out of constructive proofs) the sys- tem provides tangible feedback of the verification to the designer. We describe the components of the framework and illustrate the functionality based on an existing factory production line.

This paper strikes two technical aspects that have become commonly applied in engineering, but, nevertheless, barely benefit from each other, at least what today’s concurrent engineering is concerned. One of them has to do with 3D-Visualization, be it as an output of a CAD-system, or even photo-realistic rendered/raytraced images and animations of the product or production line under consideration, and the other deals with Formal Analysis, i.e., the verification of (safety) properties against a suitable formal model of the scenario. In this paper we bring both these aspects together. We show how behaviors of a system deduced from verification results can be visualized as animations in the 3D model of the system. We also discuss how modifications of the 3D scene like positioning and adding or removing of objects can be reflected in the formal model of the system. As formal basis we use the language of hybrid automata, as 3D modeling language we use XML3D.

Verisoft XT was a three-year research project , funded by the German Federal Ministry of Education and Research (BMBF). The main goal of the project was the pervasive formal verification of computer systems. One of its sub-projects examined the application of formal methods in the avionics domain. Today’s avionics software should be developed in accordance with the RTCA/EUROCAE standard DO-178B/ED-12B to achieve formal acceptance by certification authorities. This standard lists formal methods merely as alternative means but does not provide guidance on the use and acceptance of formal methods. Its successor DO-178C/ED-12C will provide this guidance in its Formal Methods Supplement. Although DO-178C was not published during project runtime, the available material nevertheless allowed us to examine the compliance of two of the formal methods and tools – VSE and VCC – that have been used in Verisoft XT. This paper summarises the results of this evaluation and thus may serve as a first step in the certification planning of a real avionics project that would use either one or both methods.

Showing the absence of security hazards in cryptographic protocols is of major interest in the area of protocol security analysis. Standard model checking techniques - despite their advantages of being both fast and automatic - serve as mere debuggers that allow the user at best to detect security risks if they exist at all. In general they are not able to guarantee that all such potential hazards can be found, though. A full verification usually involves induction and therefore can hardly be fully automatic. Therefore the definition and application of suitable heuristics has turned out to become a central necessity. This paper describes how we attack this problem with the help of the Verification Support Environment (VSE) and how we nevertheless arrive at a high degree of automation.

Safety and security guarantees for individual applications in almost all cases depend on assumptions on the given context provided by distributed instances of operating systems, hardware platforms, and other application level programs running on these. In particular for formal approaches the problem is to formalize these assumptions without looking at the (formal) model of the operating system (including the machines that execute applications) in all detail. The work described in the paper proposes a modular approach which uses histories of observable events to specify runs of distributed instances of the system. The overall verification approach decomposes the given verification problem into local tasks along the lines of assume-guarantee reasoning. As an example the paper discusses the specification and implementation of the SMTP scenario. It shows in detail how this methodology is utilized within the Verification Support Environment (VSE) to verify the SMTP server part.

Safety and security guarantees for individual applications in general depend on assumptions on the given context provided by distributed instances of operating systems, hardware platforms, and other application level programs that are executed on these platforms. The problem for formal approaches is to formalize these assumptions without having to look at the details of the (formal) model of the operating system (including the machines that execute applications). The work described in this paper presents a modular approach which uses histories of observable events to specify runs of distributed instances of the system. The overall verification approach decomposes the given verification problem into local tasks along the lines of assume-guarantee reasoning. In this paper we focus on this methodology and on its realization in the Verification Support Environment (VSE). We also illustrate the proposed approach with the help of a suitable example, namely the specification and verification of an SMTP server whose implementation makes extensive use of various system calls as e.g. fork and socket commands.

Formal software development turns out to become one of the key issues in software engineering. Today an enormous variety of methods and tools exist that serve as an aid for the software engineer to formally specify and verify large-scaled systems. This paper reviews some of the most important general notions in formal software engineering and, in particular, gives an overview on VSE (Verification Support Environment), a tool that supports both hierarchical specification and formal verification.

Today we are confronted with an enormous variety of formal software engineering approaches and tools. Among these are many that address the critical early stages of software development. However, only little attention has been paid to the integration of different specialised approaches and to the overall development process. In this paper we present a technique for formal requirements analysis (observer models) that deals with particular perspectives on a system rather than with particular aspects of it. A realistic gasburner example illustrates the overall approach.

Verification of non-linear hybrid systems is a challenging task. Unlike manyy other verification methods the deduction-based verification approach we investigate in this paper avoids approximations and operates directly on the original non-linear system specifications. This approach, however, requires the solution of non-trivial mathematical sub-tasks. We propose to model existing reasoning systems, such as computer algebra systems and constraint solvers, as mathematical services and to provide them in a network of mathematical tools in a way that they can reasonably support subtasks as they may occur in formal methods applications. The motivation is to make it simpler to implement and test verification approaches by out-sourcing complex but precisely identifiable mathematical subtasks for which specialised reasoners do already exist.

It is well known that in many cases severe errors occur in the early stages of the software development process. Following this insight, considerable emphasis was put on requirements engineering. Formal methods provide means for the abstract yet precise description of required system properties. However, specialized description techniques are needed to treat certain aspects adequately. Moreover, complex systems often make it necessary to cover several of these views. Among the most critical and most difficult (to describe) aspects of systems behaviors are realtime properties. A major problem in this area lies in the complexity of timing constraints and the variety of situations that can appear in such systems. It turned out that timed automata or (linear) hybrid automata serve as a comprehensive mean to express temporal behavior. Verification Support Environment (VSE) supports abstract system specifications, the formulation and proof of safety an security properties, and refinements. The formal development method of VSE is based on Abstract Data Types and Temporal Logic. The aim of the work presented here is to integrate hybrid automata as a means for comprehensively describing realtime properties into the VSE method where an abstract system specification serves as the starting point of a formal refinement process. Hybrid automata (translated into VSE) provide a realtime view on these systems. Additional requirements specifications representing different views of the behavior can be "linked" to the same specification.

In formally analyzing and developing industrial sized systems we are often confronted with the problem of expressing realtime properties. Especially in safety critical applications as, for example, in embedded systems or in control software, these properties are crucial for the right functioning of the systems. There are numerous suitable approaches that allow us to specify realtime properties: MTL, TLA or VSE-SL to name a few, and also there are various tools available to formally develop such systems. But in most cases the approaches are trimmed for their own highly specialized application area. We try to overcome this restriction by exploiting the advantages of a (fairly general) formal development tool like VSE-II and the rather specialized Hybrid Automata by combining these two approaches.

In this paper we propose a verification method for hybrid systems that is based on a successive elimination of the various system locations involved. Briefly, with each such elimination we compute a weakest precondition (strongest postcondition) on the predecessor (successor) locations such that the property to be proved cannot be violated. Experiments show that this approach is particularly interesting in cases where a standard reachab lity analysis would require to travel often through some of the given system locations.

In this paper we focus on two powerful techniques to obtain compact clause normal forms: Renaming of formulae and refined Skolemization methods. We illustrate their effect on various examples. By an exhaustive experiment of all first-order TPTP problems, it shows that our clause normal form transformation yields fewer clauses and fewer literals than the methods known and used so far. This often allows for exponentially shorter proofs and, in some cases, it makes it even possible for a theorem prover to find a proof where it was unable to do so with more standard clause normal form transformations.

In this paper we propose a verification method for hybrid systems that is based on a successive elimination of the various system locations involved. Briefly, with each such elimination we compute a weakest precondition (strongest postcondition) on the predecessor (successor) locations such that the property to be proved cannot be violated. This is done by representing a given verification problem as a second-order predicate logic formula which is to be solved (proved valid) with the help of a second-order quantifier elimination method. In contrast to many ``standard'' model checking approaches the method as described in this paper does not perform a forward or backward reachability analysis. Experiments show that this approach is particularly interesting in cases where a standard reachability analysis would require to travel often through some of the given system locations. In addition, the approach offers possibilities to proceed where ``standard'' reachability analysis approaches do not terminate.

In modal logics we are interested in classes of frames that characterize the logic under consideration. Such classes are usually distinguished by their respective frame properties. In general these characterizations are not unique and it is desirable to find a strongest possible. In this article an approach is presented which helps in this respect. It allows us to transform a given background theory into one which is more general and which modal logics cannot distinguish from the former because of their syntactic and semantic restrictions. The underlying technique is based on the idea to find conservative extensions of a given logic whose frame properties allow us to extract significantly stronger characterizations of the original logic.

Second-Order predicate logic formulae with existentially or universally quantified predicate variables occur in various applications, as for instance in default reasoning with circumscription or correspondence theory in non-classical logics. In the latter cases it is important to find an equivalent first--order formula for a given formula with predicate quantifiers. Following early approaches by Wilhelm Ackermann a number of algorithms have been developed which accept a formula with predicate quantifiers as input and compute an equivalent first--order formula as output. In this chapter we give an overview of these algorithms and some of their applications. At least one algorithm is implemented and publicly available.

This paper is about automated techniques for second-order quantifier elimination and (modal logic) correspondence theory. Given a modal schema and a semantics based method of translating modal formulae into fist-order ones, we try to derive automatically a fixpoint formula characterizing precisely the class of frames validating this schema. We propose to consider fixpoint calculus as the underlying formalism rather than the classical first-order logic in order to be able to express more subtle correspondences. The technique we consider can, in many cases, be easily applied without any computer support. Although we mainly concentrate on Kripke semantics, our fixpoint approach is much more general, as it is based on the elimination of second-order quantifiers from formulae. Thus it can be applied in second-order theorem proving as well. We show some application examples for the method which may serve as new, automated proofs of the respective correspondences.

In this paper a technique is presented which provides us with a means to develop resolution-based calculi for (first-order) modal and temporal logics. The approach is based on three parts: A special translation technique from modal and temporal logic formulae into classical predicate logic, a certain kind of saturation technique which is to be applied to given background theories, and an extraction of either suitable ``simpler'' background theories or logic-specific inference rules. The former is interesting in case existing classical logic theorem provers are to be utilized; the latter gains importance if one is prepared to extend theorem provers that are already at hand.

In modal logics we are interested in classes of frames which determine the logic under consideration. Such classes are usually distinguished by their respective frame properties, often also called the modal logic's background theory. In general these characterizations are not unique and it is desireable (and that not only from a theorem prover's perspective) to find a strongest possible. In this paper an approach is presented which helps in this respect. It allows us to transform a given background theory into one which is more general and which modal logics cannot distinguish from the former because of their syntactic and semantic restrictions. The underlying technique is based on the idea to find conservative extensions (of a given logic) whose determining properties serve as a starting point from which it is possible to extract significantly stronger characterizations of the original logic.

This paper is about automated techniques for (modal logic) correspondence theory. The theory we deal with concerns the problem of finding fixpoint characterizations of modal axiom schemata. Given a modal schema and a semantics based method of translating modal formulae into classical ones, we try to derive automatically a fixpoint formula characterizing precisely the class of frames validating this schema. The technique we consider can, in many cases, be easily applied without any computer support. Although we mainly concentrate on Kripke semantics, our fixpoint approach is much more general, as it is based on the elimination of second-order quan- tifiers from formulae. Thus it can be applied in second-order theorem proving as well. We show some application examples for the method which may serve as new, automated proofs of the respective correspondences.

Standard logic programming languages like Prolog lack thepossibility of dealing with modalities and/or sorts. A first idea how to overcome this problem (and that without changing anything on Prolog itself) would be to apply the well-known relational translation approaches from modal and sorted logic into first-order predicate logic and to feed this translation result into Prolog. This, however, leads into other problems: firstly, the transformed problem is usually of much bigger size (number of clauses) than the original one and, secondly, very often it is not even in Horn form anymore. In this paper a translation approach is proposed which avoids both of these problems, i.e. the number of clauses after translation is exactly as big as it would have been if we simply ignored the modal operators and sort restrictions and, also, the result is in Horn form provided it was already before (modulo modal operators and sorts).

In this paper we focus on the application of description logics to natural language processing. In cooperation with the {\sc pracma} project we have been developing a suitably extended knowledge representation system, called {\sc motel}. In our approach to agent modelling and natural language processing we use an extension of the well-known description language $\cal ALC$. Our system {\sc motel}\ serves on one hand as a knowledge base for the natural language front-end, and on the other hand, it provides powerful {\em logical\/} representation and reasoning components. As our approach is logic based we hope that this enhances the overall capabilities of the natural language processing (NLP) system. We present a brief overview of {\sc motel} and the different extensions we are working on, i.e.\ modal extension of description logics, a cardinality-based approach to quantitative information, reason maintenance, probablistic, non-monotonic, and abductive reasoning.

MOTEL is a logic-based knowledge representation languages of the KL-ONE family. It contains as a kernel the KRIS language which is a decidable sublanguage of first-order predicate logic (see Baader and Hollunder (1990)). Whereas KRIS is a single-agent knowledge representation system, i.e. KRIS is only able to represent general world knowledge or the knowledge of one agent about the world, MOTEL is a multi-agent knowledge representation system. The MOTEL language allows modal contexts and modal concept forming operators which allow to represent and reason about the believes and wishes of multiple agents. Furthermore it is possible to represent defaults and stereotypes. Beside the basic resoning facilities for consistency checking, classification, and realization, MOTEL provides an abductive inference mechanism. Furthermore it is able to give explanations for its inferences.

We propose a translation approach from modal logics to first-order predicate logic which combines advantages from both, the (standard) relational translation and the (rather compact) functional translation method and avoids many of their respective disadvantages (exponential growth versus equality handling). In particular in the application to serial modal logics it allows considerable simplifications such that often even a simple unit clause suffices in order to express the accessibility relation properties. Although we restrict the approach here to first-order modal logic theorem proving it has been shown to be of wider interest, as e.g.\ sorted logic or terminological logic.

Many attempts have been started to combine logic programming and modal logics. Most of them however, do not use classical PROLOG, but extend the PROLOG idea in order to cope with modal logic formulae directly. These approaches have the disadvantage that for each logic new logic programming systems are to be developed and the knowledge and experience gathered from PROLOG can hardly be utilized. Modal logics based on Kripke-style relational semantics, however, allow a direct translation from modal logic into first-order predicate logic by a straightforward translation of the given relational semantics. Unfor- tunately such a translation turns out to be rather naive as the size of formulae increases exponentially during the translation. This paper now introduces a translation method which avoids such a rep- resentational overhead. Its basic idea relies on the fact that any binary re- lation can be replaced by equations and inequations which (under certain circumstances) can be eliminated later on by some further transformation. The overall approach thus works essentially for any modal logic having a Kripke-style possible world semantics and first-order describable frame properties. If at all, its application as a pre-processing for PROLOG is limited merely by the possibility of having frame properties which are not Horn or not even first-order describable.

Standard knowledge representation systems are supposed to be able to represent either common or individual knowledge about the world. In this paper we propose an extension to such knowledge representation systems which, in a uniform manner, allows to express beliefs of multiple agents as well as knowledge, desire, time and in fact any modality which has a first-order predicate logic possible world semantics.

Asynchronous processes arise naturally in real time environments where there is human-computer interaction, but formalisms for describing asynchronous processes and the ways of reasoning about them are not well understood. Abstract programming systems which assume asynchrony display a variety of of message-passing and stream architectures in which a process receives input through a mail-box or set of channels. These systems can be contrasted with programming systems like CSP and Ada which use the primitive notion of a rendevous to provide a synchronous basis for communication. In this paper we develop a compositional proof theory for the safety properties of asynchronous systems.

A short introduction to term rewriting systems. This chapter is supposed to provide beginners in logic with the basics of term rewriting, the Knuth-Bendix completion algorithm and theorem proving by rewriting.

A short introduction to term rewriting systems. This chapter is supposed to provide beginners in logic with the basic ideas behind term rewriting systems, Knuth-Bendix-Completion, and theory proving based on rewriting

A short introduction to modal and temporal logic. This chapter is supposed to provide beginners with the basic notions of modal and temporal logics, their syntax and semantics, frame topology and correspondence theory.