STINT PhD Course on Enabledness Preserving Abstractions

August 27, 2019
Room 8103 (EDIT building, Johanneberg, Chalmers)
Gothenburg, Sweden

Lecturers: Sebastián Uchitel, Diego Garbervetsky

Examiner: Gerardo Schneider

DESCRIPTION

Many software engineering artefacts, such as source code or specifications, define a set of operations and impose restrictions to the ordering on which they have to be invoked. Enabledness Preserving Abstractions (EPAs) are concise representations of the behaviour space for such artefacts. In this short course we will present EPAs, how to build them and how they can be used for a variety of software engineering tasks.

============================================

LECTURES

Lecture 1:
- Introduction to model driven development.
- Validation vs Verification.
- Behavioral models.
- Use of abstraction for Validation and Verification.
- Introducing Enabledness Preserving Abstractions (EPAs).

Lecture 2:
- Building EPAs for contracts.
- Validation of contracts using EPAs.
- Findings on real artifacts.
- Validation hints.

Lecture 3:
- Validation of classes using EPA.
- Introduction to software model checking.
- Building EPAs for C programs.
- Building EPAs for OO programs using the Boogie/Corral approach.

Lecture 4:
- Testing with EPAs: manual and automatic test generation ŕ la model-based.
- Combining search-based approach with abstract behavioral models.
- Typestate strengthening using EPAs.

============================================

EXAMINATION

Students will be required to engage in a project, which will consist in reading one technical paper from the literature on the topic and make a public presentation of the paper.

BIBLIOGRAPHY

- Guido de Caso, Víctor A. Braberman, Diego Garbervetsky, Sebastián Uchitel: Enabledness-based program abstractions for behavior validation. ACM Trans. Softw. Eng. Methodol. 22(3): 25:1-25:46 (2013)
- Guido de Caso, Víctor A. Braberman, Diego Garbervetsky, Sebastián Uchitel: Automated Abstractions for Contract Validation. IEEE Trans. Software Eng. 38(1): 141-162(2012)
- Guido de Caso, Víctor A. Braberman, Diego Garbervetsky, Sebastián Uchitel: Abstractions for Validation in Action. SFM 2012: 192-218 2011
- Edgardo Zoppi, Víctor A. Braberman, Guido de Caso, Diego Garbervetsky, Sebastián Uchitel: Contractor.NET: inferring typestate properties to enrich code contracts. TOPI@ICSE 2011: 44-47
- Guido de Caso, Víctor A. Braberman, Diego Garbervetsky, Sebastián Uchitel: Program abstractions for behaviour validation. ICSE 2011: 381-390
- Guido de Caso, Víctor A. Braberman, Diego Garbervetsky, Sebastián Uchitel: Validation of contracts using enabledness preserving finite state abstractions. ICSE 2009: 452-462