Tutorials
- Tutorial 1: Uncertainty Modeling in Cyber-Physical Systems
- Tutorial 2: Security, specification and refinement
Tutorial 3: Executable Models of Gene Regulatory Networks (Canceled)Tutorial 4: The DisCoVeri continues ... (On the Application of Concurrency Theory to Fault-Tolerant Distributed Algorithms) (Canceled)
Tutorial 1: Uncertainty Modeling in Cyber-Physical Systems
Summary
This tutorial will be research oriented, intending to introduce the audience into the state of art and the research problems in a newly emergent domain. The tutorial format is interdisciplinary and multi-speakers, offering perspectives from complementary disciplines.
Cyber physical systems represent a modelling paradigm that promotes a holistic perspective on systems that have been previously known as embedded, hybrid, or pervasive. The essential feature of the cyber physical systems is the deep interaction between physics and computation and their behaviour, as well as the interaction with their environment or other systems. The tutorial lectures will present a systematic methodological framework for the holistic modelling. The illustrating examples show the extraordinary application potential of this paradigm. The applications span from nano-scale robots to mega-scale satellites and aircraft. The tutorial will focus on modelling the uncertainty, which is inherent in the behaviour of these complex systems.
More Info
Full-day Tutorial on Sunday Morning. March 21, 2010
Tutorial 2: Security, specification and refinement
Summary
Since 1995 [1] there has been intensive research in source-level assertion-style reasoning for developing probabilistic systems via stepwise refinement [2] through layers of abstraction [3], which work was summarised in a comprehensive text [4] in 2005. Since then the method has been adapted to deal with non-interference-style security, initially without probability [5]
but most recently with probability as well [6].
This tutorial will build on a basic understanding of specification and refinement to explain these recent developments and how they fit in to research themes which overlap secure systems and quantitative reasoning. In particular it will focus on systematic source-level developments of a number of well known probabilistic and security-sensitive algorithms, as examples, as well as explaining and illustrating general principles for doing work of this kind. There are many opportunities of up-to-the-minute topics for further research.
[1] Probabilistic predicate transformers. Morgan, McIver, Seidel. ToPLaS 18(3), 1996.
[2] Program development by stepwise refinement. Niklaus Wirth. CACM 14(4), 1971.
[3] The B Book. J-R Abrial. Cambridge University Press, 1996.
[4] Abstraction, Refinement and Proof for Probabilistic Systems: McIver and Morgan. Springer Monographs in Computer Science. 2005.
[5] The Shadow Knows: Refinement of ignorance in sequential programs. Carroll Morgan. In LNCS 4014 Proc. MPC 2006, Tarmo Uustalu (ed).
[6] Security, probability and nearly fair coins in the cryptographers' café. Carroll Morgan. Invited talk in LNCS 5850, Proc. FM09. Cavalcanti, Dams (eds).
More Info
Full-day Tutorial on Sunday Morning. March 21, 2010
Tutorial 3: Executable Models of Gene Regulatory Networks
Summary
In this tutorial, we will give an introduction to what is phrased executable biology, and
the role that formal methods in this context. We will focus on Petri nets, which constitute
an excellent formalism for modelling biological systems, in particular gene regulatory networks.
We will explain the basic formalism, the analysis method based on Monte Carlo simulations and
on state space exploration. The framework will be explained on the basis of three different
case studies. The first case study is vulval development of C. elegans, where the Petri
net simulations turn out to be in line with in vitro experiments, and moreover new predictions
can be made. Next we will explain how to use Petri nets to build the gene regulatory network
that captures the hematopoiesis process in mice and how is possible to infer, check, and
predict biological properties exploring the generated state space. Furthermore, we will show
how we applied the same approach to derive insightful predictions on Yeast behavior during
starvation. Moreover, we will present a proof-of-concepts tool used to design and analyze our
models. Finally, we will discuss future perspectives, especially with regard to model checking
analysis.
More Info
Half-day Tutorial on Sunday Morning. March 21, 2010
Tutorial 4: The DisCoVeri continues ... (On the Application of Concurrency Theory to Fault-Tolerant Distributed Algorithms)
Summary
The formal verification of distributed algorithms, in particular fault-tolerant ones, still represents a rather non-trivial challenge. The field of Concurrency Theory offers a range of methods and techniques to formally specify and possibly verify concurrent and distributed systems. In this tutorial, we elaborate on a number of different techniques that are often expected to be adequate on this matter. Among them, we touch upon process calculi, temporal logics, I/O automata as well as abstract state machines and the HO model. The emphasis is put on the general approach and applicability of the above-named methods, usually referring to either the comparison between specifications and abstract implementations, using notions of equivalence or simulation, or the satisfaction of logical formulae by such an implementation. A number of examples are presented, where we focus on variants the Disributed Consensus problem; advantages and disadvantages as well as potential pitfalls are outlined.
Half-day Tutorial on Sunday Afternoon. March 21, 2010
Satellite Events Chairs
The satellite organisers can be contacted by sending e-mail
to <etaps10_satellite_events@cs.ucy.ac.cy>.