|
|
|
|
::TUTORIALS::
August 31, 2008
Sabanci University
Campus
To
register for the tutorials, please fill in the Registration
Form and
(fax or email) it to the ICTAC'08 Registration Office
10:00-12:00 "Event-B and the Rodin Platform" by Jean-Raymond
Abrial [slides]
13:30-15:30 "Some non-standard authentication methods" by Bill
Roscoe [slides]
16:00-18:00 "A Formal Introduction to Model-Based Testing" by Jan Peleska
[slides]
"Event-B and the Rodin Platform"
by Jean-Raymond
Abrial
Abstract:
This tutorial is an introduction to the construction of complex systems
usingEvent-B and the Rodin
Platform.
Event-B is a mathematical formalism (based on first-order logic and set
theory) used to develop formal models of discrete transition systems. These
models are elaborated before effectively building these systems which are thus
intended to be correct by construction.
Discrete transition system is the unifying paradigm which can be used in
many different areas: sequential, distributed, concurrent, parallel. It also
covers larger systems where one takes into account not only the future software
but also its (fragile) environment.
Models are made of constants and variables related by possibly complex
invariants. Their dynamics is defined by means of transitions (called events)
made of guards (the enabling conditions) and actions (supposed to modify
variables in parallel).
Models are developed by means of successive refinements steps: from quite
simple and abstract to very concrete.When a model becomes too complicated, it can be decomposed into smaller
ones communicating in a systematic fashion.
Proofs and model-checking are performed at each step of the development.
They insure that each model is coherent and that it indeed refines its
abstraction (if any).
The Rodin Platform is the tool set which has been developed (as funded by
the European Project Rodin) to ensure a mechanical aid to the user of this
approach. This platform is open source and implemented on Eclipse. It works on
Windows, Linux and Mac-OS. It contains a database support which contains the
developed models. This database is surrounded by various plug-ins: provers,
model-checkers, animators, UML transformers, etc. New plug-ins can be added.
The intent of the tutorial is to explain all this in
greater details by means of various practical examples and tool demonstrations.
Jean-Raymond
Abrial is the co-inventor of Z, B and Event-B. He is the author of the B-book,
which presents the B-Method. He is currently finishing a new book on Event-B.
He was a guest Professor at ETH Zurich from 2004 to 2007 where he led the team
developing the Rodin Platform for Event-B (funded by the European Project
Rodin). He is currently a researcher also at ETH Zurich, working on a new
European Project called Deploy. Before being in Zurich, he was a consultant for
more than 20 years working in close contact with Industrial Companies but also
with various Universities around the world.
"Some
non-standard authentication methods" by Bill Roscoe
Abstract:
This tutorial will cover new methods of message and entity
authentication developed both by the Oxford group and others over the past
years, based on the use of a high bandwidth standard (insecure) channel and a
lower bandwidth authentic one. In most,
but not all, of the scenarios we will consider, the authentic one is
implemented by one or more human beings.We will a wide range of topics in this tutorial, including protocol
design, new cryptographic primitives, human factors, implementation and
efficiency.
Bill
Roscoe is the author of more than 120 books and papers on computer science and
mathematics. He has been a professor of computer science at Oxford for the past
11 years, and the head of department there for 5.He is best known for his work on the theory
and applications of Hoare's CSP, and has also done significant work on computer
security (information flow, protocol analysis and protocol design) as well as
hardware verification (having led the team that performed the first-ever
verification of a floating point unit in 1989).
"A
Formal Introduction to Model-Based Testing" by Jan Peleska
Abstract:
In this tutorial an introduction to model-based
testing is given. We start with a classical theorem by Chow who showed that
black-box tests can prove the equivalence of a system under test (SUT) with its
(finite, deterministic, untimed) automata specification, if an upper bound of
the number of internal SUT states is known. It is sketched how this result
could be generalised by Vaandrager et. al. to Timed Automata. Since equivalence
(i.e. bi-similarity) may be too restrictive as a relation between specification
and SUT, it is interesting to observe that a similar approach is possible for
process algebras such as CSP, CCS or Lotos and the refinement relations defined
for these algebraic models, as has first been observed by Hennessy and de
Nicola.
While these results provided very valuable insight
into the theoretical foundations of testing, equivalence testing requires to
investigate so many test cases that the practical applicability is very
restricted (though certainly not impossible, as an example from the field of
"real-world" railway control systems will show). As a consequence, it
is interesting to investigate the elaboration of test strategies which - though
not capable of proving equivalence between SUT and its specification -
guarantee to come up with "useful" test cases which can be
automatically generated and executed within acceptable time. We give an
overview of the underlying heuristics of test strategies that are relevant in
the field of safety-critical embedded systems testing. Moreover, the constraint
solving problems associated with the test case generation tasks are described,
together with automated solver techniques.
Jan
Peleska studied mathematics and wrote his doctoral thesis on a topic in the
field of differential geometry at the University of Hamburg. From 1984 to 1990
he worked with Philips as Senior Software Designer and later on as department
manager in the field of fault-tolerant systems, distributed systems and
database systems. From 1990 to 1994 he was manager of a department at Deutsche
System-Technik responsible for the development of safety-critical embedded
systems. Since 1994 he has worked as a consultant, specialising on development
methods, verification, validation and test of safety-critical systems. His
habilitation thesis focusing on Formal Methods for the development of
dependable systems was finished in 1995. Together with his wife Cornelia
Zahlten, he has founded the company Verified Systems International GmbH in
1998, providing tools and services in the field of safety-critical system
development, verification, validation and test. His current research interests
include formal methods for the development of dependable systems, test
automation based on formal methods with applications to embedded real-time
systems, verification of security properties, and formal methods in combination
with CASE methods. Current industrial applications of his research work focus
on the development and verification of avionic software, space mission systems
and railway and automotive control systems. He is associated with the Center
for Computing Technology TZI at the Department of Mathematics and Computer
Science of Bremen University and was TZI director from September 2001 to
September 2003. Together with his colleague Rolf Drechsler he manages the Post
Graduate Programme Embedded Systems GESywhich has been founded in 2006.