Finite-state verification (FSV) techniques are intended for proving properties of software systems. Although significant progress has been made in the last decade automating FSV techniques, the adoption of these techniques by software developers is low. The Specification Pattern System (SPS) is intended to assist users in creating such specifications. It identifies common specification patterns and indicates how to translate the patterns into a variety of different specification languages. However, the patterns in the SPS are defined informally and their translations are not verified. This work discusses the informal nature of these definitions, proposes a formalization for them and provides formal proofs for the translation of patterns to Linear Temporal Logic.
Read
