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 Real-Time Systems: Course Plan
There is a strong need for the use of advanced,
systematic techniques and tools that support the system validation
process. [Klaus
Havelund]
Brief course description
Software is becoming
increasingly complex and there is a growing awareness within software engineering
practice that formal verification techniques are helpful in dealing with
this growing complexity. In particular, formal verification is finding
its way into areas such as embedded systems as used in consumer electronics,
time dependent systems occurring in safety critical systems and communication
protocols from the telecommunication industry.
The focus of the
course is on techniques and software-tools that can be used to assess the
quality and formal correctness of such systems. Particular emphasis will
be put on the tools UPPAAL and
SPIN,
which allow for modeling, validation and automatic verification of properties
of real-time systems and communication protocols. The underlying description
languages, including (timed) automata and PROMELA, and specification formalisms,
(timed) temporal logic, will be dealt with in detail. The theoretical
and practical aspects of the tools will be studied. To enable effective
validation of systems special attention is given to modeling and
abstraction techniques that help to limit the complexity of the models
used.
In addition to the
lectures this course will be based on elaboration of a number of concrete,
practical exercises. Some of these exercises are based upon real-life applications,
such as protocols for Philip's consumer electronics systems (BRP), SAAB/VOLVO
gear controllers, etc.
Objectives
The aim of the course
is that the students learn to validate formal specifications, in particular
of real-time systems, with the aid of software tools for the verification
and analysis. In addition, they should learn to understand the main underlying
theoretical and practical problems.
TOPICS
Introduction to model
checking.
Abstract models and
specifications of timed systems:
Finite state machines and CTL,
Timed Automata and TCTL..
The verification
tool UPPAAL:
Modeling and verification.
Case studies.
SPIN and PROMELA;
Büchi Automata
and LTL;
modeling and validation
of communication protocols.
Formal specification
of real-time properties using Duration Calculus (DC),
an interval-based temporal logic.
Implementation of
real-time programs:
Schedulability, languages, operating systems.
The form of the course
will be lectures, exercise classes, programming labs and a project.
The course is evaluated
by assessment of a project report to be carried out in smaller groups.