In the domain of Spoken Language Understanding (SLU) the primary objective is to extract important information from audio commands, like the intent of what a user wants the system to do and specific entities like locations or numbers. This paper presents a simple method that integrates intents and entities into a beam search algorithm, and, in combination with a general-purpose Speech-to-Text model, enables the creation of customized SLU-decoders without any additional training. Constructing such decoders is very fast and only takes a few seconds. It is also completely language-independent. In comparative assessments across multiple benchmarks, this method demonstrates comparable performance to several other SLU strategies, while significantly surpassing them in terms of computational speed.

This paper presents a proof technique for proving refinements for general state-based models of concurrent systems that reduces proving forward simulations to thread-local, step-local proof obligations. The approach has been implemented in our theorem prover KIV, which translates imperative programs to a set of transition rules and generates proof obligations accordingly. Instances of this proof technique should also be applicable to systems specified with ASM rules, B events, or Z operations. To exemplify the proof methodology, we demonstrate it with two case studies. The first verifies linearizability of a lock-free implementation of concurrent hash sets by showing that it refines an abstract concurrent system with atomic operations. The second applies the proof technique to the verification of opacity of Transactional Mutex Locks (TML), a Software Transactional Memory algorithm. Compared to the standard approach of proving a forward simulation directly, both case studies show a significant reduction in proof effort.

Abstract Drone formation flights, exemplified by performances such as the Intel Drone Shows, demonstrate the advancements and capabilities of current technology. This work revisits the concept of self-organization through swarm behavior for this goal, presenting 2.0 as an advanced approach in this domain. The proposed method facilitates parametrizable swarm behavior at a high level of abstraction. Building upon its predecessor, , it enables the generation of emergent effects through a single, generalized implementation, wherein only the parameters governing individual swarm members need to be adjusted. Leveraging swarm behavior for formation flight offers distinct advantages, including enhanced scalability, robustness, and flexibility. Unlike centrally coordinated approaches, swarm-based methods support the emergence of complex and dynamic formations. Notable formations include parallel swarms interacting with one another, single swarms utilizing multiple reference points to achieve novel flight patterns, and hierarchical swarm structures that further extend the range of possible configurations of swarm behavior. This paper introduces fundamental swarm behaviors that can be realized within the 2.0 framework in detail and explores their composition into more complex formations. The primary focus is the experimental and empirical evaluation of these concepts in simulated environments, including their stabilization properties when facing disturbances. In combination with previous successful pre-evaluations involving real drones it provides a strong foundation for future real-world applications of 2.0.

Assembly modeling in computer-aided design (CAD) refers to designing new products based on a collection of preexisting individual parts. To streamline this process, designers would benefit from recommendations for parts needed next, tailored to a specific extension point within the design. By their nature, assemblies can be represented as undirected graphs over parts. As parts of an assembly can be inserted in any order, we employ graph neural networks (GNNs) that are invariant to permutations. In terms of graph machine learning, the problem of localized part recommendation does not match traditional formulations such as link prediction or purely generative tasks that mostly focus on generating graphs with specific statistical properties on a macro-level. Instead, a novel approach is required that integrates the prediction of parts along with their connection to the existing graph at a specific node. In this problem setting, we investigate two distinct use cases: predicting new parts for a given partial design and user-selected extension point, as well as recommending both a new part and its extension point within the existing design. Our experiments indicate that our approaches significantly reduce the cognitive burden for designers: When recommending ten potential next parts, they included the needed part in up to 97.5% of cases for the first and both the part and its location in up to 92.0% for the second use case.

The manufacturing industry is undergoing a significant transformation in the context of Industry 4.0, and production is shifting from mass products to individual products of batch size one. Moreover, the increasing complexity of components, e.g., due to additive manufacturing, makes the testing setups of components even more complex. Due to the low quantities of the components, it is not profitable to build test benches for each individual component to test a large number of different forces and torsions to ensure the needed product quality. In order to be able to test various components flexibly through different motions, we developed a concept to perform robot-based destructive component testing with industrial robots. The six degrees of freedom and the broad working range of an industrial robot make it possible to apply forces and torques to different products. Since industrial robots cannot apply the same forces and torques in all axis positions, a position must be calculated whe re the specimen can be tested. Therefore, we propose an approach for automatic specimen placement, which includes a format to map applicable forces and torques of industrial robots. Furthermore, we present an algorithmic approach to execute an automatic feasibility check for the required test motions and an automatic specimen placement using an exemplary robot-based component testing bench.

Resin transfer molding (RTM) is a composite manufacturing process that uses a liquid polymer matrix to create complex-shaped parts. There are several challenges associated with RTM. One of the main challenges is ensuring that the liquid polymer matrix is properly distributed throughout the composite material during the molding process. If the matrix is not evenly distributed, the resulting part may have weak or inconsistent properties. This is the challenge we tackle with the approach presented in this work. We implement an online control using deep reinforcement learning (RL) to ensure a complete impregnation of the reinforcing fibers during the injection phase, by controlling the input pressure on different inlets. This work uses this self-learning paradigm to actively control the injection of an RTM process, which has the advantage of depending on a reward function instead of a mathematical model, which would be the case for model predictive control. A reward function is more straightforward to model and can be applied and adapted to more complex problems. RL algorithms have to be trained through many iterations, for which we developed a simulation environment with a distributed and parallel architecture. We show that the presented approach decreases the failure rate from 54 % to 27 %, by 50 % compared to the same setup with steady parameters.

A key aspect of industry 4.0 is the transition of production to batch size one and consequently unique dimensions and structures of components for each product. Since many components are only available in small quantities it is not feasible to design expensive test benches for each of these components, however it is still important to test them to ensure the quality of each individual component. Therefore, we propose an approach for a flexibly programmable robotic test bench for destructive component testing of various components. This includes a concept for planning and execution of different test movements in a component test on robotic test benches and a unified data platform for controlling sensor-based motions as well as the recording of test data.

With the recent advance in speech technology, smart voice assistants have been improved and are now used by many people. But often these assistants are running online as a cloud service and are not always known for a good protection of users' privacy. This paper presents the architecture of a novel voice assistant, called Jaco, with the following features: (a) It can run completely offline, even on low resource devices like a RaspberryPi. (b) Through a skill concept it can be easily extended. (c) The architectural focus is on protecting users' privacy, but without restricting capabilities for developers. (d) It supports multiple languages. (e) It is competitive with other voice assistant solutions. In this respect the assistant combines and extends the advantages of other approaches.

When developing file systems, caching is a common technique to achieve a performant implementation. Integrating write-back caches is not primarily a problem for functional correctness, but is critical for proving crash safety. Since parts of written data are stored in volatile memory, special care has to be taken when integrating write-back caches to guarantee that a power cut during a running operation leads to a consistent state. This article shows how non-order-preserving caches can be added to a virtual file system switch (VFS) and gives a novel crash-safety criterion matching the characteristics of such caches. Broken down to individual files, a power cut can be explained by constructing an alternative run, where all writes since the last synchronization of that file have written a prefix. VFS caches have been integrated modularly into Flashix, a verified file system for flash memory, and both functional correctness and crash-safety of this extension have been verified with the interactive theorem prover KIV.

Industrial manufacturing is currently undergoing a transformation from mass production with inflexible production systems to individual production with adaptable cells. In order to ensure this adaptability of these systems, technologies such as plug & produce are needed, to integrate, modify and remove devices at runtime. Therefor an exact description of the system, the products and the capabilities / skills of the devices is essential as well as a network for communication between the devices. Deterministic data transmission is particularly important for distributed control systems. We propose an architecture for plug & produce mechanisms with hard real-time capable communication paths between the cyber-physical components using OPC UA PubSub over TSN and the ability to load and execute real-time critical tasks at runtime.

In this work, we describe a ROS-based method for whole-body control (WBC) of mobile manipulators in the context of safe human-robot interaction. Our method is based on cyclic quadratic programming (QP) with a set of simultaneously active tasks that define constraints. The importance of different tasks is captured through priorities and weights. Robot behavior can be changed at run-time by re-configuring the active tasks through ROS interfaces. We evaluate the suitability of our method for safe human-robot collaboration in a Gazebo simulation. We show that our method lets the mobile manipulator perform evasive motions while staying consistent with other tasks if possible. At the same time, self-collisions and static obstacles are avoided. If a given safety threshold is crossed, the robot comes to a safe stop. Operation continues once the distance is high enough again.

Setting up fiber-threading for a pultrusion line is tedious, error prone and takes a long time. Between 100 and 1000 fibers have to be arranged into a two-dimensional shape, which have to be threaded between several support plates without causing crossovers. When manually planning this process based on intuition, it is hard to keep track of the complexity. This slows the process down to where it can take several hours or several days, and shortening this duration reduces the cost considerably. As planning the setup takes up a large chunk of time, we are proposing a simulation and an algorithm to automatically calculate how the fiber bundles need to be threaded from the creels through the support plates to result in the desired shape. Using a three-dimensional simulation for collision detection in conjunction with a genetic algorithm, we are able to shorten the planning of the fibers to around 10 minutes on a modern 8-core personal computer. Based on this data, further work can be done to further improve, visualize or permanently store the data in a digitized company.

The inspection of large structures is increasingly carried out with the help of Unmanned Aerial Vehicles (UAVs). When navigating relative to the structure, multiple data sources can be used to determine the position of the UAV. Examples include track data from an installed camera and sensor data from the orientation sensors of the UAV. This paper deals with the fusion of this data and its use for navigation alongside the structure. For the sensor fusion, a concept is developed using a Kalman filter and evaluated simulatively in a prototype. The calculated position data are also fed into a vector flight control system, which dynamically calculates and flies a trajectory along the component using the potential field method. This is done taking into account obstacles detected by the onboard sensors of the UAV. The established concept is then implemented with the Robot Operating System (ROS) and evaluated simulatively.

Carbon fiber reinforced polymers (CFRP) offer highly desirable properties such as weight-specific strength and stiffness. Liquid composite moulding (LCM) processes are prominent, economically efficient, out-of-autoclave manufacturing techniques and, in particular, resin transfer moulding (RTM), allows for a high level of automation. There, fibrous preforms are impregnated by a viscous polymer matrix in a closed mould. Impregnation quality is of crucial importance for the final part quality and is dominated by preform permeability. We propose to learn a map of permeability deviations based on a sequence of camera images acquired in flow experiments. Several ML models are investigated for this task, among which ConvLSTM networks achieve an accuracy of up to 96.56%, showing better performance than the Transformer or pure CNNs. Finally, we demonstrate that models, trained purely on simulated data, achieve qualitatively good results on real data.

A key aspect of Industry 4.0 is the continuous interconnectedness of components. The standardized industrial communication protocol OPC UA offers a solution to this problem by enabling the exchange of data between the shop floor level and the inter-enterprise level. Due to the integration of the Time Sensitive Network (TSN) into OPC UA, it is now even possible to exchange information in real-time. Especially on the shop floor, there are numerous heterogeneous distributed devices from sensors to robots which must communicate with each other in real-time to achieve a distributed industrial control. Therefore, we propose an approach to combine real-time communication over TSN with OPC UA Programs to synchronize multiple distributed OPC UA Programs and exchange process data between them without losing real-time guarantees. This can be seen as the enabler of Plug-and-Produce with real-time requirements.

Components made from carbon fiber reinforced plastics (CFRP) offer attractive stability properties for the automotive or aerospace industry despite their light weight. To automate CFRP production, resin transfer molding (RTM) based on thermoset plastics is commonly applied. However, this manufacturing process has its shortcomings in quality and costs. The project CosiMo aims for a highly automated and cost-attractive manufacturing process using cheaper thermoplastic materials. In a thermoplastic RTM (T-RTM) process, the polymerization of ε-caprolactam to polyamide 6 is investigated using an intelligent mold tooling. Multiple sensor types integrated into the mold allow for tracking of process-relevant variables, such as material flow and polymerization state. In addition to monitoring the T-RTM process, a digital twin visualizes progress and makes predictions about issues and countermeasures based on machine learning.

Automation mechanisms are increasingly established in the field of visual inspections. UAVs can be used for particularly large components, such as those used in ship production and for critical infrastructures. This paper concentrates on the problem of visual inspection in the field of perspective-dependent route planning. It is shown how the requirements for such a system can be implemented and elaborated. Furthermore we investigate how sensor positions can be calculated offline, based on optical and geometrical requirements and how a trajectory can be planned which contains the found sensor positions for each given area on the component. It is shown how the systems architecture can be designed in order to be able to adapt it to different requirements for the planning of sensor positions and trajectory. The implementation was tested in a simulation environment, evaluated using a benchmark data set and it was shown how above-average results can be achieved on this data set.

Multi-functional cells with cooperating teams of robots promise to be flexible, robust, and efficient and, thus, are a key to future factories. However, their programming is tedious and AI-based planning for multiple robots is computationally expensive. In this work, we present a modular and efficient two-layer planning approach for multi-robot assembly. The goal is to generate the program for coordinated teams of robots from an (enriched) 3D model of the target assembly. Although the approach is both motivated and evaluated with LEGO, which is a challenging variant of blocks world, the approach can be customized to different kinds of assembly domains.

Smart factories of the future will be equipped with dynamic and task-specific teams of robots in order to manufacture custom-tailored products.For this, it is necessary to facilitate the planning of appropriate task sequences for cooperating robots.In this paper, we introduce a modular and domain-guided planning approach for multiple robots.Due to its modularity, the approach can be adapted to different assembly problems.Moreover, domain knowledge is used to guide the planning towards feasible solutions.We evaluate the approach with different examples from the blocks world domain (i.e. LEGO R DUPLO R ).This evaluation shows that this domain-guided approach outperforms classical planning based on state space search such as A * .

Considering initiatives like Industry 4.0 or the Industrial Internet of Things, robots will play an important role in intelligent factories, producing highly customized products with high variability and in small lot sizes. In this setting, complexity of planning and programming such robotic applications grows due to the drastic increase in flexibility, performance and robustness required. In this paper, we propose a tool-supported methodology for the development of control software for dynamically forming multi-functional robot teams. The main challenges for achieving this overall goal are modeling of robot team skills, techniques for automatically deriving process steps from the products’ construction plans, finding allocations of those steps to possible robot teams with compatible skills and calculating collision-free execution schedules with a high degree of parallelization to improve cycle times. The proposed approach integrates process experts and automation experts on all level s. Two case studies will serve as test beds to the developed approach: production of carbon-fiber reinforced polymers and assembly of furniture.

When automating small-batch manufacturing processes, the time spent for process planning and robot programming becomes more important.This paper proposes an automated process including construction plan analysis, process planning and execution to reduce the amount of manual work required.The process starts by analyzing the structure of the desired product and deriving required process step results, then uses heuristic search to find possible production steps and task assignments, and concludes by simulating or executing the resulting production plan.The approach is evaluated on a case study with a simulated robot automatically building different LEGO R DUPLO R structures starting from a 3D model defining the desired product.

Abstract This paper reports on our experiences of applying S# (“safety sharp”) to model and analyze the case study “hemodialysis machine.” The S# safety analysis approach focuses on the question, what happens if we place a controller with correct software into an unreliable environment. To answer that question, the S# toolchain natively supports the Deductive Cause Consequence Analysis, a fully automatic model checking‐based safety analysis technique that determines all sets of component faults with the potential of causing a system hazard. Furthermore, S# can give an approximate estimate of the hazard's probability. To demonstrate our approach, we created a model with a simplified controller of the hemodialysis machine and relevant parts of its environment and performed a safety analysis using Deductive Cause Consequence Analysis.

Many applications that handle private or confidential data release part of this data in a controlled manner through filter functions.However, it can be difficult to reason formally about exactly what or how much information is declassified.Often, anonymity is measured by reasoning about the equivalence classes of all inputs to the filter that map to the same output.An observer or attacker that sees the output of the filter then only knows that the secret input belongs to one of these classes, but not the exact input.We propose a technique suitable for complex filter functions together with a proof method, that additionally can provide meaningful guarantees.We illustrate the technique with a DistanceTracker app in a leaky and a non-leaky version.

Recently, the need for safe human-robot-interaction has become increasingly important, and with it the requirement to reliably detect persons in the workspace of a robot. Capacitive sensors mounted to the robot structure can be used to measure the presence of conductive objects and, hence, allow the detection of persons. However, various objects in the workspace can influence capacitive sensor measurements. Thus, we propose to record an environment model containing the expected sensor values for relevant robot poses. Using this model, distance estimation and real-time reaction can be performed even in the presence of additional conductive objects in the workspace. A demonstration of our approach was shown at the Hannover Messe 2015.

Multi-functional robot cells will play an important role in smart factories of the future.Equipped with flexible toolings, teams of robots will be able to realize manufacturing processes with growing complexity.However, to efficiently support small batch sizes and a multitude of process variants, powerful software tools are required.This paper illustrates the challenges that developers face in multi-functional robot cells, using the example of CFRP production.The vision of a new programming environment for such future flexible automation systems is sketched.

Simple robot applications can be run on a single computer, but when it comes to more complex applications or multiple mobile robots, software distribution becomes important.When structuring mobile robot systems and applications, distribution has to be considered on various levels.This paper proposes to distinguish between real-time level, system level, application level and regarding the world model.Advantages and disadvantages of distribution on each level are analyzed, and examples are given how this distribution is realized in the robotics frameworks OROCOS, ROS and the Robotics API.The results are demonstrated using a case study of two cooperating youBots handing over a work-piece while in motion, which is shown in simulation as well as in real life.

Resource allocation is a common problem in many technical systems. In multi-agent systems, the decentralized or regionalized solution of this problem usually requires the agents to cooperate due to their limited resources and knowledge. At the same time, if these systems are of large scale, scalability issues can be addressed by a self-organizing hierarchical system structure that enables problem decomposition and compartmentalization. In open systems, various uncertainties—introduced by the environment as well as the agents’ possibly self-interested or even malicious behavior—have to be taken into account to be able to allocate the resources according to the actual demand. In this article, we present a trust- and cooperation-based algorithm that solves a dynamic resource allocation problem in open systems of systems. To measure and deal with uncertainties imposed by the environment and the agents at runtime, the algorithm uses the social concept of trust. In a hierarchical setting, we additionally show how agents create constraint models by learning the capabilities of subordinate agents if these are not able or willing to disclose this information. Throughout the article, the creation of power plant schedules in decentralized autonomous power management systems serves as a running example.

Resource allocation is a task frequently encountered in energy management systems such as the coordination of power generators in a virtual power plant (unit commitment).Standard solutions require fixed parametrised optimisation models that the participants have to stick to without leaving room for tailored behaviour or individual preferences.We present a modelling methodology that allows organisations to specify optimisation goals independently of concrete participants and participants to craft more detailed models and state individual preferences.While considerable efforts have been spent on devising efficient control algorithms and detailed physical models in power management systems, practical aspects of unifying several heterogeneous models for optimisation have been widely ignored -a gap we aim to close.As a by-product, we give a formulation of warm and cold start-up times for power plants that improves existing power plant models.The concepts are detailed with the loaddistribution problem faced in virtual power plants and evaluated on several random instances where we observe that a significant number of soft constraints of individual actors can be satisfied if considered. I. CONSTRAINT OPTIMISATION PROBLEMS IN POWER SYSTEMSR ESOURCE allocation and scheduling are difficult prob- lems that occur frequently in energy systems, be it the coordination of power generation [1], demand-side management, or building control software.In a producer-based view, supply needs to meet the demand as accurately as possible in order to guarantee stability and avoid costs incurred by corrective measures.Similarly, consumers may try to find cost-minimising schedules for processes required throughout a day with respect to time-dependent energy prices.Current initiatives 1 are based on the assumption that groups of prosumers (i.e., energy producers and/or consumers) can form and team up to achieve better prices or production rates for their participants.We also adopt the notion of agents, indicating that the prosumers are in principle autonomous entities, even if they surrender the decision about their power output to the group.A straightforward solution (see, e.g., [2], [3], [4], [5]) to this resource allocation problem is to model the decision making process (e.g., distributing the load in a virtual power plant (VPP) or scheduling energy-consuming domestic processes in a consumer coalition) as a mathematical optimisation problem such as a mixed integer program (MIP), a linear program

Many resource allocation problems are hard to solve even with state-of-the-art constraint optimisation software upon reaching a certain scale.Our approach to deal with this increasing complexity is to employ a hierarchical "regio-central" mechanism.It requires two techniques: (1) the synthesis of several models of agents providing a certain resource into a centrally and efficiently solvable optimisation problem and (2) the creation of an abstracted version of this centralised model that reduces its complexity when passing it on to higher layers.We present algorithms to create such synthesised and abstracted models in a fully automated way and demonstrate empirically that the obtained solutions are comparable to central solutions but scale better in an example taken from energy management. 15

Partial constraint satisfaction and soft constraints enable to deal with over-constrained problems in practice. Constraint relationships have been introduced to provide a qualitative approach to specifying preferences over the constraints that should be satisfied. In contrast to quantitative approaches like weighted or fuzzy CSPs, the preferences just rely on a directed acyclic graph. The approach is particularly aimed at scenarios where soft-constraint problems stemming from several independently modeled agents have to be aggregated into one problem in a multi-agent system. Existing transformations into weighted CSP introduce unintended, additional preference decisions. We first illustrate the application of constraint relationships in a case study from energy management along with deficiencies of existing work. We then show how to embed constraint relationships into the soft constraint frameworks of partial valuation structures and further c-semi rings by means of free constructions. We finally provide a prototypical implementation of heuristics for the well-known branch-and-bound algorithm along with an empirical evaluation.

Knowledge about the current state of the system serves at least two purposes: it is the basis for decisions to act and adapt to ensure reliable operation and it can be used to verify the correctness of the system at runtime. Both purposes require that current information is available at runtime that can be evaluated. Thus, the system designers have to create a complex monitoring infrastructure that suits the purposes of the system. We propose a combination of proven techniques that can be used as the basis for such a monitoring infrastructure. We combine it with a model-driven approach that allows a model transformation of information contained in the requirements and design documents to implementations of observers and controllers that allow adaptation at runtime based on current information as well as runtime verification. The approach can be easily integrated into an iterative-incremental software engineering process and is illustrated with two complex case studies.

Nietzsche describes what is at the core of the concept of trust as it is used in agent societies and self-organising systems. Trust describes the expectation of one entity that the other behaves according to a set of rules. If that trust is broken, it is very hard to repair. If it exists, however, it is the basis of cooperation and enables a collective effort that gives a society purpose and allows it to succeed in its respective goals. Self-organisation is often at the root of such collective efforts as it allows the restructuring of a society to adapt to changing objectives, a changing environment, and new cooperation partners. Trust arises in such systems from the interactions of agents and the experiences of attempts to collaborate. It is thus only natural to regard trust and self-organisation together and explore the concepts' relation.

The development of a secure service application is a difficult task and designed protocols are very error-prone. To develop a secure SOA application, application-independent protocols (e.g. TLS or Web service security protocols) are used. These protocols guarantee standard security properties like integrity or confidentiality but the critical properties are applicationspecific (e.g. “a ticket can not be used twice”). For that, security has to be integrated in the whole development process and application-specific security properties have to be guaranteed. This paper illustrates the modeling of a security-critical service application with UML. The modeling is part of an integrated software engineering approach that encompasses model-driven development. Using the approach, an application based on service-oriented architectures (SOA) is modeled with UML. From this model executable code as well as a formal specification to prove the security of the application is generated automatically. Our approach, called SecureMDD, supports the development of security-critical applications and integrates formal methods to guarantee the security of the system. The modeling guidelines are demonstrated with an online banking example.

Open, heterogeneous multi-agent systems (MAS) have to cope with a variety of uncertainties introduced by the systems' participants and their environment. In such systems, agents can use trust values that characterize the behavior of their interaction partners as a measure of uncertainty, allowing agents to make more appropriate decisions. However, because of the systems' dynamics and the agents' limited knowledge, the accuracy of these trust values is often limited as well, introducing another form of uncertainty. In this paper, we present confidence as a general concept to indicate the degree of certainty that a trust value describes the actual observable behavior of an agent. On the basis of three open MAS, we identify different criteria the confidence depends on by revealing situations in which trust values can be inaccurate and therefore impair an agent's decision. By means of scenarios, we show that a trust-aware agent can increase its own utility when its decisions are based on the confidence in trust values.

This paper presents a logic that extends basic ITL with explicit, interleaved programs. The calculus is based on symbolic execution, as previously described. We extend this former work here, by integrating the logic with higher-order logic, adding recursive procedures and rules to reason about fairness. Further, we show how rules for rely-guarantee reasoning can be derived and outline the application of some features to verify concurrent programs in practice. The logic is implemented in the interactive verification environment KIV.

Abstract Linearizability is a global correctness criterion for concurrent systems. One technique to prove linearizability is applying a composition theorem which reduces the proof of a property of the overall system to sufficient rely-guarantee conditions for single processes. In this paper, we describe how the temporal logic framework implemented in the KIV interactive theorem prover can be used to model concurrent systems and to prove such a composition theorem. Finally, we show how this generic theorem can be instantiated to prove linearizability of two classic lock-free implementations: a Treiber-like stack and a slightly improved version of Michael and Scott’s queue.

Formal verification can give more confidence in the security of cryptographic protocols. Application specific security properties like "The service provider does not loose money" can give even more confidence than standard properties like secrecy or authentication. However, it is surprisingly easy to get a meaningful property slightly wrong. The result is that an insecure protocol can be 'proven' secure. We illustrate the problem with a very small application, a copy card, that has only five different messages. The example is taken from a paper where the protocol is secure, but the proved property slightly wrong. We propose to solve the problem by incorporating more of the real-world application into the formal model.

During the last two decades, software development has evolved continuously into an engineering discipline with systematic use of methods and tools to model and implement software. For example, object-oriented analysis and design is structuring software models according to real-life objects of the problem domain and their relations. However, the industrial robotics domain is still dominated by old-style, imperative robot programming languages, making software development difficult and expensive. For this reason, we introduce the object-oriented Robotics Application Programming Interface (Robotics API) for developing software for industrial robotic applications. The Robotics API offers an abstract, extensible domain model and provides common functionality, which can be easily used by application developers. The advantages of the Robotics API are illustrated with an application example.

In this paper we introduce our model-driven software engineering method, called SecureMDD, which facilitates the development of security-critical applications that are based on cryptographic protocols. The approach seamlessly integrates the generation of code and formal methods. Starting with a platform-independent UML model of a system under development, we generate executable Java (Card) code as well as a formal model from the UML model. Subsequent to this, the formal model is used to verify the security of the modeled system. Our goal is to prove that the generated code is correct w.r.t. the generated formal model in terms of formal refinement. The approach is tailored to the domain of security-critical systems, e.g. smart card applications.

The application of industrial robots is strongly limited by the use of old-style robot programming languages. Due to these languages, the development of robotic software is a complex and expensive task requiring technical expertise and time. Hence, the use of industrial robots is often not a question of technical feasibility but of economic efficiency. This paper introduces a new architectural approach making available modern concepts of software engineering for industrial robots. The core idea is to hide the real-time critical robot control from application developers. Instead, common functionality is provided by a generic and extensible application programming interface and can be easily used. Hence, this approach can lead to an industrialization of software development for industrial robotics.

Abstract The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results. First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study. Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework for defining such protocols based on abstract state machines (ASMs). We prove the refinement using a forward simulation.

The next generation of embedded computing systems will have to meet new challenges. The systems are expected to act mainly autonomously, to dynamically adapt to changing environments and to interact with one another if necessary. Such systems are called organic. Organic Computing systems are similar to autonomic computing systems. In addition Organic Computing systems often behave life-like and are inspired by nature/biological phenomena. Design and construction of such systems brings new challenges for the software engineering process. In this paper we present a framework for design, construction and analysis of organic computing systems. It can facilitate design and construction as well as it can be used to (semi-)formally define organic properties like self-configuration or self-adaptation. We illustrate the framework on a real-world case study from production automation.

Developing security-critical applications is very difficult and the past has shown that many applications turned out to be erroneous after years of usage. For this reason it is desirable to have a sound methodology for developing security-critical e-commerce applications. We present an approach to model these applications with the Unified Modeling Language (UML) [1] extended by a UML profile to tailor our models to security applications. Our intent is to (semi-) automatically generate a formal specification suitable for verification as well as an implementation from the model. Therefore we offer a development method seamlessly integrating semi-formal and formal methods as well as the implementation. This is a significant advantage compared to other approaches not dealing with all aspects from abstract models down to code. Based on this approach we can prove security properties on the abstract protocol level as well as the correctness of the protocol implementation in Java with respect to the formal model using the refinement approach. In this paper we concentrate on the modeling with UML and some details regarding the transformation of this model into the formal specification. We illustrate our approach on an electronic payment system called Mondex [10]. Mondex has become famous for being the target of the first ITSEC evaluation of the highest level E6 which requires formal specification and verification.

An important property of embedded systems is dependability. Today this addresses mostly safety and reliability. Guaranteeing these properties is normally done by adding redundancy to the system. This approach is expensive and can not cope with changing environments. Therefore new designs are researched, which allow systems to self-adapt and self-heal. For broad acceptance in industry it is important, that organic systems can be modeled and analyzed with standard modeling tools and languages. We present a case study of an adaptive production automation cell modelled in the Lustre language using the SCADE suite and the verification of functional properties. SCADE is used widely in industry, especially in safety critical applications. Being able to model and verify adaptive systems in SCADE could increase their acceptance for these target areas.

There is a mismatch between the data format used in implementations of security protocols and the data types used in formal verification of security protocols. We present a verified encoding scheme for data used in security protocols, which links the abstract data types of the formal world to a byte format usable in implementations. The encoding is inspired by the ASN1 encoding scheme. The encoding is implemented in Java and the implementation is proven to be correct against a formal specification. The implementation can be used as a reusable reference library in security protocol implementations. The benefit is a separation of concerns: The protocol can be verified on an abstract level. The mapping to bytes is automatically correct by linking the library. Additionally the encoding is a challenging Java verification case study in its own.

In this paper we present a technique for safety analysis of self-adaptive systems with formal methods. Self-adaptive systems are characterized by the ability to dynamically (self-)adapt and reorganize. The aim of this approach is to make the systems more dependable. But in general it is unclear how big the benefit is compared to a traditional design. We propose a dependability analysis based on the results of safety analysis to measure the quality of self-x capabilities of an adaptive system with formal methods. This is important for unbiased and evidence-based decision making in early design phases. To illustrate the results we show the application of the method to a case study from the domain of production automation.

This paper presents an approach to the verification of large Java programs. The focus lies on programs that implement a distributed communicating system e.g. in a M- or E-commerce scenario. When trying to verify such programs, thousands of Java classes with tens of thousands of lines of code would have to be taken into consideration. That is impossible. The paper introduces a technique that dramatically reduces the amount of source code that must be considered. Additionally, a suitable method for programming security critical systems is introduced. The reduction is achieved by extracting a verification kernel from the program, which is sufficient for proving the correctness of the relevant part. An algorithm for the automatic computation of the verification kernel has been developed and is presented in the paper. The correctness of the verification kernel approach is proved on the level of the Java language semantics.

We present a new form of quantitative safety analysis -safety optimization. This method is a combination of fault tree analysis (FTA) and mathematical optimization techniques. With the use of the results of FTA, statistics, and a quantification of the costs of hazards, it allows to find the optimal configuration of a given system with respect to opposed safety requirements. Furthermore, the system may not only be examined for safety, but usability as well. We illustrate this method on a real-world case study: the height control system of the Elbtunnel in Hamburg. Safety optimization showed some significant problems in trustworthiness of the system, yielded optimal values for configuration of free parameters and showed possible modifications to improve the system.

We present two generic formal security models for operating systems of multiapplicative smart cards. The models formalize the main security aspects of secrecy, integrity, secure communication between applications and secure downloading of new applica

Current techniques for interactively proving temporal properties of concurrent systems translate transition systems into temporal formulas by introducing program counter variables. Proofs are not intuitive, because control flow is not explicitly considered. For sequential programs symbolic execution is a very intuitive, interactive proof strategy. In this paper we will adopt this technique for parallel programs. Properties are formulated in interval temporal logic. An inplementation in the interactive theorem prover KIV has shown that this technique offers a high degree of automation and allows simple, local invariants.

Investigates an algebraic specification method for abstract data types which is designed for the application in formal software development. The specification language is full first-order logic, and the semantics of a specification is the class of its generated models. Full first-order specifications are more flexible than Horn clause specifications and exhibit better deductive properties. The author presents criteria for the correctness of full first-order specifications and for the incremental development of large specifications from smaller ones.>