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
[go: Go Back, main page]

VERIFICATION

Kim Guldstrand Larsen
 


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.

In the course we shall concentrate on fully automatic formal verification (coined model checking by Ed Clarke). The course will cover the area  through  a number of prototypical automatic verification tools illustrating the models, specification formalisms, and underlying algorithmic techniques within the area.  Opportunities of getting hands-on experience with these tools will be given.
 

Objectives

The primary aim of the course is that the students becomes familiar with  state-of-the art algorithmic techniques and datastructures for model-checking computer based systems, and the way the techniques both depends and utilizes the choice of formalisms for modelling and specifying the system various technques.  The secondary aim is that the student obtains hands-on experience with the techniques and formalisms via a range of tools.
 

Preliminary Schedule

 
No. Lecture date Subject
1. April 26 Introduction.Binary Decision Diagrams
2. None Selfstudy. Work on Exercises to hand in.
3. May 10 LTL, Büchi Automata, Partial Order Reduction.SPIN.NuSMV
4. None Selfstudy. Work on Exercises to hand in.
5. May 25 Modelling Real Time Systems. Timed Automata. UPPAAL
6. None Selfstudy. Work on Exercises to hand in..

 

COURSE MATERIAL

Chapters from

TOOLS

CWB:
     If not already you will become (somewhat) familiar with the tool CWB (the Concurrency
     Workbench), its underlying model (CCS, bisimulation) and specification language (the modal
     mu-calculus). We will illustrate various basic algorithmic techniques for equivalence
     and model checking.

SPIN:
     The tool SPIN, developed by researchers at AT&T, is one of the most commonly
     used tools in the verification of real life communication protocols. One of the
     distinguishing features of this tool is the use it makes of the techniques based
     on the so-called 'partial-order reduction method' to alleviate the well known
     problem of combinatorial state-explosion.

visualSTATE:
     visualSTATE is developed by the danish company BEOLOGIC A/S and is a design tool
     used by many companies for developing embedded software in a variety of embedded
     applications ranging from simple controllers to very large advanced interactive
     simulators.
     Together with BRICS at Aalborg and Computer Systems Section at Denmarks
     Technical University, the BEOLOGIC is now developing a new generation of the
     visualSTATE tool that will move the limit  on the complexity of the embedded
     software that can be verified by several orders of magnitude.  The underlying
     technique is exploiting the art of symbolic model checking  using Binary
     Decision Diagram (BDDs), a notion which will be covered in the course.  The
     developed technique itself - on which a patent is currently being filed - will
     also be illustrated.

UPPAAL:
     Since the emergence of the notion of timed automata introduced by Alur and Dill
     in 1990 a number of real-time verification tools has emerged, including UPPAAL.
     UPPAAL  has been developed in collaboration between Uppsala University and BRICS
     at Aalborg.  In addition to classical techniques for dealing with discrete
     state-spaces, real-time verification tools such as UPPAAL deals with the
     continuous part of  a state-space through a variety  of data structures and
     techniques for representing and manipulating subsets of the Euclidean space.

INTERESTING LINKS