Mathematical proofs are a cornerstone of control theory, and it is important to get them right. Deduction systems can help with this by mechanically checking the proofs. However, the structure and level of detail at which a proof is represented in a deduction system differ significantly from a proof read and written by mathematicians and engineers, hampering understanding and adoption of these systems. This paper aims at helping to bridge the gap between machine-checked proofs and proofs in engineering and mathematics by presenting a machine-checked proof for stability using Lyapunov's theorem in a human-readable way. The structure of the proof is analyzed in detail, and potential benefits of such a proof are discussed, such as generalizability, reusability and increased trust in correctness.

Digitalization in seaports dovetails the IT infrastructure of various actors (e.g., shipping companies, terminals, customs, port authorities) to process complex workflows for shipping containers. The security of these workflows relies not only on the security of each individual actor but actors must also provide additional guarantees to other actors like, for instance, respecting obligations related to received data or checking the integrity of workflows observed so far. This paper analyses global security requirements (e.g., accountability, confidentiality) of the workflows and decomposes them - according to the way workflow data is stored and distributed - into requirements and obligations for the individual actors. Security mechanisms are presented to satisfy the resulting requirements, which together with the guarantees of all individual actors will guarantee the security of the overall workflow.

In this position paper, we propose a new design flow for cyber-physical systems which builds on our previous experiences in both the hardware and software domain. Its defining features are the integration of natural language processing, the formal specification level which allows an abstract description of the system’s behaviour, and a comprehensive functional change management throughout. We introduce the design flow and its three levels of abstraction by example, and argue why it is particularly suited for the development of cyber-physical systems.

A browser based protocol is the chief security component of a safety critical web application, such as e-banking. Accordingly, browser based protocols need to be thoroughly verified in order to guarantee they are up to comply with key security properties. To this end, we have developed WebMC, a model checker especially designed to consider web standards, with the aim of analyzing browser based protocol execution, as encompassed by the interactions of a typical user, a browser, and active attacker playing the role of the network, and one or more servers. In this paper, we shall show how to use WebMC in the design and the development of browser based protocols. Our tool has been successfully validated: WebMC has been able to reproduce a number of the verification results found in the literature, but fully automatically.

A browser based protocol is the chief security component of a safety critical web application, such as e-banking. Accordingly, browser based protocols need to be thoroughly verified in order to guarantee they are up to comply with key security properties. To this end, we have developed WebMC, a model checker especially designed to consider web standards, with the aim of analyzing browser based protocol execution, as encompassed by the interactions of a typical user, a browser, and active attacker playing the role of the network, and one or more servers. In this paper, we shall show how to use WebMC in the design and the development of browser based protocols. Our tool has been successfully validated: WebMC has been able to reproduce a number of the verification results found in the literature, but fully automatically.

This video paper describes the practical outcome of the first milestone of a project aiming at setting up a so-called Hybrid Team that can accomplish a wide variety of different tasks. In general, the aim is to realize and examine the collaboration of augmented humans with autonomous robots, virtual characters and SoftBots (purely software based agents) working together in a Hybrid Team to accomplish common tasks. The accompanying video shows a customized packaging scenario and can be downloaded from http://hysociatea.dfki.de/?p=441.

Thomas Bauereiß∗, Abhishek Bichhawat†, Iulia Boloşteanu‡, Peter Faymonville†, Bernd Finkbeiner†, Deepak Garg‡, Richard Gay¶, Sergey Grebenshchikov§, Christian Hammer†, Dieter Hutter∗, Ondřej Kunčar§, Peter Lammich§, Heiko Mantel¶, Christian Müller§, Andrei Popescu§,‖, Markus Rabe†, Vineet Rajani‡, Helmut Seidl§, Markus Tasch¶ and Leander Tentrup† ∗German Research Center for Artificial Intelligence (DFKI), Bremen, Germany, Email: {firstname.lastname}@dfki.de †Saarland University, Germany, Email: {lastname}@cs.uni-saarland.de ‡MPI-SWS, Saarbrücken, Germany, Email: {iulia mb, dg, vrajani}@mpi-sws.org §Technische Universität München, Germany, Email: {lastname}@in.tum.de ¶Technische Universität Darmstadt, Germany, Email: {lastname}@mais.informatik.tu-darmstadt.de ‖Dept. of Computer Science, School of Science and Technology, Middlesex University, UK, Email: a.popescu@mdx.ac.uk

Structuring theories is one of the main approaches to reduce the combinatorial explosion associated with reasoning and exploring large theories. In the past we developed the notion of development graphs as a means to represent and maintain structured theories. In this paper we present a methodology and a resulting implementation to reveal the hidden structure of flat theories by transforming them into detailed development graphs. We review our approach using plain TSTP-representations of MIZAR articles obtaining more structured and also more concise theories.

The increasing availability of smart objects demands for flexible mechanisms to orchestrate different types of these objects to smart environments. As smart objects are typically not aware of each other, an orchestrating platform has to manage common resources, to harmonize the individual behavior of the acting objects, and to combine their activities to an intelligent team work. This paper presents a corresponding framework to implement such an orchestrating platform. It provides a concurrent programming language representing states in Description Logics and state transitions as logical updates enabling deductive support to infer non-explicitly represented knowledge. It uses temporal logic to suspend execution of a process for a particular evolution of the global state that is specified by a LTL formula. Since a process can fork into subprocesses this provides a mechanism for runtime verification by splitting a process into a subprocess executing some critical program and another parallel subprocess monitoring the first one by waiting for the desired evolution of states specified in its LTL formula.

Workflow management plays an important role in analyzing and automating business processes. Security requirements in workflow management systems are typicallymapped to (role-based) access control configurations. This paper focuses on information flow control, taking into account implicit information leaks. The presented approach operates on a specification level in which no executable programis available yet. We illustrate the modeling of a workflowmanagement systemas a composition of state-event systems, each representing one of the activities of the workflow. This facilitates distributed deployment and eases verification by splitting up the verification of the overall system into verification of the individual components. Confidentiality requirements are modeled in terms of information flow predicates using the MAKS framework and verified following existing decomposition methodologies, which are adapted for open systems with ongoing user interaction. We discuss the interaction with other security requirements, notably separation of duty.

Motivated by typical security requirements of workflow management systems, we consider the integrated verification of both safety properties (e.g. separation of duty) and information flow security predicates of the MAKS framework (e.g. modeling confidentiality requirements). Due to the refinement paradox, enforcement of safety properties might violate possibilistic information flow properties of a system. We present an approach where sufficient conditions for the compatibility of safety properties and information flow security are derived by performing an information flow analysis of a monitor enforcing the safety property and applying existing compositionality results for MAKS security predicates. These conditions then guarantee that the composition of a target system with the monitor satisfies both kinds of properties. We illustrate our approach by deriving sufficient conditions for the security-preserving enforcement of separation of duty and ordered message delivery in an asynchronous communication platform.

In workflows and business processes, there are often security requirements on both the data, i.e. confidentiality and integrity, and the process, e.g. separation of duty. Graphical notations exist for specifying both workflows and associated security requirements. We present an approach for formally verifying that a workflow satisfies such security requirements. For this purpose, we define the semantics of a workflow as a state-event system and formalise security properties in a trace-based way, i.e. on an abstract level without depending on details of enforcement mechanisms such as Role-Based Access Control (RBAC). This formal model then allows us to build upon well-known verification techniques for information flow control. We describe how a compositional verification methodology for possibilistic information flow can be adapted to verify that a specification of a distributed workflow management system satisfies security requirements on both data and processes.

Provable security guarantees for software systems are highly desirable. Our work aims at improving and integrating existing formal verification techniques into a framework for the specification and verification of typical security requirements of large-scale, distributed workflow systems. Challenges include the uniform modelling of different types of security requirements, the decomposition of global security requirements into requirements on subcomponents, and the refinement of an abstract specification towards an implementation. We focus our attention on workflow management systems due to their interesting security requirements and the widespread use of model-driven techniques in this area (e.g. using BPMN diagrams). We build upon existing verification techniques for a specific notion of information flow security, and intend to apply our results to concrete example systems such as a secure web-based conference management system.

LDAP directory services are widely used to store and manage information about the assets of organisations and to ease the administration of IT infrastructure. With the popularity of cloud computing many companies start to distribute their computational needs in mixed-cloud infrastructures. However, distributing an LDAP directory including sensitive information to partially trusted cloud servers would constitute a major security risk. In this paper, we describe an LDAP replication mechanism that allows for a fine-grained selection of parts of an LDAP directory tree that are replicated to another server using content-based filters, while maintaining the availability and performance advantages of a full multi-master replication. We discuss sufficient conditions on replication topology and admissible operations such that the replication mechanism provides eventual consistency of selectively replicated data.

The algorithmic character of many clinical guidelines promoted their formal representation and use in decision support systems for giving advice in daily clinical routine. However, their typical formalization as workflow graphs restricts supervised care to a fixed set of treatment paths incapable to react on unforeseen events. Medication, for instance, constitutes a workflow on its own as an iterated process having restrictions on its duration, on the total amount of drugs to take, or the condition to stop it prematurely. Multi-morbidity gives rise to treatments following different guidelines but resulting in the need for alignment of the suggested care. Sometimes, a treatment has to deviate from the official guidelines because, for instance, the patient either refuses a designated intervention or gets an allergic reaction. Nonetheless, the remaining care should follow the guideline as close as possible. Rather than a fixed set of treatments paths encoded in a workflow graph, there is a need for a more flexible approach to react to the characteristics and needs of the individual cases. In this paper we present a new approach in which we consider care as an orchestration of various processes which altogether have to follow given clinical guidelines. The approach is based on the use of formal logics to specify the world as well as actions and processes operating in it. Workflows or other requested activities, which are encoded in clinical guidelines, are represented as temporal logical formulas. Activated as monitors they compare the actual development against the specified behavior and report once the specified behavior has been observed or the world has entered a state which violates the specification. In either case the system can actively react on such a new situation by starting new processes that deal with the occurred new situation. We illustrate our approach with the help of clinical guidelines to treat an acute coronary syndrome.

Developing ambient intelligence for a smart home living lab is a complex task. We present the SHIP-tool to define ambient intelligence processes on an adequate level of abstraction. Based on the representation of the environment in a formal logical description, communication from and to the environment is via updates of the logical description. Processes are built from basic actions to update the current logical descriptions and include means to monitor the evolution of the environment in a temporal logic formalism. The SHIP-tool implements the process language and serves both for simulation and execution of sample ambient intelligent services in a real smart home living labs also presented in the paper. Two showcases have been realized: a night surveillance service and a transportation assistance. The demonstration consisted of showing both showcases both simulated in a desktop VR environment and remotely controlling the real smart home living lab.

Our digital world is characterized by various concurrent processes that interact with the physical world. Each of them follows its own rules and goals and only few of them are under a central control. While usually a human mediates between these processes, we developed the SHIP-tool to orchestrate these processes automatically. It uses Description Logic to represent a current state, which is constantly updated by messages sent by sensors and other processes. Temporal-logical formulas act as monitors that supervise the evolution of the system. The failure or success of monitors can initiate procedures given as programs on actions and specified in a Dynamic Logic. In this paper we describe in particular the aspect of storing and maintaining the state of the system in Description Logic ontologies. We formulate restrictions on ABoxes and their updates to always ensure a constructive specification of the current state while keeping the general rules of the system (i.e the TBox and RBOX) invariant.