Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 IZEND1: Protocol Validation Home Page, Spring 2005
1. Motivation/Overview:
As our daily lives depend increasingly on digital systems, the reliability
of these systems becomes a concern of overwhelming importance, and as the
complexity of the systems grows, their reliability can no longer be
sufficiently controlled by traditional approaches of testing and simulation.
It becomes essential to build mathematical models of these systems,
and to use (algorithmic) verification methods to analyse these models.
During recent years there has been enormous progress in the areas of
hardware and software verification.
In this course, an overview will be presented of mathematical techniques for the
specification and validation of reactive hardware and software systems.
The application of these techniques will be illustrated via a series of
distributed algorithms and protocols as used, for instance,
in modern consumer electronics and within the internet.
Participants learn how to make formal models
and how to analyze them using state-of-the-art techniques and tools.
2. Objectives: General Objectives:
After successful completion of the course, participants are able to:
recognize situations in which the applications of formal methods
for specification and verification may be useful,
model distributed algorithms and protocols (or more generally:
reactive systems) as networks of automata,
formalize desired properties of these algorithms and protocols in terms
of automata or temporal logic, and
use state-of-the-art proof techniques and computer tools for the analysis
of distributed algorithms and protocols of "average" complexity.
Specific Objectives:
More specifically, at the end of the course participants:
are able to derive and manually prove invariants of (networks of) automata
defined in precondition/effect style,
are able to use model checking tools for checking of invariant properties,
are familiar with both the theory and application of the
I/O automaton model; are able to use this model for the modelling
of simple reactive systems at different levels of abstraction,
are familiar with concepts such as fairness, safety en liveness,
are able to describe properties of reactive systems as a conjunction of
safety and liveness properties,
are familiar with simulation relation based proof techniques for refinement,
are able to prove refinement relations using these techniques,
are familiar with linear and branching time temporal logics,
and with (symbolic) model checking algorithms,
are able to describe properties of reactive systems in temporal logic,
are familiar with extensions of the I/O automata model for modelling
of real-time, hybrid and probabilistic automata,
are familiar with the use of model checking tools for real-time and
hybrid systems.
3. Topics: Theory:
I/O automata model, invariant proof techniques, safety and liveness properties,
fairness, temporal logic, (symbolic) model checking, simulation proof
techniques, timed automata, hybrid automata, probabilistic automata. Tools:
IOA toolset, Murphy, Uppaal, .. Applications: Various distributed algorithms and protocols:
leader election for networks with ring, tree or general topology,
mutual exclusion algorithms, communication protocols for physical
and datalink layer, wave protocols such as distributed summation
algorithm, voting algorithms, security protocols, ..
Also, some case studies from the area of control will be discussed,
ranging from a trivial controller for a LEGO car, to the control software
for collision avoidance of airplanes (TCAS).
4. Time investment:
Participants are supposed to spend approximately 168 hours (=6ec) on this
course: during 14 weeks they will need about 6 hours per week to
attend+prepare classes (2 hours lectures, 2 hours problem session, 2 hours
reading and working on exercises at home).
In addition they will need about 28 hours for each of the three larger
homework assignments (to be made in small groups of 2 or 3 participants)
based on which their participation in the course will be evaluated.
Participants are expected to be present during the lectures and the
problem sessions.
5. Prerequisites:
Familiarity with propositional and predicate logic, finite automata,
basic complexity theory, and basic (graph) algorithms is assumed.
For instance, you should know what a tautology is,
how to formally prove a formula in predicate logic,
how to determinize a finite automaton,
what is the time complexity of sorting,
and how to find the strongly connected components of a graph.
The mathematics and theory courses from our bachelor curriculum
will certainly provide enough background (frequently, I will refer
to topics that have been previously addressed during the bachelor courses
courses such as Discrete Wiskunde, Talen, Beweren en Bewijzen,
Inleiding in de Complexiteitstheorie, Logica).
If you are not familiar with the concepts, please see the instructor.
6. Grading:
Grades will be awarded on the basis of three larger homework assignments,
which participants may do on their own of in groups of at most three
So instead of a final exam this course has "integrated examination".
The final score is obtained as the average of the scores for the three
assignments.
If the final score is 5 or below, participants will be offered the opportunity
to make a 4th homework assignment.
The final score will then be the average of the 3 highest scores
(so the lowest score may be dropped).
8. Course material:
The course material consists of
hand-outs, sheets, and recent papers from the literature.
These will be made available electronically via the course page or
distributed during the course.
A detailed list of
references and links is available.
9. When and where:
what
day
time
where
lectures
Wednesday
10.45-12.30
HG00.150
problem sessions
Thursday
13.45-15.30
HG00.150
See also the
schedule as generated by the NIII schedule generator.