Program (tentative; click on the titles to see abstracts):

Wednesday 21 September
8:00	Registration opens
8:50	Welcome
9:00	Oded Maler	Invited talk: Performance Evaluation of Schedulers in a Probabilistic Setting We show how to evaluate the performance of solutions to finite-horizon scheduling problems where task durations are specified by bounded uniform distributions. Our computational technique, based on computing the volumes of zones, constitutes a contribution to the computational study of scheduling under uncertainty and stochastic systems in general.
10:00	Break
10:30	Session 1: Verification and testing
	Lange, Badban	Exact Incremental Analysis of Timed Automata with an SMT-Solver Timed automata as acceptors of languages of finite timed words form a very useful framework for the verification of safety properties of real-time systems. Many of the classical automata-theoretic decision problems are undecidable for timed automata, for instance the inclusion or the universality problem. Here we consider restrictions of these problems: universality for deterministic timed automata and inclusion of a nondeterministic one by a deterministic one. We then advocate the use of SMT solvers for the exact incremental analysis of timed automata via these problems. We stratify these problems by considering domains of timed words of bounded length only and show that each bounded instance is in (co-)NP. We present some experimental data obtained from a prototypical implementation measuring the practical feasibility of the approach to timed automata via SMT solvers.
	Lampka, Woehrle, Thiele	Segmented State Space Traversal for Conformance Testing of Cyber-Physical Systems Quantitative conformance testing of cyber-physical system (CPS) exploits time series of measurements, such as temperature or energy, for validating the correctness of deployed systems. We present the foundations of segmented state space traversal in the setting of quantitative conformance testing of a CPS. It is demonstrated how this strategy together with domain-specific adaptations remedies state space explosion inherent to formal (state-based) verification. The presented contributions improve the scalability of quantitative conformance testing of a CPS and is demonstrated with a case study.
	Geeraerts, Sznajder, Raskin	Event-Clock Automata: From Theory to Practice Event clock automata (ECA) are a model for timed languages that has been introduced by Alur, Fix and Henzinger as an alternative to timed automata, with better theoretical properties (for instance, ECA are determinizable while timed automata are not). Here we revisit and extend the theory of ECA. We first prove that no finite time abstract language equivalence exists for ECA, thereby disproving a claim in the original work on ECA. This means in particular that regions do not form a time abstract bisimulation. Nevertheless, we show that regions can still be used to build a finite automaton recognizing the untimed language of an ECA. Then, we extend the classical notions of zones and DBMs to let them handle event clocks instead of plain clocks (as in timed automata) by introducing event zones and Event DBMs (EDBMs). We discuss algorithms to handle event zones represented as EDBMs, as well as (semi-) algorithms based on EDBMs to decide language emptiness of ECA.
	Pandya, Krishna, Kini	On Construction of Safety Signal Automata for MITL[U,S] using Temporal Projections Construction of automata for Metric Temporal Logics has been an active but challenging area of research. We consider here the continuous time Metric temporal logic MTL[UI,SI] as well as corresponding signal automata. In previous works by Maler, Nickovic and Pnueli, the signal automaton synthesis has mainly addressed MTL under an assumption of bounded variability. We propose a novel technique of "Temporal Projections" that allows easy synthesis of safety signal automata for continuous time MITL[UI,SI] over finite signals without assuming bounded variability. Using the same technique, we also give synthesis of safety signal automata for MITL[UI,SI] with bounded future operators over infinite signals. For finite signals, the Temporal Projections allow us to syntactically transform an MITL formula ϕ(Q) over a set of propositions Q to a pure past time MITL formula ψ(P,Q) with extended set of propositions (P,Q) which is language equivalent "modulo temporal projection". A similar such transformation over infinite signals is also formulated for MITL[UI,SI] restricted to Bounded Future formlae where the Until operators use only bounded (i.e. non-infinite) intervals. It is straightforward to construct safety-signal-automaton for the transformed formula. We give complexity bounds for the resulting automaton. Our temporal projections are inspired by the use of projections by D'Souza et al for eliminating past in MTL.
12:30	Lunch
14:00	Session 2: Robustness
	Bouyer, Markey, Sankur	Robust Model-Checking of Timed Automata via Pumping in Channel Machines Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satisfied by digital hardware on which the models are implemented. In fact, it was shown that the presence of imprecisions, however small they may~be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system. The problem of robust model-checking was then defined to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct. In this work, we show that robust model-checking against ω-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of ω-regular properties, which is both optimal and valid for general timed automata.
	Basset, Asarin	Thin and Thick Timed Regular Languages In previous literature on timed automata, it was noticed that they are in several aspects too precise, which leads sometimes to strange artifacts, mathematical pathologies or unrealistic models. In particular, some timed automata are non-implementable, non-robust, behave badly under discretization, have many Zeno runs etc. We propose a unifying approach to most of these issues for deterministic timed automata. We classify these automata either as thin or as thick. In thin automata, all the infinite trajectories are, in some weak sense, Zeno; the discretization of long trajectories is difficult, since it requires very small discretization step. In thick automata, most of trajectories are non-Zeno and behave well under discretization; such automata satisfy a sort of pumping lemma. Formally, the thin-thick alternative is based on the notion of entropy of timed regular languages introduced by E. Asarin and A. Degorre in [3, 4]. Thin languages have the entropy = -∞ while thick have a larger one. An important application of thin-thick alternative is again the entropy theory of timed languages. We show that the entropy can be computed with a desired precision using discretization and thus it is computable, which closes a question left open in [3, 4].
	Traonouez, Legay, Wasowski, Larsen	Robust Specification of Real Time Components Specification theories for real-time systems allow to reason about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout the entire design process from an abstract specification to an implementation, we need to be able to reason about possibility to effectively implement the theoretical specifications on physical systems. In the literature, this implementation problem has already been linked to the robustness problem for Timed Automata, where small perturbations in the timings of the models are introduced. We address the problem of robust implementations in timed specification theories. Our contributions include the analysis of robust timed games and the study of robustness with respect to the operators of the theory.
15:30	Break
16:00	Session 3: Games
	Chatterjee, Majumdar	Minimum Attention Controller Synthesis for Omega-Regular Objectives A controller for a discrete game with -regular objectives requires attention if, intuitively, it requires measuring the state and switching from the current control action. Minimum attention controllers are preferable in modern shared implementations of cyber-physical systems because they produce the least burden on system resources such as processor time or communication bandwidth. We give algorithms to compute minimum attention controllers for ω-regular objectives in imperfect information discrete two-player games. We show a polynomial-time reduction from minimum attention controller synthesis to synthesis of controllers for mean-payoff parity objectives in games of incomplete information. This gives an optimal EXPTIME-complete synthesis algorithm. We show that the minimum attention controller problem is decidable for infinite state systems with finite bisimulation quotients. In particular, the problem is decidable for timed and rectangular automata.
	Quesel, Fränzle, Damm	Crossing the Bridge Between Similar Games Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. We identify a family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.
Thursday 22 September
9:00	Boudewijn Haverkort	Invited talk: Formal Modeling and Analysis of Timed Systems: Technology Push or Market Pull? I will address the question whether the methods and techniques we develop are applied well in industrial practice. To address this question, I will make a few observations from the academic field, as well as from industrial practice. This will be followed by a concise analysis of the cause of the perceived gap between the academic state-of-the-art and industrial practice. I will conclude with some opportunities for improvement.
10:00	Break
10:30	Session 4: Probabilistic models
	Chen, Diciolla, Kwiatkowska, Mereacre	Time-Bounded Verification of CTMCs Against Real-Time Specifications We study time-bounded verification of a finite continuous-time Markov chain (CTMC) C against a real-time specification, provided either as a metric temporal logic (MTL) property ϕ, or as a timed automaton (TA) A. The key question is: what is the probability of the set of timed paths of C that satisfy ϕ (or are accepted by A) over a time interval of fixed, bounded length? We provide approximation algorithms to solve these problems. We first derive a bound N such that timed paths of C with at most N discrete jumps are sufficient to approximate the desired probability up to ε. Then, for each discrete (untimed) path σ of length at most N, we generate timed constraints over variables determining the residence time of each state along σ, depending on the real-time specification under consideration. The probability of the set of timed paths, determined by the discrete path and the associated timed constraints, can thus be formulated as a multidimensional integral. Summing up all such probabilities yields the result. For MTL, we consider both the continuous and the pointwise semantics. The approximation algorithms differ mainly in constraints generation for the two types of specifications.
	Theelen, Geilen, Voeten	Performance Model Checking Scenario-Aware Dataflow Dataflow formalisms are useful for specifying signal processing and streaming applications. To adequately capture the dynamic aspects of modern applications, the formalism of Scenario-Aware Dataflow (SADF) was recently introduced, which allows analysis of worst/best-case and average-case performance across different modes of operation (scenarios). The semantic model of SADF integrates non-deterministic and discrete probabilistic behaviour with generic discrete time distributions. This combination is different from the semantic models underlying contemporary quantitative model checking approaches, which often assume exponentially distributed or continuous time or they lack support for expressing discrete probabilistic behaviour. We discuss a model-checking approach for computing quantitative properties of SADF models such as throughput, time-weighted average buffer occupancy and maximum response time. A compositional state-space reduction technique is introduced as well as an efficient implementation of this method that combines model construction with on-the-fly state-space reductions. Strong reductions are possible because of special semantic properties of SADF, which are common to dataflow models. We illustrate this efficiency with several case studies from the multi-media domain.
	Bentea, Olveczky	Probabilistic Real-Time Rewrite Theories and their Expressive Power Unbounded data structures, advanced data types, and/or different forms of communication are often needed to model large and complex probabilistic real-time systems such as wireless sensor networks. Furthermore, it is often natural to model such systems in an object-oriented style, using subclass inheritance and dynamic object and message creation and deletion. To support the above features, we introduce probabilistic real-time rewrite theories (PRTRTs), that extend both real-time rewrite theories and probabilistic rewrite theories, as a rewriting-logic-based formalism for probabilistic real-time systems. We then show that PRTRTs can be seen as a unifying model in which a range of other models for probabilistic real-time systems--including probabilistic timed automata, stochastic automata, deterministic and stochastic Petri nets, as well as two probabilistic timed transition system models with underspecified probability distributions--can naturally be represented.
	David, Larsen, Legay, Mikučionis, Poulsen, van Vliet, Wang	Statistical Model Checking for Networks of Priced Timed Automata We offer a natural stochastic semantics of Networks of Priced Timed Automata (NPTA) based on races between components. The semantics provides the basis for satisfaction of Probabilistic Weighted CTL properties (PWCTL), conservatively extending the classical satisfaction of timed automata with respect to TCTL. In particular the extension allows for hard real-time properties of timed automata expressible in TCTL to be refined by performance properties, e.g. in terms of probabilistic guarantees of time- and cost-bounded properties. A second contribution is the application of Statistical Model Checking (SMC) to efficiently estimate the correctness of non-nested PWCTL model checking problems with a desired level of confidence, based on a number of independent runs of the NPTA. In addition to applying classical SMC algorithms, we also offer an extension that allows to efficiently compare performance properties of NPTAs in a parametric setting. The third contribution is an efficient tool implementation of our result and applications to several case studies.
12:30	Lunch
14:00	Session 5: Verification
	Kupferschmid, Becker	Craig Interpolation in the Presence of Non-linear Constraints An increasing number of applications in particular in the verication area leverages Craig interpolation. Craig interpolants (CIs) can be computed for many dierent theories such as: propositional logic, linear inequalities over the reals, and the combination of the preceding theories with uninterpreted function symbols. To the best of our knowledge all previous tools that provide CIs are addressing decidable theories. With this contribution we make Craig interpolation available for an in general undecidable theory that contains Boolean combinations of linear and non-linear constraints including transcendental functions like sin(·) and cos(·). Such formulae arise e.g. during the verication of hybrid systems. We show how the construction rules for CIs can be extended to handle non-linear constraints. To do so, an existing SMT solver based on a close integration of SAT and Interval Constraint Propagation is enhanced to construct CIs on the basis of proof trees. We provide rst experimental results demonstrating the usefulness of our approach: With the help of Craig interpolation we succeed in proving safety in cases where the basic solver could not provide a complete answer. Furthermore, we point out the (heuristic) decisions we made to obtain suitable CIs and discuss further possibilities to increase the exibility of the CI construction.
	Abdulla, Delzanno, Sangnier, Rezine, Traverso	On the Verification of Timed Ad Hoc Networks We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is represented by a graph and the behavior of each node is represented by a timed automaton communicating with its neighbors via broadcast messages. We consider verification problems formulated in terms of reachability, starting from initial configurations of arbitrary size, of a configuration that contain at least one occurrence of a node in a certain state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.
15:00	Coffee
18:00	Excursion and Banquet
Friday 23 September
9:00	Rajeev Alur	Invited talk: Interfaces for Control Components Modern software engineering heavily relies on clearly specified interfaces for separation of concerns among designers implementing components and programmers using those components. The need for interfaces is evident for assembling complex systems from components, but more so in control applications where the components are designed by control engineers using mathematical modeling tools and used by software executing on digital computers. However, the notion of an interface for a control component must incorporate some information about timing, and standard programming languages do not provide a way of capturing such resource requirements. This talk will describe how finite automata over infinite words can be used to define interfaces for control components. When the resource is allocated in a time-triggered manner, the allocation from the perspective of an individual component can be described by an infinite word over a suitably chosen alphabet. The control engineer can express the interface of the component as an omega-regular language that contains all schedules that meet performance requirements. The software must ensure, then, that the runtime allocation is in this language. The main benefit of this approach is composability: conjoining specifications of two components corresponds to a simple language-theoretic operation on interfaces. We have demonstrated how to automatically compute automata for performance requirements such as exponential stability and settling time for the LQG control designs. The framework is supported by a toolkit, RTComposer, that is implemented on top of Real Time Java. The benefits of the approach will be demonstrated using applications to wireless sensor/actuator networks based on the WirelessHART protocol and to distributed control systems based on the Control Area Network (CAN) bus.
10:00	Break
10:30	Session 6: Hybrid systems
	Dzetkulič, Ratschan	Incremental Computation of Succinct Abstractions For Hybrid Systems We introduce a new approach to computing abstractions for hybrid dynamical systems whose continuous behavior is governed by non-linear ordinary differential equations. The abstractions try to capture the reachability information relevant for a given safety property as succinctly as possible. This is achieved by an incremental refinement of the abstractions, simultaneously trying to avoid increases in their size as much as possible. The approach is independent of a concrete technique for computing reachability information, and can hence be combined with whatever technique suitable for the problem class at hand. We illustrate the usefulness of the technique with computational experiments.
	Mitrohin, Podelski	Composing Stability Proofs for Hybrid Systems A recent automatic proof method for the region stability of a hybrid system is based on the reachability analysis for a transformed hybrid system with double dimensionality (the transformation duplicates each of the continuous variables). We propose a new method which composes the reachability analyses for a sequence of transformed hybrid systems with essentially the same dimensionality (each transformation in the sequence duplicates one of the continuous variables). The new method thus trades the double dimensionality for the number of reachability analyses.
	Schneider, Nestmann	Rigorous Discretization of Hybrid Systems Using Process Calculi In the context of a hybrid process calculus, we present a formal discretization procedure that abstracts a class of hybrid systems to simply timed systems while preserving observational congruence. The resulting term is not completely discrete because the temporal synchronization between concurrent hybrid processes needs to be maintained. Here we (i) define the hybrid process calculus HCCS as a suitable minimalistic extension of CCS, (ii) study its metatheory including an important connection between behavioural congruence and zenoness, (iii) state and prove properties that are required for a rigorous analysis of discretization, and (iv) apply our methodology to prove a hybrid tank system correct.
12:30	Lunch
14:00	Session 7: Applications
	Sankaranarayanan, Homaie, Lewis	Model-Based Dependability Analysis of Programmable, Real-Time Medical Devices Infusion pumps are commonly used in home/hospital care to inject drugs into a patient at programmable rates over time. However, in practice, a combination of faults including software errors, mechanical failures and human error can lead to catastrophic situations, causing death or serious harm to the patient. Dependability analysis techniques such as failure mode effect analysis (FMEA) can be used to predict the worst case outcomes of such faults and facilitate the development of remedies against them. We present the use of model-checking to automate the dependability analysis of programmable, real-time medical devices. Our approach uses timed and hybrid automata to model the real-time operation of the medical device and its interactions with the care giver and the patient. Common failure modes arising from device failures and human error are modeled in our framework. Specifically, we use "mistake models" derived from human factor studies to model the effects of mistakes committed by the operator. We present a case-study involving an infusion pump used to manage pain through the infusion of analgesic drugs. The dynamics of analgesic drugs are modeled by empirically validated pharmacokinetic models. Using model checking, our technique can systematically explore numerous combinations of failures and characterize the worse case effects of these failures.
	Kharmeh, Eder, May	A Design-for-Verification Framework for a Configurable Performance-Critical Communication Interface We present a Design-for-Verification framework for a Configurable Performance-Critical Communication Interface. To manage the inherent complexity of the problem we decomposed the interface into independent parametrisable communication blocks. Tock-CSP was then used to model the timing and functional specifications of our interface. The FDR model checker and its tau-priority model were used to prove that the properties of the configured interface are within the properties of targeted communication protocols.
15:00	Closing