Abstract:
Proving software systems correct is a difficult task, and automated
validation, e.g., model checking, has been proposed as a savior.
To achieve success, however, a software system must first be abstracted
to a simpler, manageably sized model before automated validation proceeds.
This talk presents the basics of abstracting software: crucial notions, such as homomorphisms and simulations, are defined and applied to simple examples. Unfortunately, the abstraction process inherently limits the properties one can validate, so safe subsets of temporal logic are presented alongside the abstraction techniques.
The dual to abstraction is refinement---the expansion/elaboration of a system's design into its implementation. The same issues that accompany validation techniques for abstraction also haunt methodologies for stepwise refinement, and the talk illustrates this duality in its examples.
Finally, Larsen's modal transition systems are proposed as a unifying framework for both validation-by-abstraction and implementation-by-refinement.