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
Test and Verification

Test and Verification 2003

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 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 (see CISS).

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 model-based validation/verification of system designs. The last part of the course considers tools and techniques for testing system implementations.

In the first part of the course, particular emphasis will be put on our own real-time validation tool UPPAAL and the commercial tool visualSTATE. 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 this course we will try to evaluate the usefulness of the various features of the 2 tools above (by application on small case-studies).

In the second part of the course, emphasis will be on methods and techniques for testing. This part of the course will to a large extent be given by Jan Tretmans (Nijmegen University, The Netherlands).

In addition, the course will involve guest lectures on topics such as Object Oriented Testing,Testing of Functional Programs and Run Time Validation of Real Time Systems.

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	Time and Place	Slides	Subject
1.	February 12	10.15-12.00	Lecture1.pdf	Introduction
2.	February 19	10.15-12.00	Lecture2.pdf	Modelling: Hierarchical State Machines
3.	February 26	Exercises in PC-Lab 8.15-10.00. See exercises under Lecture 2 10.15-12.00, E1-214		Verification and Code Generation
4-9.	March 3-6	More detailed plan to be announced		Testing week with Jan Tretmans, Twente University
10.	March 12	Exercises in PC-lab 8.15-10.00. See exercises under Lecture 3. 10.15-12.00, E1.214		jUnit Testing & Testing by Contract, Per Madsen
11.	March 19	10.15-12.00, E1-214	Lecture11.pdf Emmanuel.pdf	Real Time Modelling
12.	March 26	Exercises in PC-lab 8.15-10.00. See exercises under Lecture 11. 10.15-12:00, E1-214	Lecture12.pdf	Real Time Verification
13.	March 28	Exercises in PC-lab 8.15-10.00. See exercises under Lecture 12. 10.15-12.00, E3-209		IAR visualSTATE by Henrik Leerberg
14-15.	April 2 April 14	Hand in by April 30 (latest)		Modelling Exercise

Practical Exercises with UPPAAL and visualSTATE will take place in the PC-lab in E1.

Lectures

Course material

[JPK] Joost-Pieter Katoen: " Concepts, Algorithms, and Tools for Model Checking ". (Lecture Notes)
[AD] Alexandre David: "Uppaal2k Tutorial "
[UPPAAL] Larsen, Pettersson, Yi: " UPPAAL in a Nutshell ", in Journal for Software Tools for Technology Transfer vol 1, 1997.
[LSW] Laarsen, Pettersson, Yi: "Continuous Modeling of Real Time and Hybrid Systems", * in Journal for Software Tools for Technology Transfer, vol 1, 1997.
[CW] Edmund M. Clarke and Jeanette M. Wing: " Formal Methods: State of the Art and Future Directions "
[JPK2]: Joost-Pieter Katoen: System Verification .
[CK] Edmund M. Clarke and Robert P. Kurshan: " Computer-Aided Verification "
[SALLT+] Jørgen Staunstrup, Henrik Reif Andersen, Kim G. Larsen, Henrik Leerberg, Niels Bo Theilgaard et al.: "Practical Verification of Embedded Software "
[HSLL] Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund: " Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL "
Various local Theses and Papers on Hierarchical State Machines.
More will be added later ....