Testing, Verification and Validation (6 ECTS)
The purpose of this course is to understand the role of testing, verification and validation in the design and analysis of systems, and to provide an advanced background on related methods and tools.
The course introduces the basis concepts of formal modelling and specification techniques that can be used for verification and validation: model checking, theorem proving, static analysis and abstract interpretation.
The course also presents the fundamentals of software testing. It provides an understanding of testing problems, and covers the major test design techniques. Emphasis is put on the need for rigorous, semi-automated approaches.
- Model checking
- Temporal logics as a foundation for model checking
- Modelling of systems for model checking
- Standard techniques for model checking, including BDD-based model checking
- Theorem proving
- Logical foundations
- Specification and verification with a theorem prover tool
- Static program analysis
- Static program analysis definition and main application areas
- Data-flow analysis
- Basic elements of abstract interpretation theory
- Software testing
- Fundamentals of testing: role of testing throughout the software life cycle, test selection and oracle problems, test integration strategy, classification of test methods.
- Usual structural & functional approaches: control and data flow criteria, predicate coverage, domain testing, model-based testing (e.g., from finite state machines, labelled transition systems).
- Mutation analysis: principle, examples of usage.
- Probabilistic test approaches: uniform profile, operational profile, profiles based on structural and functional criteria.
T. Kropf: Introduction to Formal Hardware Verification, Springer, 1999.
B. Berard, et al.: System and Software Verification – Model-Checking Techniques and Tools, Springer, 2001.
C. Hankin, F. Nielson, H. R. Nielson: Principles of Program Analysis, Springer, 1999.
A. V. Aho, M. S. Lam, R. Sethi, J. D. Ullman: Compilers: Principles, Techniques, and Tools, Addison-Wesley, 2006.
P. Cousot, R. Cousot: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL77, pages 238–252, Los Angeles, California, 1977.
P. Cousot, R. Cousot: Systematic Design of Program Analysis Frameworks, POPL79, pages 269–282, San Antonio, Texas, 1979.
B. Beizer: Software Testing Techniques, Van Nostrand Reinhold, 1990 (2nd edition)
R. D. Craig, S. P. Jaskiel: Systematic Software Testing, Artech House, 2002
A. Robinson, A. Voronkov (eds.): Handbook of Automated Reasoning, Volume I, North Holland, 2001
ReSIST Courseware (right click and select "Save as" to download)
Courseware examples and locations where taught:
- "Computer-Aided Verification", Rajeev Alur at University of Pennsylvania, Philadelphia, USA, http://www.cis.upenn.edu/cis673/, Slides and draft textbook available
- "Deductive Verification of Reactive Systems", Amir Pnueli at The Weizmann Institute of Science, Rehovot, Israel http://www.wisdom.weizmann.ac.il/~amir/Course02a/header.html, Slides available
- "Test and Verification" Emmanuel Fleury, Kim G. Larsen, Brian Nielsen, Arne Skou at Aalborg University, Denmark http://www.cs.auc.dk/~kgl/TOV04/Plan.html, Slides available
- "Theorem Proving and Model Checking in PVS" Edmund M. Clarke and Daniel Kroening at CMU, Pittsburgh, USA http://www.cs.cmu.edu/~emc/15-820A/ Slides available
- "System Validation" Theo C. Ruys at University of Twente http://fmt.cs.utwente.nl/courses/systemvalidation/ Slides available
- "Validation and Verification" J.P. Bowen at University College London http://www.cs.ucl.ac.uk/staff/J.Bowen/GS03/ Slides available
- "Abstract Interpretation" Patrick Cousot, Jerome Clarke Hunsaker at MIT http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www Slides available
- "Abstract interpretation and static analysis", David Schmidt at International Winter School on Semantics and Applications, Uruguay, 2003 http://santos.cis.ksu.edu/schmidt/Escuela03/home.html Slides available
- "Introduction to software testing" Paul Ammann and Jeff Offutt at George Mason University http://www.cs.gmu.edu/~offutt/softwaretest/powerpoint/ Slides available
Line of teaching
View this course in the RKBExplorer
Back to MSc Curriculum.