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

Test and 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 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 the first part of the course, particular emphasis will be put on our own real-time validation tool UPPAAL,and (at your choice) the commercial tools visualSTATE and ESTEREL Studio . 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 and ESTEREL are toolsets that support analysis, design, prototyping, validation, and verification through simulation, code generation and testing of systems. The toolsets are based on the UML and MSC standards languages. Both tools provide 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 3 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 and Testing of Functional Programs and Automatic Test Generation in visualSTATE.

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 14 10.15-12.00, E1-214 Lecture1.pdf Introduction to Validation using UPPAAL, visualSTATE and ESTEREL
2. February 21 10.15-12.00, E1-214  Lecture2.pdf Modelling in UPPAAL. Timed Automata.
3. February 28 10.15-12.00, E1-214  Lecture3.pdf Verification Engine and Options of UPPAAL
4. March 8 12:30-16:00, PC-lab+ E1-214   Introduction to visualSTATE 
5. March 14 8.15-10.00, E1-214    More on visualSTATE
6. March 21 10.15-12.00, E1.214  Lecture6.pdf Lars Kornbeck, IAR visualSTATE
7. April 4 8.15-12.00, grouproom   Modelling Exercise
8. April 18 10.15-12:00, E1-214   jUnit Testing, Per Madsen
9. April 25 10.15-12.00, E1-214   Testing and Modelling at SIEMENS, Brian Nielsen
10. April 29- May 3     Testing week with Jan Tretmans, Twente University

 

Course material