The goal of the course is to introduce techniques for verifying and validating software properties, either by analysing a model extracted from a program with model checking, or by testing the software before (the next) deployment, or equipping the running software with tools that monitor its execution.
- Specifying software properties [2 CFU]
o Assertions
o Invariants, Safety and Liveness Properties, Fairness
o Temporal logics: LTL, CTL, CTL*
- Model Checking [4 CFU]
o Transition systems and Program graphs
o Checking regular safety properties
o Checking omega regular properties with Büchi automata
o Overview of Promela-SPIN and SMV
o Extracting models from Java source code: BANDERA
- Testing [3 CFU]
o Coverage criteria and metrics: statement, function, branch, path and data-flow coverage
o Test cases selection, prioritization and minimization
o Automatic generation of test cases
Topics to be chosen among:
o Component-based and Service-oriented system testing
o Object-oriented testing and Junit
o Access Control Systems testing
o Performance and other non-functional aspects testing