Formalware Engineering: Formal Methods for Engineering of Software
September 24, 2001 — September 28, 2001
Coordinators:
- Simone Martini (Università di Bologna, Bologna, Italy)
- Furio Honsell (Sindaco di Udine, Udine, Italy)
- Egon Börger (Università di Pisa, Pisa, Italy)
The goal of the school is to introduce into the leading formally supported design and anlysis methods which are theoretically well founded and at the same time have proved useful for engineering reliable complex software under industrial constraints. The school is organized into modules of 5 lectures, each held by a leading scientist in the field, and covers the Abstract State Machines (ASM) method, the B-method, the Vienna Development Method (VDM), the verification system PVS, Model Checking (MC) and Logical Frameworks (LF).
These methods start providing rigorous specifications and lead by a well documented model refinement process to the formulation of executable code.
The rigorous character of the models allows one to make them executable in various ways and to formulate properties supporting that the code performs as desired.
The formulated properties can be proved to hold using theorem proving or model checking.
The executability of abstract models allows the practitioner to validate high-level models of code prior to coding, namely by running user scenarios and test suites which are defined in terms of the specification. The methods come with different refinement and abstraction notions which allow to split the design, and accordingly to discharge the proof obligations, into pieces which can be dealt with in a modular way.
In this school the participants will learn both the simple theoretical foundation of the above methods and how to apply them successfully in industrial software design. This will be done on real-life examples which derive from industrial applications. The participants will be introduced to the tool environments which support the methods.
The course is addressed to both practitioners and researchers, in particular to system programmers and to postgraduates who want to learn how to develop a complex software system, starting from reliable abstract models, refining them stepwise to executable code and verifying and validating them to possess the desired properties. For attending the school no particular knowledge other than some experience in system development is required, although for each course a short list of useful preliminary readings is provided.