Automated Specification Extraction and Analysis with Specstractor

摘要

This paper presents Specstractor, a tool chain for the extraction and analysis of system specifications in the form of collections of invariants. Such invariants convey valuable information about the behavior of a software system and are also useful in identifying missing or defective parts of existing specifications. Using data-mining techniques, Specstractor derives likely invariants from test data that it automatically generates from the system under analysis, using an iterative approach to refine the set of proposed invariants and eliminate false positives. The paper describes the Spectstractor technology and evaluates it on real-world artifacts from automotive-control and medical-device applications.