Behavioral Modeling, Inference and Validation for Component Specifications

Hosted by Prof. Daniel Jackson (MIT CSAIL).

Abstract

Formal specifications are critical for many software engineering activities like verification and validation. In practice, however, they are often incomplete, inconsistent with the implementation, or even absent. To address specification absence and inconsistency, recent research activity has investigated techniques to automatically extract formal descriptions of the behavior of software artifacts.

This talk addresses a particular instantiation of this problem, focusing on a fully black-box specification synthesis algorithm through dynamic analysis, which takes a class implementation as a source artifact. The extracted specifications are expressed in a novel specification method, called intensional behavior models, which is particularly suitable for data abstractions. Finally, a validation approach is presented, which leverages an adaptation of the small scope hypothesis to check intensional behavior models against algebraic axioms.