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 finitehorizon
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 SMTSolver
Timed automata as acceptors of languages of finite timed
words form a very useful framework for the verification of safety properties of realtime systems. Many of the classical automatatheoretic 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 CyberPhysical Systems
Quantitative conformance testing of cyberphysical 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 domainspecific adaptations remedies state
space explosion inherent to formal (statebased) verification. The presented contributions improve the scalability of quantitative conformance
testing of a CPS and is demonstrated with a case study.


Geeraerts, Sznajder, Raskin 
EventClock 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[U_{I},S_{I}] 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[U_{I},S_{I}] over finite
signals without assuming bounded variability. Using the same technique, we also
give synthesis of safety signal automata for MITL[U_{I},S_{I}] 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[U_{I},S_{I}] restricted to Bounded Future formlae where the Until operators
use only bounded (i.e. noninfinite) intervals. It is straightforward to construct
safetysignalautomaton 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 ModelChecking 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 modelchecking 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 modelchecking against ωregular
properties for timed automata can be reduced to standard modelchecking of
timed automata, by computing an adequate bound on the imprecision. This
yields a new algorithm for robust modelchecking 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 nonimplementable, nonrobust, 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 nonZeno
and behave well under discretization; such automata satisfy a sort of
pumping lemma. Formally, the thinthick 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 thinthick 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 realtime 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 OmegaRegular 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 cyberphysical 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 twoplayer games. We show a
polynomialtime reduction from minimum attention controller synthesis to synthesis of controllers for meanpayoff parity objectives in games of incomplete
information. This gives an optimal EXPTIMEcomplete 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 stateoftheart and industrial practice. I will conclude with some
opportunities for improvement.

10:00 
Break 
10:30 
Session 4: Probabilistic models 

Chen, Diciolla, Kwiatkowska, Mereacre 
TimeBounded Verification of CTMCs Against RealTime Specifications
We study timebounded verification of a finite continuoustime Markov chain (CTMC) C against a realtime 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 realtime 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 ScenarioAware Dataflow
Dataflow formalisms are useful for specifying signal processing and
streaming applications. To adequately capture the dynamic aspects of modern applications, the formalism of ScenarioAware Dataflow (SADF) was recently introduced, which allows analysis of worst/bestcase and averagecase performance
across different modes of operation (scenarios). The semantic model of SADF integrates nondeterministic 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 modelchecking
approach for computing quantitative properties of SADF models such as throughput, timeweighted average buffer occupancy and maximum response time. A
compositional statespace reduction technique is introduced as well as an efficient
implementation of this method that combines model construction with onthefly
statespace 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 multimedia domain.


Bentea, Olveczky 
Probabilistic RealTime 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 realtime systems such as wireless sensor networks.
Furthermore, it is often natural to model such systems in an objectoriented style, using subclass inheritance and dynamic object and message creation and deletion. To support the above features, we introduce
probabilistic realtime rewrite theories (PRTRTs), that extend both realtime rewrite theories and probabilistic rewrite theories, as a rewritinglogicbased formalism for probabilistic realtime systems. We then show
that PRTRTs can be seen as a unifying model in which a range of other
models for probabilistic realtime systemsincluding probabilistic timed
automata, stochastic automata, deterministic and stochastic Petri nets,
as well as two probabilistic timed transition system models with underspecified probability distributionscan 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 realtime properties of timed automata
expressible in TCTL to be refined by performance properties, e.g. in
terms of probabilistic guarantees of time and costbounded properties.
A second contribution is the application of Statistical Model
Checking (SMC) to efficiently estimate the correctness of nonnested
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 Nonlinear 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
nonlinear 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
nonlinear 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
timetriggered 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 omegaregular
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 languagetheoretic 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 nonlinear 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 
ModelBased Dependability Analysis of Programmable, RealTime 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 modelchecking to automate the dependability
analysis of programmable, realtime medical devices. Our approach uses timed
and hybrid automata to model the realtime 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 casestudy 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 DesignforVerification Framework for a Configurable PerformanceCritical Communication Interface
We present a DesignforVerification framework
for a Configurable PerformanceCritical Communication Interface. To
manage the inherent complexity of the problem we decomposed the interface into independent parametrisable communication blocks. TockCSP
was then used to model the timing and functional specifications of our
interface. The FDR model checker and its taupriority model were used
to prove that the properties of the configured interface are within the
properties of targeted communication protocols.

15:00 
Closing 