Algebraic specifications and sequencing: A defect detection method
Kurt M. Olender, James M. Bieman · Software Testing Verification and Reliability · 1995
Abstract One class of program defects results from illegal sequences of otherwise legal operations in software implementations. Explicit statement of sequencing constraints, however, is not a common activity when specifying software even when using formal specification methods. This paper shows that constraints on program execution sequences can be derived directly from algebraic specifications. Results include heuristic methods for generating sequencing constraints and a generalization of these methods into automatable rules. The heuristics can be integrated into a specification methodology such as Larch. Engineers can use the generated sequencing constraints to detect sequencing defects in software even before dynamic testing begins. The method can be used to increase the reliability of software that is specified using algebraic methods.