Formal Modeling and Verification of Cyber-Physical Systems

Frontmatter

Verification of Embedded Real-time Systems

Abstract

Real-time systems are systems where the correctness does not only depend on their correct functioning but also on meeting realtime constraints. Such systems are often deployed in safety-critical applications, for example in airplanes, trains, or automotive systems. There, a failure may result in enormous costs or even in human injuries or loss of lifes. As a consequence, systematic verification and validation of real-time systems is a crucial issue.

The main application area for real-time systems are embedded applications, where the system controls technical processes that also evolve in real-time. Such systems are usually composed of deeply integrated hardware and software components, and they are developed under severe resource limitations and high quality requirements. In connection with the steadily increasing demands on multi-functioning and flexibility, analog control components are more and more replaced by complex digital HW/SW systems.

A major challenge is to develop automated quality assurance techniques that can be used for the verification and validation of complex embedded real-time systems that consist of both hardware and software. In this chapter, we give an overview over our research contributions to this topic. In particular, we present our framework for the verification of safety and timing properties of digital embedded real-time systems, which are modeled in SystemC, using timed automata and the UPPAAL model checker.

Paula Herber, Sabine Glesner

MARTE/CCSL for Modeling Cyber-Physical Systems

Abstract

Cyber Physical Systems (CPS) combine digital computational systems with surrounding physical processes. Computations are meant to control and monitor the physical environment, which in turn affects the computations. The intrinsic heterogeneity of CPS demands the integration of diverse models to cover the different aspects of systems. The UML proposes a great variety of models and is very commonly used in industry even though it does not prescribe a particular way of using those models together. The MARTE profile proposes a set of extensions to UML in a bid to allow for the modeling of real-time and embedded systems (RTES). Yet CPS are a wider class of systems than mere RTES. Hence a legitimate question arises as whether MARTE can be used for CPS as well. This paper illustrates some possible uses of MARTE to model CPS and uses logical clocks as a way to bring together the different models.

Frédéric Mallet

An Introduction to Hybrid Automata, Numerical Simulation and Reachability Analysis

Abstract

Hybrid automata combine finite state models with continuous variables that are governed by differential equations. Hybrid automata are used to model systems in a wide range of domains such as automotive control, robotics, electronic circuits, systems biology, and health care. Numerical simulation approximates the evolution of the variables with a sequence of points in discretized time. This highly scalable technique is widely used in engineering and design, but it is difficult to simulate all representative behaviors of a system. To ensure that no critical behaviors are missed, reachability analysis aims at accurately and quickly computing a cover of the states of the system that are reachable from a given set of initial states. Reachability can be used to formally show safety and bounded liveness properties. This chapter outlines the major concepts and discusses advantages and shortcomings of the different techniques.

Goran Frehse

Model Checking and Model-Based Testing in the Railway Domain

Abstract

This chapter describes some approaches and emerging trends for verification and model-based testing of railway control systems. We describe state-of-the-art methods and associated tools for verifying interlocking systems and their configuration data, using bounded model checking and k-induction. Using real-world models of novel Danish interlocking systems, it is exemplified how this method scales up and is suitable for industrial application. For verification of the integrated HW/SW system performing the interlocking control tasks, a modelbased hardware-in-the-loop testing approach is presented. The trade-off between complete test strategies capable of uncovering every error in implementations of a given fault domain on the one hand, and on the other hand the unmanageable load of test cases typically created by these strategies is discussed. Pragmatic approaches resulting in manageable test suites with good test strength are explained. Interlocking systems represent just one class of many others, where concrete system instances are created from generic representations, using configuration data for determining the behaviour of the instances. We explain how the systematic transition from generic to concrete instances in the development path is complemented by associated transitions in the verification and testing paths.

Anne E. Haxthausen, Jan Peleska

Modeling Unknown Values in Test and Verification

Abstract

With increasing complexities and a component-based design style the handling of unknown values (e. g., at the interface of components) becomes more and more important in electronic design automation (EDA) and production processes. Tools are required that allow an accurate modeling of unknowns in combination with algorithms balancing exactness of representation and efficiency of calculation. In the following, state-ofthe-art approaches are described that enable an efficient and successful handling of unknown values using formal techniques in the areas of Test and Verification.

Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf Wimmer

Specification of Parametric Monitors

Quantified Event Automata versus Rule Systems

Abstract

Specification-based runtime verification is a technique for monitoring program executions against specifications formalized in formal logic. Such logics are usually temporal in nature, capturing the relation between events occurring at different time points. A particular challenge in runtime verification is the elegant specification and efficient monitoring of streams of events that carry data, also referred to as parametric monitoring. This paper presents two parametric runtime verification systems representing two quite different approaches to the problem. qea (Quantified Event Automata) is a state machine approach based on trace-slicing, while LogFire is a rule-based approach based on the Rete algorithm, known from AI as being the basis for many rule systems. The presentation focuses on how easy it is to specify properties in the two approaches by specifying a collection of properties gathered during the 1st International Competition of Software for Runtime Verification (CSRV 2014), affiliated with RV 2014 in Toronto, Canada.

Klaus Havelund, Giles Reger

Advances in Design Automation Techniques for Digital-Microfluidic Biochips

Abstract

Due to their emergence as an efficient platform for pointof-care clinical diagnostics, digital-microfluidic biochips (DMFBs) have received considerable attention in recent years. They combine electronics with biology, and they integrate various bioassay operations, such as sample preparation, analysis, separation, and detection. In this chapter, we first present an overview of digital-microfluidic biochips. We next describe emerging computer-aided design (CAD) tools for the automated synthesis and optimization of biochips from bioassay protocols. The chapter includes solutions for fluidic-operation scheduling, module placement, droplet routing, and pin-constrained chip design. We also show how recent advances in the integration of sensors into a DMFB can be exploited to provide cyberphysical system adaptation based on feedback-driven control.

Mohamed Ibrahim, Zipeng Li, Krishnendu Chakrabarty

Intuitive Interaction with Robots – Technical Approaches and Challenges

Abstract

A challenging goal in human-robot interaction research is to build robots that are intuitive interaction partners for humans. Although some research does focus on building robots which look and behave exactly like a human, even simple toylike robots can be accepted as adequate and intuitive interaction partners. However, for complex interaction tasks, intelligent support, or cooperative behavior more advanced and ”on board” solutions have to be developed, that still support natural interaction behavior between human and robot. This chapter will discuss some relevant research in the field of human-robot interaction which is fundamental for more complex but still intuitive interaction. The focus is to convey the complexity of research that is required and to point out different research areas which are relevant to achieve the goal of developing robots that can be natural interaction partners for humans.

Elsa Andrea Kirchner, Jose de Gea Fernandez, Peter Kampmann, Martin Schröer, Jan Hendrik Metzen, Frank Kirchner

Physical Safety in Robotics

Abstract

Over the last decade, safe physical Human-Robot Interaction (pHRI) has been made possible due to significant advances in mechatronics, control, and planning. One result of these developments were fully integrated safer lightweight robots that are equipped with sophisticated interaction control capabilities. These new robots have even opened up novel and unforeseen application domains, in which human and robot are sought to work and interact with each other. For this, safe physical interaction is prime. This chapter gives a brief overview on two of its central aspects: human safety from an injury and standards standpoint, and control for physical interaction with focus on interaction control and collision handling.

Sami Haddadin

In-circuit Error Detection with Software-based Error Correction – An Alternative to TMR

Abstract

FPGAs are often utilized in space avionics. To protect the FPGA application data against radiation effects in space, data redundancy can be used. A well-known method is to triplicate the circuit and eliminate the erroneous circuit output with a local voter (TMR). Alternatively, in-circuit error detection with software-based error correction can be used, if the FPGA works as a co-module next to a processor running the mission software. In this work, we present an implementation of this method on a commonly used spacecraft data handling architecture.

Gökçe Aydos, Görschwin Fey

Behavior Driven Development for Tests and Verification

Abstract

Nowadays, hardware is usually tested and verified at postdesign time. The bottom line is that more effort is spend in the validation phases than in the implementation, because it is harder to fix bugs in later design stages than during the implementation of the design. In contrast, test-first approaches such as test driven development (TDD) have become increasingly important for software development. Behavior driven development (BDD) extends TDD by using natural language style scenarios to describe tests. But both approaches miss formal verification methods which are very important in hardware design. This research project presents a new approach based on BDD that combines testing and verification seamlessly.

Melanie Diepenbeck, Rolf Drechsler

Semantic Object Recognition Based on Qualitative Probabilistic Spatial Relations

Abstract

Intelligent systems able to perform everyday tasks in human living environments are going to play an important role in the future. Especially service and assistive robots, which could take over tasks such as fetch and carry, would be of great use. However, dealing with objects in natural environments is not a trivial but rather very challenging task. The robot has to extract the objects from noisy sensor data and give them a meaningful and correct description. The goal of this thesis is to develop an approach for robust semantic object recognition, which can be used for such purposes. In our approach, we take advantage of the spatial contextual information about objects’ co-occurrences to perform a robust object recognition. Our approach is unique in that it uses spatial semantics in a probabilistic manner. We also develop a new representation of this information, termed Spatial Potential Fields.

Malgorzata Goldhoorn, Frank Kirchner

Constraint-based Handling of Component Networks

Abstract

The ability to reconfigure running complex component networks in a robust manner is the next challenge in robotic software frameworks. The increasing complexity of hard- and software leads to an increasing systems’ complexity. The need to have a non-static version of a collection of components that form a behaviour, for one point in time, is caused not least by limiting resources of processing power. It is not possible to have all algorithms running at each point in time. Therefore, the requirement to manage these component networks came up. This work presents a new constraint-based approach to tackle the problem. The aim of this work is to model a constraint-based system that is able to handle state of the art robotic component networks, without increasing the complexity for the system handling and system instantiation.

Matthias Goldhoorn, Frank Kirchner

Model-Based Testing Against Complex SysML Models

Abstract

In recent years higher level of abstractions are considered to cope with the complexity in today’s system design. Especially, modeling languages such as SysML get increasingly popular in early design phases. Model-based testing allows to use those models for test generation. Test cases are derived from the model and not directly from the specification. In this work a new proposed methodology will be implemented in an existing model-based testing tool. Afterwards this methodology is used to extend the tool to support activities as well as state machines and not only state machines.

Christoph Hilken, Jan Peleska

Integrated Model-based Testing and Model Checking with the Benefits of Equivalence Partition Testing

Abstract

In safety-critical systems the verification process is one of the most important and most time-consuming tasks. Therefore automated methods are needed to guide the verification process. Typical methods for system verification are model checking and model-based testing. Both methodologies have a lot in common. It seems promising to investigate possible synergies of these two research areas. In this work, the possibilities for the integration of model-based testing with model checking will be investigated. Additionally, a novel model-based testing approach based on equivalence class partitioning has been implemented recently. In this paper a short overview of the implementation is given.

Felix Hübner, Jan Peleska

An SMT-based Approach to analyze Non-Linear Relations of Parameters for Hybrid Systems

Abstract

Deriving constraints over parameters to avoid unexpected system behaviors is extremely important for parametric analysis of hybrid systems. In the long run, our project aims for an SMT-based approach to reveal non-linear relations between parameters for hybrid systems that are specified by parameterized formal models using standard data types (reals, integers and booleans) and affine dynamics. The problem we address is undecidable since the underlying logic consists of boolean combinations of propositional logic atoms as well as atoms from non-linear arithmetic theories over integers and reals with quantifiers. Currently, a symbolic simulation algorithm has been prototypically implemented based on a new developed prototypical constraint solver.

Xian Li, Klaus Schneider

Analyzing and Simulating Time Descriptions from UML/MARTE CCSL

Abstract

The complexity of modern embedded systems makes it inevitable to consider higher abstraction levels in the design process to overcome problems in acceptable time and effort. In higher abstraction levels, the utilization of functional requirements is quite advanced, while the utilization of non-functional requirements like timing still is an open problem. We aim to address this problem utilizing the timing definitions from UML/MARTE CCSL.

Judith Peters, Rolf Drechsler

Design and Synthesis of Reversible Circuits using Hardware Description Languages

Abstract

Reversible computation recently gained a lot of interest due to applications in areas like quantum computation and low power design. Due to its special properties, the established circuit design flow cannot simply be applied to reversible logic. In this work, we consider hardware description languages for the scalable design and synthesis of reversible circuits. Two complementary directions are discussed, namely (1) exploiting the conventional design flow and mapping the result to a reversible circuit, and (2) developing an entirely new design flow, which considers reversibility right from the beginning.

Eleonora Schönborn, Rolf Drechsler

Dynamic Rebound Control and Human Robot Interaction of a Ball Playing Robot

Abstract

Building a ball playing entertainment robot with the main contribution of a task level optimal control which handles trajectory planning and optimal control in a single controller and takes redundancy and elasticity into account. For faster actuation the feedback gain is used and the controller distributes into two parts. Human-Robot- Interaction(HRI) completes the entertainment aspect.

Dennis Schüthe, Udo Frese

Development of Consistent Formal Models

Abstract

Formal models can be used in the system design process to find design errors as soon as possible and to reduce the time-to-market and the development costs. Several methods for the verification of such models have been proposed in the past. However, developing such a formal model usually requires several iterations in a so-called refinement process. Between each of these steps, the consistency of the models’ behavior has to be ensured as new errors can be introduced. Additionally, coverage metrics are necessary to determine if the model can be implemented yet or requires further consideration. The major contributions of this thesis are (1) a formally sound approach for the verification of model refinements, (2) a technique to retrieve correct and formal relations between the iterations of the refinement, and (3) a coverage metric for formal models.

Julia Seiter, Rolf Drechsler

Formal Verification of Robustness

Abstract

Due to the decreasing size of transistors, the probability of transient errors and the variability of the transistor’s characteristics in electrical circuits are continuously increasing. These issues demand for techniques to check the robustness of circuits and their behavior under transient faults and variability. Furthermore, the implementation of methods that provide robustness are prone to implementation errors. Checks are needed to verify that the nominal behavior of the system did not change due to modifications that are meant to provide robustness. Solutions for both problems are presented in this work.

Niels Thole, Görschwin Fey

Pose and Posture Estimation using Inertial Sensor Data

Abstract

This paper discusses the estimation of the position and orientation, i.e. the pose, of a rigid body and the posture of a human using inertial sensor data only, i.e. without absolute pose information. Since this is impossible in general, specific assumptions as to the rigid body motion and the skeleton’s structure are introduced. What to expect of estimates obtained using such assumptions is also briefly covered.

Felix Wenk, Udo Frese

Reconfigurable Hardware-Based Acceleration for Machine Learning and Signal Processing

Abstract

Certain application areas of signal processing and machine learning, such as robotics, impose technical limitations on the computing hardware, which make the use of generic processors unfeasible. In this paper we propose a framework for the development of dataflow accelerators as a possible solution. The approach is based on model based development and code generation to allow a rapid development of the accelerators and perform a functional verification of the overall system.

Hendrik Woehrle, Frank Kirchner

Backmatter