Workshop
on Probabilistic and Hybrid System Verification
Pictures!
About the Workshop
Formal verification techniques have been successfully applied
to complex systems such as Microsoft hardware drivers, airborne software at
Airbus and consumer electronic protocols. In this context, the properties a
system has to satisfy are often specified in temporal logics. The formal
verification approach then verifies whether such property holds on a given
system model. As an example, a property could be that the system will never
reach a configuration in which two hosts share the same IP address. Formal
verification of classical transition systems has received considerable
attentions in the past decades: the 2007 Turing award was given to three
researchers for their pioneering research in this area.
Quantitative verification is an important extension of
the basic approach towards verifying systems involving various quantitative
aspects, including randomizations, costs, time, and security metrics. These
characteristics are the key ingredients for modeling and analyzing networked,
embedded, biological and energy systems.
Verification of probabilistic systems with discrete
time and discrete state spaces has first been studied in the nineties by
Hansson & Jonsson. Afterwards, researchers have
investigated the verification of probabilistic systems with continuous time,
with nondeterminism, and various combinations of
them. Today there is a very rich body of literature on theories attacking the
probabilistic verification problem. Based on these theories many software tools
have been developed, which are particularly appealing, as one can use them to
model and analyze real life case studies. These tools are at most loosely
interconnected, which limits their mutual fertilization.
Hybrid system consists of both discrete components and
continuous dynamics: continuous dynamics can represent model the evolution of
variables like velocity, distance or temperature, while discrete components are
often used to model control effects, like the action of turning on or off the
heater. Hybrid systems are very suitable for modeling controllable systems with
continuous variables. On the other side, the interplay of random phenomena and
continuous real-time control deserves increased attention for instance in
wireless sensing and control applications. Thus, probabilistic hybrid systems
arise as the genuine modeling formalism for such applications. Recently,
probabilistic hybrid systems have been applied to the problem of balancing the
energy production and consumption in electric power systems under renewable infeed.
The purpose of this symposium is to identify potential
techniques that are the most promising to further pursued for analyzing
probabilistic hybrid systems, as well as to coin entirely new techniques. The
prospective participants represent the researchers in Germany and China very
well, working on the probabilistic hybrid systems spectrum spanning from
foundations over algorithms to applications. Due to the selection of invitees,
we expect a highly cross-fertilizing atmosphere.
In this workshop, we have altogether 9 institutes from Germany and 12 from China as prospective participants.
The central goal of this workshop is to form the nucleus for a research network
between China and Germany for researchers in the quantitative verification
area. Through the technical program, state-of-the-art knowledge will be
exchanged between all the partners. Further, the workshop will create the forum
for identifying research topics that both sides are interested in so as to make
plans for further collaboration projects.
·
Participants outside of Beijing will stay in the hotel
Holiday Inn, Building
A, No.89 Shuangqing Road, Haidian
District, Beijing 100085, P.R. China. A map can be found
here.
Taking a taxi from the airport
to the hotel will cost about 100RMB.
·
The workshop will be held at ISCAS, Institute of Software Chinese Academy of Sciences. Here is information
about how to get to ISCAS from the hotel.
·
Organizers: Holger Hermanns, Naijun Zhan and Lijun Zhang.
·
Local Organizers: Please feel free to contact
one of the following local organizers for assistence: Ernst Moritz Hahn (+86 132 4019 8152), Naijun Zhan (+86 138 1046 0251), Lijun Zhang (+86 158 0115 0886)
|
24th |
|
|
Session 1 (08:30--10:00): Hybrid Systems I |
|
|
Leucker, Martin |
|
|
He, Fei (贺飞) |
Complete and Learning-based Compositional Verification
for Probabilistic Systems |
|
Liu, Jiang (刘江) |
Nonlinear Estimation and Hybrid Verification |
|
Session 2 (10:30--12:00): Probabilistic Verification II |
|
|
Katoen, Joost-Pieter |
|
|
Buchholz, Peter |
|
|
Wu, Peng (吴鹏) |
Towards Model Checking of Probabilistic Timed
Automata with REDLIB |
|
Session 3 (13:30--15:00): Safety and Abstractions |
|
|
Dong, Wei (董威)
|
Anticipatory Active Monitoring of Safety-Critical
Systems |
|
Chen, Liqian (陈立前) |
Extending octagon abstract domain with absolute
value |
|
Liu, Jing (刘静) |
|
|
Li, Xuandong (李宣东) |
Hybrid
system: modelling and verification |
|
Session 4 (15:30--17:00): Program Verification |
|
|
Kapur, Deepak |
Program verification and invariant generation |
|
Kyas, Marcel |
Verification and Validation of Systems with
Uncertain Measurements for Position Estimation |
|
Chen, Zhengbang (陈振邦) |
Property Guided Dynamic Symbolic Execution |
|
Ying, Mingsheng |
|
|
Feng, Yuan |
|
|
25th |
|
|
Session 1 (08:30--10:00): Hybrid Systems II |
|
|
Abate, Alessandro |
Computable analysis and control synthesis over
complex dynamical systems via formal verification |
|
She, Zhikun (佘志坤) |
Discovering Multiple Lyapunov
Functions for Switched hybrid Systems |
|
Zhan, Naijun （詹乃军） |
|
|
Sesserion 2 (10:30--12:00): Markov Chains |
|
|
Krcál, Jan |
Compositional Verification
and Optimization of Interactive
Markov Chains |
|
Jansen, David N. |
|
|
Wimmer, Ralf |
|
|
afternoon: excursion (Great Wall) |
|
|
26th |
|
|
Session 1 (8:30--10:00): Tools and Applications |
|
|
Hermanns, Holger |
|
|
Wolter, Katinka |
Validating retry mechanisms using queuing systems
with signals |
|
Gu, Bin |
Embedded systems and
cybernation in spacecraft |
|
Wang, Haifeng (王海峰) |
Safety verification of railway train control
system |
|
Session 2 (10:30--12:00): Modelling and Verification |
|
|
Dong, Yunwei (董云卫） |
On Reliability Analysis for Embedded Systems with
AADL Behavior Model |
|
Wang, Zheng (王政） |
Runtime verification for periodic control systems |
|
Lv, Jidong
(吕继东) |
Model Based safety test case Generation method
and its application in train |
|
Sun, Meng (孙猛) |
|
|
afternoon: excursion (Hutong
tour) |
|
|
27th |
|
|
Session 1 (08:30--10:00): Hybrid Systems III |
|
|
Yang, Shaofa (杨绍发) |
Modular discrete time approximations of
distributed hybrid automata |
|
Hahn, Ernst Moritz |
|
|
Abraham, Erika |
|
|
Sesserion 2 (10:30--12:00): Probabilistic Verification II |
|
|
Siegle, Markus |
State-of-the-art techniques and tools for performability evaluation |
|
Tribastone, Micro |
Efficient State-Space Aggregations for
Large-Scale Dynamical Systems |
|
Zhao, Lin (赵琳) |
Runtime Checking Temporal Properties of System
Hybrid Behaviors |
|
Session 3 (13:30--15:00): Bounded Model Checking |
|
|
Bu, Lei
(卜磊） |
SAT-LP-IIS Joint-Directed Path-Oriented Bounded Reachability Analysis of Linear Hybrid Automata |
|
Zhang, Miaomiao (张苗苗) |
Bounded model checking of duration calculus |
|
Liu, Wanwei (刘万伟) |
Bounded Model Checking of Extended Temporal Logic
Cooperating Both Finite and Looping Automata Connectives |
|
Sesserion 4 (15:30--17:00): Probabilistic Verification II |
|
|
Zhang, Lijun （张立军） |
Probabilistic Model Checking for Linear Temporal
Logics |
|
Song, Lei |
|
|
Turrini, Andrea |
The Algorithmics of
Probabilistic Automata Weak Bisimulation |
