Search

Hybrid system dynamics arises when discrete actions meet continuous behaviour due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities. Various flavours of hybrid automata have been suggested as a means to formally analyse dynamics of such systems. In this article, we present our current work on a revised formal model that is able to represent state tracking and estimation in hybrid systems and thereby enhancing precision of verification verdicts.

Functional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.

In this paper, we propose an approach how connected and highly automated vehicles can perform cooperative maneuvers such as lane changes and left-turns at urban intersections where they have to deal with human-operated vehicles and vulnerable road users such as cyclists and pedestrians in so-called mixed traffic. In order to support cooperative maneuvers the urban intersection is equipped with an intelligent controller which has access to different sensors along the intersection to detect and predict the behavior of the traffic participants involved. Since the intersection controller cannot directly control all road users and - not least due to the legal situation - driving decisions must always be made by the vehicle controller itself, we focus on a decentralized control paradigm. In this context, connected and highly automated vehicles use some carefully selected game theory concepts to make the best possible and clear decisions about cooperative maneuvers. The aim is to improve traffic efficiency while maintaining road safety at the same time. Our first results obtained with a prototypical implementation of the approach in a traffic simulation are promising.

Delays in feedback dynamics of coupled dynamical systems arise regularly, especially in embedded control where the physical plant and the controller continuously interact through digital networks. Systems featuring delays are however notoriously difficult to analyze. Consequently, formal analysis often addresses simplified, delay-free substitute models, risking negligence of the adverse impact of delay on control performance. In this ongoing work, we demonstrate that for continuous systems such as delay differential equations, a major part of the delay-induced complexity can be reduced effectively when adding natural constraints to the model of the delayed feedback channel, namely that it transports a band-limited signal and implements a non-punctual, distributed delay. The reduction is based on a sampling approach which is applicable when the above conditions on the feedback are satisfied. We further discuss the possibilities of lifting this method to mixed discrete-continuous dynamics of delayed hybrid systems and the open issues thereof.

This special issue presents seven overview articles on research conducted in the Research Training Group “System Correctness under Adverse Conditions” (SCARE) at the University of Oldenburg.

Ensuring safe behavior for automated vehicles in unregulated traffic areas poses a complex challenge for the industry. It is an open problem to provide scalable and certifiable solutions to this challenge. We derive a trajectory planner based on model predictive control which interoperates with a monitoring system for pedestrian safety based on cellular automata. The combined planner-monitor system is demonstrated on the example of a narrow indoor parking environment. The system features deterministic behavior, mitigating the immanent risk of black boxes and offering full certifiability. By using fundamental and conservative prediction models of pedestrians the monitor is able to determine a safe drivable area in the partially occluded and unstructured parking environment. The information is fed to the trajectory planner which ensures the vehicle remains in the safe drivable area at any time through constrained optimization. We show how the approach enables solving plenty of situations in tight parking garage scenarios. Even though conservative prediction models are applied, evaluations indicate a performant system for the tested low-speed navigation.

Autonomous vehicles may become an important part of traffic in the next few decades. One of the key factors that contribute to the acceptance of the technology is that the user can understand and to a certain degree predict the behaviour of the automation. One way to communicate the automation's intention and behaviour are graphical human-machine interfaces (HMIs). An online survey was conducted to evaluate five designs for HMIs for turning manoeuvres in automated vehicles. During the survey the participants rated the HMIs based on videos. The overall ratings don't show a clear favourite, however, a separation of the participants regarding their trust in automation and technical affinity indicate preferences regarding the preferred level of abstraction. Furthermore, 97% of the participants agreed that HMIs like the ones presented would help them gain or increase their trust in automated vehicles.

We study conflict situations that dynamically arise in traffic scenarios, where different agents try to achieve their set of goals and have to decide on what to do based on their local perception. We distinguish several types of conflicts for this setting. In order to enable modelling of conflict situations and the reasons for conflicts, we present a logical framework that adopts concepts from epistemic and modal logic, justification and temporal logic. Using this framework, we illustrate how conflicts can be identified and how we derive a chain of justifications leading to this conflict. We discuss how conflict resolution can be done when a vehicle has local, incomplete information, vehicle to vehicle communication (V2V) and partially ordered goals., In Proceedings CREST 2019, arXiv:1910.13641. arXiv admin note: substantial text overlap with arXiv:1905.11764

Hybrid automata are an elegant formal model seamlessly integrating differential equations representing continuous dynamics with automata capturing switching behavior. Since the introduction of the computational model more than a quarter of a century ago [Maler et al. 1992], its algorithmic verification has been an area of intense research. Within this note, which is dedicated to Oded Maler (1957--2018) as one of the inventors of the model, we are trying to delineate major lines of attack to the reachability problem for hybrid automata. Due to its relation to system safety, the reachability problem is a prototypical verification problem for hybrid discrete-continuous system dynamics.

Stochastic discrete-time systems, i.e., discrete-time dynamic systems subject to stochastic disturbances, are an essential modelling tool for many engineering systems, and reach-avoid analysis is able to guarantee safety (i.e., via avoiding unsafe sets) and progress (i.e., via reaching target sets). In this paper we study the reach-avoid problem of stochastic discrete-time systems over open (i.e., not bounded a priori) time horizons. The stochastic discrete-time system of interest is modeled by iterative polynomial maps with stochastic disturbances, and the problem addressed is to effectively compute an inner approximation of its p-reach-avoid set. The p-reach-avoid set collects those initial states that give rise to a bundle of trajectories which with probability being larger than p eventually hits a designated set of target states while remaining inside a set of safe states before the first hit. The computation of the p-reach-avoid set is first reduced to the computation of a corresponding strict p-super-level set and is then inner-approximated by solving a semi-definite programming problem obtained from a relaxation of the definition of the super-level set. Two examples demonstrate the proposed approach.

In this paper we propose a computational method based on semi-definite programming for synthesizing infinite-time reach-avoid sets in discrete-time polynomial systems. An infinite-time reach-avoid set is a set of initial states making the system eventually, i.e., within finite time enter the target set while remaining inside another specified (safe) set during each time step preceding the target hit. The reach-avoid set is first characterized equivalently as a strictly positive sub-level of a bounded value function, which in turn is shown to be a solution to a system of derived equations. The derived equations are further relaxed into a system of inequalities, which is encoded into semi-definite constraints based on the sum-of-squares decomposition for multivariate polynomials, such that the problem of synthesizing inner-approximations of the reach-avoid set can be addressed via solving a semi-definite programming problem. Two examples demonstrate the proposed approach.

Software updates are indispensable for the continuous development of Cyber Physical Systems (CPS): They allow for low-cost bug-fixing, fast adaptation to new or changing environments, or adding new functionality throughout the CPS’s life-cycle. Due to the urgent need for some safety-critical updates, their verification and validation may need to happen as fast as possible without loss of quality. For this reason, incremental checks targeting specifically the introduced changes and their impact on the system are essential as they speed up the validation process. In this paper, we introduce a concept for such an incremental verification for different types of updates by using contract-based design and verifying the integration of the introduced changes by checking their compliance with the contractually agreed assumptions and guarantees. We demonstrate our approach by applying two update types to an Adaptive Cruise Control (ACC) system and verifying the impact of the changes within the environment of the changed module(s).

The development of autonomous vehicles has gained a rapid pace. Along with the promising possibilities of such automated systems, the question of how to ensure their safety arises. With increasing levels of automation the need for fail-operational systems, not relying on a back-up driver, poses new challenges in system design. In this paper we propose a lightweight architecture addressing the challenge of a verifiable, fail-safe safety implementation for trajectory planning. It offers a distributed design and the ability to comply with the requirements of ISO26262, while avoiding an overly redundant setup. Furthermore, we show an example with low-level prediction models applied to a real world situation.

Acta informatica xx, xx-xx (2020). doi:10.1007/s00236-020-00374-7, Published by Springer, New York, NY

Highly automated driving will be a novel experience for many users and may cause uncertainty and discomfort for them [1]. An efficient real-time detection of user uncertainty during automated driving may trigger adaptation strategies, which could enhance the driving experience and subsequently the acceptance of highly automated driving [2]. In this study, we compared three different models to classify a user’s uncertainty regarding an automated vehicle’s capabilities and traffic safety during overtaking maneuvers based on experimental data from a driving-simulator study. By combining physiological, contextual and user-specific data, we trained three different deep neural networks to classify user uncertainty during overtaking maneuvers on different sets of input features. We evaluated the models based on metrics like the classification accuracy and F1 Scores. For a purely context-based model, we used features such as the Time-Headway and Time-To-Collision of cars on the opposing lane. We demonstrate how the addition of user heart rate and related physiological features can improve the classification accuracy compared to a purely context-based uncertainty model. The third model included user-specific features to account for inter-user differences regarding uncertainty in highly automated vehicles. We argue that a combination of physiological, contextual and user-specific information is important for an effectual uncertainty detection that accounts for inter-user differences.

We present an integrated method for safety assessment of automated driving systems which covers the aspects of functional safety and safety of the intended functionality (SOTIF), including identification and quantification of hazardous scenarios. The proposed method uses and combines established exploration and analytical tools for hazard analysis and risk assessment in the automotive domain, while adding important enhancements to enable their applicability to the uncharted territory of safety analyses for automated driving. The method is tailored to support existing safety processes mandated by the standards ISO 26262 and ISO/PAS 21448 and complements them where necessary. It has been developed in close cooperation with major German automotive manufacturers and suppliers within the PEGASUS project (https://www.pegasusprojekt.de/en). Practical evaluation has been carried out by applying the method to the PEGASUS Highway-Chauffeur, a conceptual automated driving function considered as a common reference system within the project.

Advances in Vehicular Cyber-Physical Systems (VCPS) are the primary enablers of the shift from no automation to fully autonomous vehicles (AVs). One of the impacts of this shift is to develop safe AVs in which most or all of the functions of the human driver are replaced with an intelligent system. However, while some progress has been made in equipping AVs with advanced AI capabilities, VCPS designers are still faced with the challenge of designing trustworthy AVs that are in sync with the unpredictable behaviours of humans. In order to address this challenge, we present a model that describes how a Human Ambassador component can be integrated into the overall design of a new generation of VCPS. A scenario is presented to demonstrate how the model can work in practice. Formalisation and co-simulation challenges associated with integrating the Human Ambassador component and future work we are undertaking are also discussed.

Emerging smart technologies add elements of intelligence, cooperation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes. Hybrid automata, in their various flavours, have been suggested as a formal model accurately capturing CPS dynamics and thus facilitating exhaustive behavioural analysis of interacting CPSes with mathematical rigour.

This paper presents a combined Nonlinear Model Predictive Control (NMPC) for position and velocity tracking of underactuated surface vessels, and collision avoidance of static and dynamic objects into a single control scheme with sideslip angle compensation and environmental disturbances counteraction. A three-degree-of-freedom (3-DOF) dynamic model is used with only two control variables: namely, surge force and yaw moment. External environmental forces are considered as constant or slowly varying disturbances with respect to the inertial frame, and hence nonlinear for the body frame of the vessel. Nonlinear disturbance observer (NDO) is used to estimate these disturbances in order to be fed into the prediction model and enhance the robustness of the controller. A nonlinear optimization problem is formulated to minimize the deviation of the vessel states from a time varying reference generated over a finite horizon by a virtual vessel. Sideslip angle is considered in the cost function formulation to account for tracking error caused by the transverse external force in the absence of sway control force. Collision avoidance is embedded into the trajectory tracking control problem as a time-varying nonlinear constraint of position states to account for static and dynamic obstacles. MATLAB simulations are used to assess the validity of the proposed technique.

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks within this category, and recommends next steps for this category towards next year’s edition of the competition. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Spring 2019.

International audience; We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.

Delayed coupling between state variables occurs regularly in technical dynamical systems, especially embedded control. As it consequently is omnipresent in safety-critical domains, there is an increasing interest in the safety verification of systems modelled by Delay Differential Equations (DDEs). In this paper, we leverage qualitative guarantees for the existence of an exponentially decreasing estimation on the solutions to DDEs as established in classical stability theory, and present a quantitative method for constructing such delay-dependent estimations, thereby facilitating a reduction of the verification problem over an unbounded temporal horizon to a bounded one. Our technique builds on the linearization technique of nonlinear dynamics and spectral analysis of the linearized counterparts. We show experimentally on a set of representative benchmarks from the literature that our technique indeed extends the scope of bounded verification techniques to unbounded verification tasks. Moreover, our technique is easy to implement and can be combined with any automatic tool dedicated to bounded verification of DDEs.

International audience

We present a method based on the Hamilton-Jacobi framework that is able to compute over- and under-approximations of reachable sets for autonomous dynamical systems beyond polynomial dynamics. The method does not resort to user-supplied candidate polynomials, but rather relies on an expansion of the evolution function whose convergence in compact state space is guaranteed. Over- and under-approximations of the reachable state space up to any designated precision can consequently be obtained based on truncations of that expansion. As the truncations used in computing over- and under-approximations as well as their associated error bounds agree, double-sided enclosures of the true reach-set can be computed in a single sweep. We demonstrate the precision of the enclosures thus obtained by comparison of benchmark results to related simulations.

Hybrid discrete-continuous system dynamics arises when discrete actions, e.g. by a decision algorithm, meet continuous behaviour, e.g. due to physical processes and continuous control. Various flavours of hybrid automata have been suggested as a means to formally analyse such dynamical systems, among them deterministic automata models facilitating reasoning about their normative behaviour, nondeterministic automata under a demonic interpretation supporting worst-case analysis, and stochastic variants enabling quantitative verification. In this article, we demonstrate that all these variants provide imprecise, in the sense of either overly pessimistic or overly optimistic, verdicts for engineered systems operating under uncertain observation of their environment due to, e.g., measurement error. We argue that even the most elaborate models of hybrid automata currently available ignore wisdom from metrology and game theory concerning environmental state estimation to be pursued by a rational player, which a control system obviously ought to constitute. We consequently suggest a revised formal model, called Bayesian hybrid automata, that is able to represent state tracking and estimation in hybrid systems and thereby enhances precision of verdicts obtained from the model.

We address the question of feasibility of tests to verify highly automated driving functions by optimizing the trade-off between virtual tests for verifying safety properties and physical tests for validating the models used for such verification. We follow a quantitative approach based on a probabilistic treatment of the different quantities in question. That is, we quantify the accuracy of a model in terms of its probabilistic prediction ability. Similarly, we quantify the compliance of a system with its requirements in terms of the probability of satisfying these requirements. Depending on the costs of an individual virtual and physical test we are then able to calculate an optimal trade-off between physical and virtual tests, yet guaranteeing a probability of satisfying all requirements.

Vehicular ad-hoc networks (VANETs) offer a diverse set of applications and therefore gain more and more attention from both academic and industrial communities. However, the deployment of VANETs is not very straight-forward. One challenge is highlighted by an uphill task of establishing and subsequently sustaining a robust communication. The need to obviate extra relay infrastructure in dynamically fluctuating topologies plus concurring shielding obstacles only magnifies this arduous task. In this context, information about traffic-density and about its estimated progress are valuable assets to tackle this issue. This paper proposes a novel routing protocol called Traffic Aware Segment-based Routing (TASR) protocol. The proposed protocol comprises two major parts: 1) Real-time vehicular traffic information for route selection allows for calculating the Expected Connectivity Degree (ECD) on different segments, and 2) a new forwarding method based on geographical information transfers packets from source to destination node. The new metric ECD takes vehicle densities into account, estimating the connectivity on each segment and thus the connectivity of nodes and data delivery ratio for transmitting packets. Furthermore, extensive simulations help analyzing the efficiency of TASR, indicating that it outperforms competing routing protocols.

The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing or actuating the environment through physical devices nor data forwarding to and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to \(\omega \)-regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm synthesizing a series of controllers handling increasing delays and reducing game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore shed some light on the practically relevant case of non-order-preserving delays, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay pioneered by Klein and Zimmermann.

For developers of assisted or automated driving systems, gaining specific feedback and quantitative figures on the safety impact of the systems under development is crucial. However, obtaining such data from simulation of their design models is a complex and often time-consuming process. Especially when data of interest hinge on extremely rare events, an estimation of potential risks is highly desirable but a non-trivial task lacking easily applicable methods. In this paper we describe how a quantitative statement for a risk estimation involving extremely rare events can be obtained by guiding simulation based on reinforcement learning. The method draws on variance reduction and importance sampling, yet applies different optimization principles than related methods, like the cross-entropy methods against which we compare. Our rationale for optimizing differently is that in quantitative system verification, a sharper upper bound of the confidence interval is of higher relevance than the total width of the confidence interval.

The timing predictability of Multi-Processor System on Chip (MPSoC) platforms with hard real-time applications is much more challenging than that of traditional platforms due to their large number of shared processing, communication and memory resources. Yet, this is an indispensable challenge for guaranteeing their safe usage in safety critical domains (avionics, automotive).In this article, a real-time analysis based on model-checking is proposed. The model-checking based method allows guaranteeing timing bounds of multiple Synchronous Data Flow Application (SDFA) implementations. This approach utilizes timed automata (TA) as a common semantic model to represent WCET of software components (SDF actors) and shared communication resource access protocols for buses, DMA, private local and shared memories of the MPSoC. The resulting network of TA is analyzed using the UPPAAL model-checker for providing safe timing bounds of the implementation. Furthermore, we will show the extension of our previous system model enabling single-beat inter-processor communication style beside the burst-transfer style and provide the implementation of the complete set of TA templates capturing the considered system model.We demonstrate our approach using a multi-phase electric motor control algorithm (modeled as SDFA) mapped to Infineon's TriCore-based Aurix multicore hardware platform with both the burst and single-beat inter-processor communication styles. Our approach shows a significant precision improvement (up to a percentage improvement of 300%) compared with the worst-case bound calculation based on a pessimistic analytical upper-bound delays for every shared resource access. In addition, scalability is examined to demonstrate analysis feasibility for small parallel systems, up to 40 actors mapped to 4-tiles and up to 96 actors on a 2-tiles platforms.

We suggest a method for significantly reducing the so-called wrapping effect, i.e., the accumulation of approximation errors incurred during reach-set computation of differential equations when repeatedly over-approximating intermediate reach sets by tractable computational representations of sets in the Rn. Our method can be implemented on top of any known reach-set computation method and generalizes bracketing systems [1] by being based on dimension-wise enclosures of the reach sets of appropriate lower-dimensional surfaces of the initial set selected due to monotonicity properties. Thus exploring just low-volume sub-sets rather than the entire initial and intermediate reach sets, accuracy is enhanced as the approximation error tends to be correlated with set volume. At the same time, the curse of dimensionality that set partitioning methods are prone to is avoided by resorting to a number of subsets linear in the problem dimension. Technically, we first conduct sensitivity analysis of the solution mapping with respect to initial states based on a simulation-based technique, and then determine subsets which are extracted from the boundary of the initial set for performing reachability analysis. We test our method by using it on top of the validated ODE solver VNODE-LP and demonstrate its effect by comparison with existing methods, using illustrative examples of non-linear dynamics.

One key goal of Vehicular Ad-hoc Networks (VANETs) is to provide sufficient Quality-of-Service (QoS) for real-time safety applications. These applications facilitate wireless broadcast warning messages between neighboring vehicles to inform drivers on time about dangerous situations like accidents. The IEEE 1609.4 standard in DSRC defines a MAC layer implementation for multichannel operations in VANETs for such broadcasts. In this paper, we present a distributed hybrid MAC scheme for emergency systems. The proposed scheme improves the Control Channel (CCH) utilization and uniformly distributes the load on Service Channels (SCHs). In the proposed scheme, the network switches its mode from general to emergency in order to effectively utilize common service channels thus increase the probability for timely reception of messages. In addition, the proposed scheme reduces the rate of transmission collisions and latency, thus resulting in high probability of message delivery. The propose MAC scheme is simulated and compared with the existing MAC schemes. The obtained results depict that the proposed hybrid scheme outperforms its competitors and thus validates its performance.

Delays in feedback control loop, as induced by networked distributed control schemes, may have detrimental effects on control performance. This induces an interest in safety verification of delay differential equations (DDEs) used as a model of embedded control. This article explores reachable-set computation for a class of DDEs featuring a local homeomorphism property. This topological property facilitates construction of over- and under-approximations of their full reachable sets by performing reachability analysis on the boundaries of their initial sets, thereby permitting an efficient lifting of reach-set computation methods for ODEs to DDEs. Membership in this class of DDEs is determined by conducting sensitivity analysis of the solution mapping with respect to the initial states to impose a bound constraint on the time-lag term. We then generalize boundary-based reachability analysis to such DDEs. Our reachability algorithm is iterative along the time axis and the computations in each iteration are performed in two steps. The first step computes an enclosure of the set of states reachable from the boundary of the step’s initial state set. The second step derives an over- and under-approximations of the full reachable set by including (excluding, resp.) the obtained boundary enclosure from certain convex combinations of points in that boundary enclosure. Experiments on two illustrative examples demonstrate the efficacy of our algorithm.

The ProCoS project has been seminal in widening the perspective on verification of computer-based systems to a coverage of the detailed interaction and feedback dynamics between the embedded system and its environment. We have since then seen a steady increase both in expressiveness of the “hybrid” modeling paradigms adopting such an integrated perspective and in the power of automatic reasoning techniques addressing relevant fragments of logic and arithmetic. In this chapter we review definitions of stochastic hybrid automata and of parametric stochastic hybrid automata, both of which unify the hybrid view on system dynamics with stochastic modeling as pertinent to reliability evaluation, and we elaborate on automatic verification and synthesis methods based on arithmetic constraint solving. The procedures are able to solve step-bounded stochastic reachability problems and multi-objective parameter synthesis problems, respectively.

Behavioral verification of technical systems involving both discrete and continuous components is a common and demanding task. The behavior of such systems can often be characterized using stochastic hybrid automata, leading to verification problems which can be formalized and solved using stochastic logic calculi such as stochastic satisfiability modulo theory (SSMT). While algorithms for discharging proof obligations in SSMT form exist, their applicability is limited due to the computational complexity, which often increases exponentially with the number of quantified variables. Recently, statistical model checking has been successfully applied to stochastic hybrid systems, thereby increasing the size of the system for which verification problems is tractable. However, being based on randomized simulation, these methods usually cannot handle non-determinism. In previous work, we have deviated from the usual approach of simulating the model and rather proposed a statistical method for SSMT solving which, being based on statistical AI planning algorithms, can also treat non-determinism over a finite domain. Here, we extend this previous work to the case of continuous domains. In particular, using ideas from noisy optimization, we adaptively build up a decision tree recording the findings and guiding further exploration, thereby favoring the currently most promising sub-domain. The non-determinism is resolved by translating the satisfaction problem into an optimization problem, thereby computing both optimistic and pessimistic bounds on the probability of satisfaction. At each stage of the evaluation process, we show how to obtain confidence statements about the probability of satisfaction for the overall SSMT formula, including reliable estimates on the optimal resolution of any non-deterministic choice involved.

Fault tolerance measures of distributed systems can be calculated precisely by state space analysis of the Markov chain corresponding to the product of the system components. The power of such an approach is inherently confined by the state space explosion, i.e. the exponential growth of the Markov chain in the size of the underlying system. We propose a decompositional method to alleviate this limitation. Lumping is a well-known reduction technique facilitating computation of the relevant measures on the quotient of the Markov chain under lumping equivalence. In order to avoid computation of lumping equivalences on intractably large Markov chains, we propose a system decomposition supporting local lumping on the considerably smaller Markov chains of the subsystems. Recomposing the lumped Markov chains of the subsystems constructs a lumped transition model of the whole system, thus avoiding the construction of the full product chain. An example demonstrates how the limiting window availability (i.e. a particular fault tolerance measure) can be computed for a self-stabilizing system exploiting lumping and decomposition.

Driven by road safety requirements and intelligent traffic control, Vehicular Ad-hoc Networks (VANETs) have been attracting significant interest in both academia and industry. One key goal of VANETs is to provide sufficient Quality-of-Service (QoS) for real-time safety applications. The MAC protocol for VANETs is crucial to provide for an efficient and reliable medium access. The challenge is to design it to be able to cope with rapid topology changes, high node mobility [1] and different QoS requirements. Safety applications require a high reliability and a bounded delay while non-critical applications are rather throughput sensitive [2]. These applications facilitate wireless broadcast warning messages between neighboring vehicles to inform drivers on time about dangerous situations like accidents. The IEEE 1609.4 standard defines a MAC layer implementation for multichannel operations in VANETs for such broadcasts. In this poster paper, we present a distributed hybrid MAC scheme for emergency systems. The proposed scheme improves the Control Channel (CCH) utilization and uniformly distributes the load on Service Channels (SCHs). In the proposed scheme, the network switches its mode from general to emergency in order to effectively utilize common service channels thus increase the probability for timely reception of messages. In addition, the proposed scheme reduces the rate of transmission collisions and latency, thus resulting in high probability of message delivery. The proposed MAC scheme is simulated and compared with the existing competitors. The obtained results depict that the proposed hybrid scheme outperforms its competitors and thus validates its performance.

As computers increasingly control the systems and services we depend upon within our daily lives like transport, communications, and the media, ensuring these systems function correctly is of utmost importance. This book consists of twelve chapters and one historical account that were presented at a workshop in London in 2015, marking the 25th anniversary of the European ESPRIT Basic Research project ProCoS (Provably Correct Systems). The ProCoS I and II projects pioneered and accelerated the automation of verification techniques, resulting in a wide range of applications within many trades and sectors such as aerospace, electronics, communications, and retail. The following topics are covered: An historical account of the ProCoS projectHybrid Systems Correctness of Concurrent Algorithms Interfaces and Linking Automatic VerificationRun-time Assertions Checking Formal and Semi-Formal Methods Provably Correct Systems provides researchers, designers and engineers with a complete overview of the ProCoS initiative, past and present, and explores current developments and perspectives within the field.

Traffic safety applications exploit vehicle-to-vehicle communication is an emerging and promising area within the intelligent transportation system (ITS) environment. This objective would be achieved essentially by the employ of efficient safety applications which should be able to wirelessly broadcast warning messages between neighboring vehicles in order to inform drivers about a dangerous situation; such as accidents in a timely manner. To ensure their efficiency, safety applications require reliable periodic data dissemination with low latency. IEEE 1609.4 defines a MAC layer implementation for multichannel operations in a vehicular ad hoc network (VANET). In this light we proposes a novel multi channel mode protocol for emergency systems to improve the channel utilization of the control channel (CCH) and uniformly distribute the channel load on service channels (SCHs). In the proposed protocol, network change their modes from general to emergency mode to increase the probability for a message to arrive in time. The scheme reduces the rate of transmission collisions which create latency and improves the reliability of message delivery in time. Furthermore, extensive analysis and simulations are presented.

Delay differential equations (DDEs) play an important role in the modeling of dynamic processes. Delays may arise in contemporary control schemes like networked distributed control and may cause deterioration of control performance, invalidating both stability and safety properties. This induces an interest in DDE especially in the area of modeling embedded control and formal methods for its verification. In this paper, we present an approach aiming at automatic safety verification of a simple class of DDEs against requirements expressed in a linear-time temporal logic. As requirements specification language, we exploit metric interval temporal logic (MITL) with a continuous-time semantics evaluating signals over metric spaces. We employ an interval-based Taylor over-approximation method to enclose the solution of the DDE. As the solution of the DDE gets represented as a timed state sequence in terms of the Taylor coefficients, we can effectively solve temporal-logic verification problems represented as time-bounded MITL formulae. We encode necessary conditions for their satisfaction as SMT formulae over polynomial arithmetic and use the iSAT3 SMT solver in its bounded model checking mode for discharging the resulting proof obligations, thus proving satisfaction of MITL specifications by the trajectories induced by a DDE. In contrast to our preliminary work in [34], we can verify arbitrary time-bounded MITL formulae, including nesting of modalities, rather than just invariance properties.

Energy saving is often achieved via “squeezing” other application-sensitive Quality of Service (QoS) parameters such as delay and throughput. Accordingly, energy-saving methods must consider those QoS parameters. In this paper, we survey the most recent work on energy efficiency in WSNs and we discuss the impacts of these methods on the QoS provided. Moreover, we propose a novel divide-and-conquer procedure to deal with the trade-off between energy consumption and other QoS parameters. The idea is to tackle a certain source of energy consumption to minimize the drawn energy. Subsequently, this energy-saving method is refined to consider other service qualities. To support the correctness of our claim, three energy-saving methods, taking the QoS issues into consideration, are given as examples. The first method exploits a so-called Fuzzy transform for shrinking the wireless traffic with highly precise lossy data compression. In the second method, the sensing module is targeted by employing reliable virtual sensors. Such sensors compensate the unavailability of main energy-hungry sensors during sleep periods. The third method exploits a self-adaptive mechanism to improve the QoS parameters via deliberately reducing the lifetime below the maximum time and exploiting design-time knowledge.

Verification by simulation, based on covering the set of time-bounded trajectories of a dynamical system evolving from the initial state set by means of a finite sample of initial states plus a sensitivity argument, has recently attracted interest due to the availability of powerful simulators for rich classes of dynamical systems. System models addressed by such techniques involve ordinary differential equations (ODEs) and can readily be extended to delay differential equations (DDEs). In doing so, the lack of validated solvers for DDEs, however, enforces the use of numeric approximations such that the resulting verification procedures would have to resort to (rather strong) assumptions on numerical accuracy of the underlying simulators, which lack formal validation or proof. In this paper, we pursue a closer integration of the numeric solving and the sensitivity-related state bloating algorithms underlying verification by simulation, together yielding a safe enclosure algorithm for DDEs suitable for use in automated formal verification. The key ingredient is an on-the-fly computation of piecewise linear, local error bounds by nonlinear optimization, with the error bounds uniformly covering sensitivity information concerning initial states as well as integration error.

Motivated by the practical need for verifying embedded control programs involving linear, polynomial, and transcendental arithmetics, we demonstrate in this paper a CEGAR technique addressing reachability checking over that rich fragment of arithmetics. In contrast to previous approaches, it is neither based on bit-blasting of floating-point implementations nor confined to decidable fragments of real arithmetic, namely linear or polynomial arithmetic. Its CEGAR loop is based on Craig interpolation within the iSAT3 SMT solver, which employs (abstract) conflict-driven clause learning (CDCL) over interval domains together with interval constraint propagation. As usual, the interpolants thus obtained on spurious counterexamples are used to subsequently refine the abstraction, yet in contrast to manipulating and refining the state set of a discrete-state abstraction, we propose a novel technique for refining the abstraction, where we annotate the abstract model’s transitions with side-conditions summarizing their effect. We exploit this for implementing case-based reasoning based on assumption-commitment predicates extracted from the stepwise interpolants in a lazy abstraction mechanism. We implemented our approach within iSAT3 and demonstrate its effectiveness by verifying several benchmarks.

Aiming at fully symbolic methods for the analysis of probabilistic hybrid systems, we recently introduced the notion of stochastic satisfiability modulo theories (SSMT) problems and the corresponding SiSAT solving algorithm. The notion of SSMT extends SMT with randomized (aka. stochastic) as well as existential and universal quantification as known from stochastic propositional satisfiability. In this paper, we describe the symbolic encoding of scheduled-event probabilistic hybrid automata by means of a case study from the networked automation system domain. We furthermore report on the SSMT solver SiSAT including recent enhancements in terms of solver performance, expressiveness of the input language, and handling of numerical issues. The significance of the performance enhancements is demonstrated by empirical results.

The Transregional Collaborative Research Center AVACS integrates the three sites Freiburg, Oldenburg, and Saarbrücken, and addresses the challenge of pushing the borderline for automatic verification and analysis of complex systems. A particular focus of the project is on models of complex transportation systems and their safety requirements. AVACS is organized in ten subprojects, each teaming researchers from all sites, and is funded by the German Science Foundation since January 1, 2004. This article surveys scope, organization, and research directions of AVACS, including pointers to key publications.

In the last decade, cooperative communication and network coding techniques gained rising attention. Based on these techniques, this paper introduces a novel protocol called cooperation and network coding based MAC (CNCMAC) for vehicular ad-hoc networks (VANETs). It employs cooperative automatic repeat request (ARQ) and network coding techniques to enhance throughput. The CNC-MAC protocol works in two phases. In the first phase - cooperation - data is sent to relay nodes. The second phase - network coding - minimizes received packets. The performance of the CNC-MAC protocol is compared with cooperative ARQ-MAC, another common protocol in this domain. The simulation results indicate that CNC-MAC outperforms ARQ-MAC.