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 2005

Test and Verification 2005

Emmanuel Fleury
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, the commercial tools visualSTATE and Cinderalla. In the course we will toevaluate 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.
Cinderella is a collection of software development tools supporting standardised notations like SDL, ASN.1, MSC, and UML for system design, specification and implementation. SDL (Specification and Description Language) graphical specification language standardized by ITU (International Telecommunication Union). Although SDL is widely used in the telecommunications field, it is not designed specifically for describing telecommunications services. Rather SDL is a general purpose specification language for communication systems and embedded systems.

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 industry, e.g. presentations from IAR Systems A/S (the provider of visualSTATE), presentations of SDL/Cinderalla by Professor Andreas Prinz, Agder University College, Norway, and presentations on testing in current industrial practise.

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	8.15-10.00	10.15-12.00	Slides	Subject
1.	February 3		E3-209	Introduction	Introduction
2.	February 10	E3-209	PC-Lab	Modelling in UPPAAL	Modelling in UPPAAL. Timed Automata.
3.	February 17	E3-209	PC-Lab		Verification Engine and Options of UPPAAL
4.	February 24	E3-209	PC-Lab	Slides	Introduction to visualSTATE
5.	March 2	E2-214	PC-Lab	Slides	More on visualSTATE
6.	March 10	PC-Lab	PC-Lab		Modelling Exercise
7.	March 17	E3-209		Slides	Software Validation (Blast and Slam)
8.	March 31	E3-209	Group Rooms	Introduction	Introduction to Testing
9.	April 7	E3-209	Group Rooms	Slides	Classical Testing
10.	April 14	E3-209	Group Rooms		Testing of Object Oriented Programs, Per Madsen
11.	April 21	E3-209	Group Rooms		Model-based Testing of Real-Time Systems
12.	April 26	E3-209	PC-Lab		SDL Basics and Structure, guest lecturer Andreas Prinz 12.30-14.15 (optional) Test driven development with SDL (optional for you)
13.	April 28	E3-209	PC-Lab		SDL Behaviour and Cinderalla, guest lecturer Andreas Prinz 12.30-14.15 (optional): Connection to Real Hardware
14.	May 12	E3-209	Group Rooms		Test exercise
15.	May 18	14.15-16.150 E3-109			Test in Practice, Niels Andersen, GateHouse

Course material

Behrmann, David, Larsen: A Tutorial on UPPAAL.
Bengtson, Wang: Timed Automata: Semantics, Algorithms and Tools
[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 "
More will be added later ....