Extending the Test Template Framework to deal with axiomatic descriptions, quantifiers and set comprehensions

CRISTIÁ, MAXIMILIANO; FRYDMAN, CLAUDIA

Pisa

Conferencia; ABZ 2012; 2012

The Test Template Framework (TTF) is a method for model-based testing (MBT) from Z specifications. Although the TTF covers many features of the Z notation, it does not explain how to deal with axiomatic descriptions, quantifiers and set comprehensions. In this paper we extend the TTF so it can process specifications including these features. The techniques presented here may be useful for other MBT methods for the Z notation or for other notations such as Alloy and B, since they use similar mathematical theories.