Topics of Interest
In cooperation with:
Jose Meseguer - University of Illinois at Urbana-Champaign, USA
Title: Symbolic Formal Methods: Combining the Power of Rewriting, Narrowing, SMT Solving and Model Checking
Abstract: Symbolic techniques that represent possibly infinite sets of states by symbolic constraints and
support decision or semi-decision procedures based on such constraints have become essential to automate large
parts of the verification effort and make verification much more scalable. They include: (i) SMT solving; (ii)
rewriting- and unification-based techniques, including rewriting and narrowing modulo theories; and
(iii) automata-based model checking techniques, which describe infinite sets of states and/or system traces
symbolically by various kinds of automata. However, a key problem limiting the applicability of current
symbolic techniques is lack of, or limited support for, extensibility. That is, although certain classes of
systems can be formalized in ways that allow the application of specific symbolic analysis techniques, many
other systems of interest fall outside the scope of such techniques. There is a real need to extend and combine
the power of symbolic analysis techniques to cover a much wider class of systems. The talk will present some
recent advances towards the goal of combined, extensible symbolic formal methods within the context of
rewriting logic and Maude.
Wolfgang Reisig - Humboldt-Universität zu Berlin, Germany
Title: Service Oriented Computing: Forthcoming challenges
Abstract: Service-oriented Computing has established itself as a core paradigm of modern software architectures. Nevertheless, some obstacles prevent even more widespread use of service oriented architectures (SOAs). To overcome those obstacles, in particular the following questions have to be addressed:
Those questions cannot seriously be answered on an intuitive, informal level. It is inevitable to model services in a formal framework, with the decisive properties of the services be represented as properties of their formal models. The above questions are then addressed and faithfully solved in the framework of the formal models. To this end we suggest methods and principles of formally modeling and analyzing SOAs.
SOAs are more and more implemented in the cloud. To what extent are the stakeholders affected by this change of technology?
It turned out useful to conceive not only software components, but also humans and technical systems as service providers and service requesters. How can a unified approach to SOA cope with this?
Basic notions such as correctness and equivalence are clear cut and undisputed for classical programs. Are there corresponding generally acceptable and manageable such notions for SOAs?
Quick assignment of needed data, software and hardware to services is inevitable for smoothly running SOAs. How can a small, flexible infrastructure guarantee this kind of elasticity?
Holger Hermanns - Saarland University, Germany
Title: Stochastic, Hybrid and Real-Time Systems: From Foundations To Applications with Modest
Abstract: Our reliance on complex safety-critical or economically vital systems such
as networked automation systems or “smart” power grids increases at an everaccelerating
pace. The necessity to study the reliability and performance of these
systems is evident, but purely functional models and properties are insufficient
in many cases. This has led to the development of integrative approaches that
combine probabilities, real-time aspects and continuous dynamics with formal
Today, formal quantitative modelling and analysis is supported by a wide
range of tools and formalisms such as Prism with probabilistic guarded commands,
Uppaal for graphical modelling and verication of timed automata, or
hybrid system model checkers like Phaver. This variety of different languages
and tools, however, is a major obstacle for new users seeking to apply formal
methods in their field of work.
To overcome these problems, the Modest [4,6] modelling language and its
underlying semantic model of stochastic hybrid automata (SHA) have been designed
as an overarching formalism of which many well-known and extensively
studied models such as Markov decision processes, probabilistic timed systems
or hybrid automata are special cases. The construction and analysis of SHA
models is supported by the Modest Toolset , which supports analysis with
a range of different methods. At the current stage, the following analysis components
are available: prohver  handles probabilistic safety properties for SHA;
mcpta performs model checking of probabilistic timed automata using Prism;
mctau  connects to Uppaal for model checking of timed automata, for which
it is more efficient than mcpta; and modes  performs statistical model checking
and simulation of stochastic timed automata with an emphasis on the sound
handling of nondeterministic models.
The Modest Toolset has been used for a variety of applications with different
levels of complexity and of expressiveness. These include really cool safety
critical hard real-time wireless control applications for bicycles  as well as
high-speed trains , and innovative electric power grid control strategies .
The applications combine different abstraction and analysis techniques supported
by the Modest Toolset.
The Modest Toolset website, www.modestchecker.net.
Jonathan Bogdoll, Alexandre David, Arnd Hartmanns, and Holger Hermanns.
mctau: Bridging the gap between Modest and UPPAAL. In SPIN, volume 7385
of LNCS, pages 227–233. Springer, 2012.
Jonathan Bogdoll, Arnd Hartmanns, and Holger Hermanns. Simulation and statistical
model checking for Modestly nondeterministic models. In MMB/DFT, volume
7201 of LNCS, pages 249–252. Springer, 2012.
H. C. Bohnenkamp, P. R. D’Argenio, H. Hermanns, and J.-P. Katoen. MoDeST:
A compositional modeling formalism for hard and softly timed systems. IEEE
Transactions on Software Engineering, 32(10):812–830, 2006.
Hernan Baro Graf, Holger Hermanns, Juhi Kulshrestha, Jens Peter, Anjo Vahldiek,
and Aravind Vasudevan. A verified wireless safety critical hard real-time design. In
WOWMOM, pages 1–9. IEEE, 2011.
Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, and Joost-Pieter Katoen.
A compositional modelling and analysis framework for stochastic hybrid systems.
Formal Methods in System Design, 2012.
Arnd Hartmanns, Holger Hermanns, and Pascal Berrang. A comparative analysis of
decentralized power grid stabilization strategies. In Winter Simulation Conference,