Most talks are scheduled to be between 90 and 105 minutes in order to have coffee breaks for discussions of at least 30 minutes length between the talks. The times given here reflect the upper-bound length of the talks and the lower-bound length of the coffee breaks.
|Mon, 2010-03-15||Tue, 2010-03-16||Wed, 2010-03-17||Thu, 2010-03-18||Fri, 2010-03-19|
|09:00-09:15||Front desk opens||Kim G. Larsen||Bernd Finkbeiner||Joel Ouaknine||Jean-François Raskin|
|09:45-10:00||Edmund M. Clarke / Paolo Zuliani|
|10:45-11:00||Coffee break||Coffee break||Coffee break||Coffee break|
|11:15-11:30||Klaus Dräger||Thomas Wies||Sebastian Kupferschmid||Bruce H. Krogh|
|14:00-14:15||Viorica Sofronie-Stokkermans||Patricia Bouyer-Decitre||Reinhard Wilhelm / Björn Wachter||Stefan Ratschan||Martin Fränzle|
|15:45-16:00||Coffee break||Coffee break||Coffee break||Coffee break||Closing|
|16:15-16:30||Bernd Westphal||Christoph Scholl||Jens Oehlerking||Holger Hermanns|
In this lecture we present a Model Checking approach for verifying complex stochastic embedded and biological systems. We start by reviewing the basics of Model Checking, including temporal logics such as LTL and CTL. Next, we introduce the verification problem for stochastic systems, and we present a Statistical Model Checking approach based on Bayesian statistics. Finally, we illustrate two representative applications of the techniques presented. The first addresses the verification of hybrid systems encoded as Stateflow/Simulink models. The second involves biological signaling pathways important for pancreatic cancer.
11:30-12:00 Coffee break
The talk will present recent results on supporting component based design of hybrid systems. A key ingredient is the definition of external component interface specifications which are rich enough to support compositional verification of safety and stability properties of such controllers.
We provide a language for hierarchical construction of hybrid controllers from such components, where each layer allows to build subsystems by what we call transition composition of nodes. We show how the verification of interface specifications can be completely automated, and provide a hiearchical and compositional approach to the verification of hybrid systems.
In this lecture I will present some recent advances in the field of efficient automated reasoning in rich data structures.
Such complex data structures occur very often in the verification of reactive and real time systems. In program verification, for instance, one needs to be able to reason about lists, arrays, or sets with elements of a certain type, or about several such data types at the same time. Similar combinations of data structures are also used when modeling other types of reactive or real-time systems such as, for instance, transportation systems with several components.
The framework I present is based on a general notion of locality — with a focus on possibilities of hierarchical and modular reasoning in local theory extensions and combinations thereof. I show that locality considerations allow us to obtain parameterized decidability and complexity results for many (combinations of) theories important in verification in general and in the verification of parametric systems in particular.
I present various applications of these results in the deductive verification of reactive and real time systems.
15:45-16:15 Coffee break
Our talk will consist of three parts. We begin with a general introduction into AVACS project area S, "Systems of Systems", which consists of three subprojects concerned with partial designs and requirements synthesis, with dynamically changing communication topologies, and with quantitative aspects such as reliability.
The main part of the talk is an introduction the problem domain of systems with dynamically changing communication topologies (DCS). A prominent example of a DCS is automatic support for dynamic car platooning on highways. Each car is an autonomous agent which can drive on its one, but also participate in a platoon either as leader or as follower. Cars join or leave a platoon according to a negotiation protocol over a wireless network, so the communication topology, i.e. the acquaintance relation between agents is changing over time. The number of agents to consider is unbounded because cars can freely enter and leave the highway.
We present how to establish properties of DCS such as "no two cars consider each other to be the leader" or "when merging two platoons, followers of the back platoon are finally handed over to the front platoon" employing a rather coarse abstraction following the so-called spotlight principle. In order to refine the abstraction, we integrate information about possible topologies gathered by a static analysis using partner abstraction or follow a counter-example guided approach.
We close the talk with a description of the problems that arise when we move to more realistic descriptions which no longer abstract from hybrid and probabilistic aspects.
Within the European Joint Technology Initiative ARTEMIS as well as several national initiatives such as CISS and DaNES, model-driven development is a key to dealing with the increasing complexity of embedded systems, while reducing the time and cost to market. The use of models should permit early assessment of the functional correctness of a given design as well as requirements for resources (e.g. energy, memory, and bandwidth) and real-time and performance guarantees. Thus, there is a need for quantitative models allowing for timed, stochastic and hybrid phenomenas to be modeled an analysed.
UPPAAL and the branches CORA and TIGA provide an integrated tool environment for modelling, validation, verification and synthesis of real-time systems modelled as networks timed automata, extended with data types and user-defined functions. The lectures will provide details on the expressive power of timed automata in relationship to embedded systems as well as details on the power and working of the UPPAAL verification engine.
In this talk we demonstrate how UPPAAL has been applied to the validation, performance analysis and synthesis of a number of real-time communication protocols and embedded control problems. The applications include Leader-Election in Mobile Networs, so-called Task Graph Scheduling and MPSoC systems consisting of application software running under different RTOS on processors interconnected through an on-chip network. Also we show how CORA and TIGA has been used to synthesize optimal (e.g. wrt. energy or memory) scheduling strategies for given applications, including climate control and robust control for hydralic pumps.
10:45-11:15 Coffee break
I will give an introduction to abstraction refinement, starting with the general concepts and then presenting the SLAB approach developed in AVACS subproject R1. This version of abstraction refinement is tailored towards complex systems with many components for which it is desirable to keep the size of the abstraction as small as possible; because of this, it uses a very local refinement strategy on a persistent, aggressively pruned graph-based abstraction. I will also discuss the tradeoff associated with the design decisions we made.
In this lecture I will briefly present the basis of real-time model-checking, before focusing on timed games, a natural extension of timed automata which can model uncertainty on delays and interaction with an environment. I will explain how those games are played and can be solved. Then I will show possible extensions of timed games with probabilities which allow to model stochastic aspects of systems, and give few recent results on that extremely expressive and complex model.
15:45-16:15 Coffee break
In this lecture I will present methods for verifiying safety requirements of hybrid systems which are characterized by a close interaction of discrete components with a physical plant. The analyzed models are given by guarded assigments to discrete and continuous variables (for the discrete components) and by a set of (simple) differential equations (for the continuous part).
In contrast to standard approaches to the verification of hybrid systems we do not translate the model description into flat linear hybrid automata (LHAs). Since such a translation may lead to an enormous blow-up in size especially for non-trivial discrete components, we perform verification based on fully symbolic representations.
In this context we present several optimization techniques which are not only relevant to hybrid system verification, but can also be employed in other applications which rely on quantifier elimination for formulas with linear arithmetic.
I will discuss the analysis of partial designs, which consist of "white-box" components, for which the implementation is known and fixed, and "black-box" components, for which an implementation is yet to be found. Classic verification (all components are "white-box") is a special case, so is classic synthesis (all components are "black-box"), and there are interesting applications in between, such as compositional verification and error localization. In this talk, I will give an overview on algorithms for the analysis of partial designs, based on infinite games, tree automata, and constraint systems.
10:45-11:15 Coffee break
Message passing concurrency is a common idiom for composing complex systems from simpler subsystems. In distributed and cyber-physical systems where subsystems communicate by message passing, the communication is often dynamic. Subsystems may appear and disappear during evolution of the system and the communication topology may change. By "communication topology" we refer to the graph whose nodes are the individual subsystems and whose edges are communication links. In this talk we are concerned with the verification of systems with dynamic communication. Correctness properties of message passing systems typically depend on the correct execution of the underlying message passing protocols. In systems with dynamic communication, the correctness of these protocols in turn depends on shape invariants of the communication topologies. I will present various techniques for the verification of such invariants.
Run-time guarantees play an important role in the area of embedded systems and especially hard real-time systems. These systems are typically subject to stringent timing constraints which often result from the interaction with the surrounding physical environment. Therefore, a schedulability analysis has to be performed which guarantees that all timing constraints will be met. All existing techniques for schedulability analysis require the worst case execution time (WCET) of each task in the system to be known before the task is executed. The search space to be explored is so large that exhaustive measurement to compute the WCETs are infeasible. So, sound estimations of the WCET have are calculated instead. These estimations should be tight, i.e., the overestimation should be as small as possible.
In modern microprocessor architectures caches and pipelines are key features for improving performance. Unfortunately, they make the analysis of the execution behaviour of instructions very difficult since this behaviour now depends on the execution history.
In the approach, developed at Saarland University and the spinoff company AbsInt, we split the analysis into a set of subtasks: value analysis, cache analysis, pipeline analysis, and path analysis. The value analysis calculates the values of registers for each program point in order to enable the cache analysis to predict the data cache behaviour and to provide the path analysis with automatically derived loop and recursion bounds. The cache analysis predicts the instruction and data cache behaviour of each instruction and the pipeline analysis predicts the pipeline behaviour. These three analyses are all done by Abstract Interpretation. The final step of the run-time prediction is the program path analysis which yields an estimation of the machine cycles needed to execute the program. This is based on Integer Linear Programming (ILP).
The abstract domains for the cache and pipeline analysis are presented. Cache states have compact abstract representations with efficient update functions. For pipelines, no such compact representation has been found so far. This forces the analysis to collect and manage sets of concrete pipeline states. A new approach represents these sets symbolically. A problem of current research is the cooperation between abstract interpretation for caches and model checking for pipelines.
15:45-16:15 Coffee break
In the field of hybrid systems verification, two main classes of properties are of interest: safety and liveness. For feedback control systems, one liveness property is of critical importance: the ability of a controller to always steer a plant toward a desirable part of the state space. This property is termed "stability". While safety verification has seen considerable progress in recent years, stability proofs have proven to be intrinsically more difficult. This talk will focus on techniques for automatically conducting stability proofs, based on methods from control theory. The core concept is the so-called Lyapunov function, an abstract energy function of the system whose existence ensures a continuous progress towards a desirable state. Both the theory of Lyapunov functions and their practical computation in the scope of verification tools will be discussed in detail in this talk.
I will survey the classical, real-time, and time-bounded theories of verification, highlighting key differences and similarities among them, and giving an overview presentation of the solutions to some longstanding open problems regarding Metric Temporal Logic and timed automata.
10:45-11:15 Coffee break
Directed model checking is a well-established technique that is tailored to the fast detection of reachable error states. This is achieved by influencing the order in which states are explored during the state space traversal. The order is typically determined by estimating a state's distance to a nearest error state.
The aim of this lecture is to provide an introduction to directed model checking. The focus of the lecture is on how abstractions can be used to automatically generate distance estimators. Some of the presented approaches are illustrated using timed automata. However, the techniques are introduced in such a way that it is easy to adopt them to other types of systems.
In order to reason about computer systems interacting with a physical environment (i.e., cyber-physical systems), one also has to be able to reason about numerical constraints. However, there is not only the problem that in recent decades numerical constraints have been more in the focus of mathematicians than of computer scientists. But even within mathematics, corresponding research has been spread among several communities (e.g., computer algebra, numerical analysis, interval computation, global optimization). The talk will give an overview of the various available techniques with special emphasis on issues relevant for reasoning about cyber-physical systems.
15:45-16:15 Coffee break
In this lecture I paint the landscape of behavioural models for probability, time, and cost, with a mild focus on concurrent Markov models and their compositionality. I discuss foundational and pragmatic aspects of compositional modelling and model checking in this context, two crucial aspects of a modern strategy to guarantee correctness of systems of systems.
In this talk, I will recall the definition of well-quasi orders and well-structured transition systems. I will review the main algorithmic tools to decide properties on infinite state well- structured transition systems. I will show applications in Petri nets and their extensions. Those models are useful to model systems that are composed of parametric or an arbitrary large number of identical subsystems.
10:45-11:15 Coffee break
The difficulty of computing and representing approximations of reachable sets for general continuous dynamic systems make it difficult to verify properties of even simple hybrid system models based on reachability. Exact reach set computations for linear hybrid automata (LHA), on the other hand, can be performed using simple operations on polyhedra. Nevertheless, the number of continuous state variables that can be handled for LHA is still limited by the rapid growth in the complexity of polyhedral reach sets in higher dimensions. Following a brief survey of the reachability problem for general hybrid systems, methods developed to verify properties of hybrid systems using LHA will be presented. The talk will conclude with an assessment of current methods for verification based on reachability and a discussion of several directions for further research.
Embedded digital systems have become ubiquitous in everyday life. Many such systems, including many of the safety-critical ones, operate within or comprise tightly coupled networks of both discrete-state and continuous-state components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling and analyzing the tight interaction of their discrete switching behavior and their continuous dynamics, as mutual feedback confines fully separate analysis to limited cases. Tools for building such integrated models and for simulating their approximate dynamics are commercially available. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, regardless of the actual disturbance and the influences of the application context, as entering through the open inputs of the system under investigation. Basic notions of being well-behaved demand that the system under investigation may never reach an undesirable state (safety), that it will converge to a certain set of states (stabilization), or that it can be guaranteed to eventually reach a desirable state (progress).
Within this lecture, we concentrate on automatic analysis of various classes of hybrid systems, with a focus on symbolic methods manipulating both the discrete and the continuous state components symbolically by means of predicative encodings and dedicated constraint solvers based on DPLL style proof search. Advances in DPLL based satisfiability solving were instrumental to the adoption of automated formal verification in industrial practice. Building on these successful algorithms, we will demonstrate how they can be extended by incorporation of numeric constraint solving capabilities, as covered by Stefan Ratschan's lecture, as well as by methods for proof-tree pruning, arriving at efficient algorithms for the analysis of various classes of hybrid systems. We will gradually develop these algorithms in the course of the lecture, covering the range from linear hybrid automata over non-linear discrete-time and continuous-time hybrid systems to probabilistic hybrid systems.