Using algebraic specifications in software testing: A case study on the software of an automatic subway
Abstract This article reports an experiment using a formal specification of a piece of critical software as a basis to derive test data sets. The software was the onboard part of the driving system of an automatic subway. It was formally specified using algebraic techniques. Then, two modules of the specification were used as input to the LOFT test selection tool, which is based on narrowing and some other aspects of advanced logic programming. The experience established that the approach is practicable for industrial examples.