Test and Verification 2006


Kim Guldstrand Larsen
Brian Nielsen
Arne Skou


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 both formal verification techniques as well as testing techniques are needed in order to deal with this growing complexity.  This is in particular true in areas such as embedded systems used in consumer electronics, time dependent systems occurring in safety critical systems and communication protocols from the telecommunication industry.

The focus of this course is on techniques and software-tools that can be used to assess the quality and correctness of software systems. The first part of the course considers tools and techniques for formal verification of system designs. The last part of the course considers tools and techniques for testing system implementations.

In a (logical) first part of the course, particular emphasis will be put on our own real-time validation tool UPPAAL. Later in the course, the commercial tool visualSTATE will also be presented. In the course we will evaluate the usefulness of the various features of these tools. Emphasis will be on application and hands-on experiment with the tools on small case-studies. 

  • Uppaal allows for the modeling, validation and automatic verification of properties of real-time systems and communication protocols The underlying description language and specification formalism --- timed automata and timed temporal logic --- will be dealt with in detail.  The theoretical and practical aspects of the tool 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. 
  • visualSTATE is a toolset that supports analysis, design, prototyping, validation, and verification through simulation, code generation and testing of systems. The toolset is based on the UML and MSC standards languages. visualSTATE provides graphical editors, simulators, a C code generator targeting real-time OS and network protocols, and a design-level debugger. 

In the (logical) second part of the course, emphasis will be on methods and techniques for testing. 

In addition, the course will involve guest lectures from colleagues at other universities.

Objectives

The aims of the course are that the students become familiar with the possibility of validating software systems based on formal models and specifications (in particular of real-time and embedded systems) with the aid of software tools for the verification and analysis, and that they learn practical techniques and methods for testing software systems.

Preliminary schedule

 

 

 

 

No.

Lecture date

Lecture

room

Exercise

room

Slides

Subject

 

1.

February 14

B2-104

 

Introduction

Introduction

2.

February 21

E3-109,12:30

PC-Lab

 Modelling in UPPAAL

Modelling in UPPAAL. Timed Automata.

 

3.

February 23

E3-109,8:15

PC-Lab

  

Verification Engine and Options of UPPAAL

 

4.

March 2

E3-209,12:30

PC-Lab

 

Modelling Exercise

 

5.

March 7

E3-209,12:30

Group Rooms

Slides

Introduction to testing

 

6.

March 9

 E3-209,12:30

 Group Rooms

Slides 

Classical testing

 

7.

March  16

E3-209,12:30

Group Rooms

Slides

FSM Testing

 

8.

March 21

E3-209,8:15

Group Rooms

 

Testing Object Oriented Programs

 

9.

March 23

E3-209,12:30

Group Rooms

Slides

Uppaal TRON

 

10.

April 3

E3-209,8:15

Group Rooms (9-10:A4-106)

  

Testing Exercise

 

11.

April 7

E3-209,8:15

PC-Lab

  

VisualState I

 

12.

April 7

E3-209, 12:30

PC-Lab

  

VisualState II

 

13.

May 9

E3-209, 12:30

Group Rooms

  

CyNC calculus

 

14.

May 19

B2-104

Group Rooms

  

Probabilistic Model Checking

 

15.

TBA

B2-104

Group Rooms

  

TBA III

 

 

Course material