Test and Verification 2007

 

Lecturers:


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. 

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.

Involved Semesters

Due to teaching capacity constraints and and study-board honorary we need to give the course jointly for several semesters.

 

Preliminary schedule

No.

Dat8 SW8 SP2 D4 C6

Lecture date

Lecture

room

Exercise

room

Lecturer

Slides

Subject

1.

2 February A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

KGL

Introduction

Introduction

2.

  9 February A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

KGL

 Modelling in UPPAAL

Modelling in UPPAAL. Timed Automata.

3.

  16 February A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

KGL

  Engine and Options

Verification Engine and Options of UPPAAL

4

    23 February

NO LECTURE

Group Rooms

+PC-Lab: E1-110

KGL

Hand in

March 26

Modelling Exercise

5.

  2 March A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

BN testIntro

Introduction to testing

6.

 9 March

A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

ASk whitebox

Classical Test 1:

(Test case design teknikker I: Whitebox + Coverage)

7.

16 March

A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

ASk blackbox,cu_unit

integration

 

Classical Test 2:
Test case design teknikker II: Blackbox + xUnit+integrationTest

13.

      23 March A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

Jacob Illum

  

Planning & Scheduling
Uppaal CORA

8.

 

30 March

A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

BN fsm-based

Model-Based Testing:
(FSM based and OO test)

            6 April         Påske

9.

 

13 April

A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

BN RT-Test

Model-Based Testing:

(Online Realtime Uppaal TRON)

15

  20 April A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

Guest

  

SW Test in Practice (TK-Validate)

10a.

    27 April A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

BN

  

Testing Exercise

10b        

(On Request)

 

Group Rooms

BN   Project Consultancy
            4 May         St. Bededag

11.

      7 May E3-209
8.15-10.00

Group Rooms

+PC-Lab: E1-110

Andrezej/Ulrik

  

VisualState I

12.

     

16 May

E3-209
8.15-10.00

Group Rooms

+PC-Lab:E1-110

Andrezej/Ulrik

  

VisualState II

14.

      23 May A4-108
8.15-10.00

Group Rooms

+PC-Lab: E1-110

KGL

  Probabilistic Modeling & Logics

Performance Modelling:
Probabilistic Model Checking

          ?     BN/Schiøler   ?Test of Logical Circuits
          ?     BN/Schiøler   ?Test & Verification of FPGA SW

 

Course material