Extending the Test Template Framework to Deal with Axiomatic Descriptions, Quantifiers and Set Comprehensions

Abstract

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{CristiaF12,
  author       = {Maximiliano Cristi{\'{a}} and
                  Claudia S. Frydman},
  editor       = {John Derrick and
                  John S. Fitzgerald and
                  Stefania Gnesi and
                  Sarfraz Khurshid and
                  Michael Leuschel and
                  Steve Reeves and
                  Elvinia Riccobene},
  title        = {Extending the Test Template Framework to Deal with Axiomatic Descriptions,
                  Quantifiers and Set Comprehensions},
  booktitle    = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
                  Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7316},
  pages        = {280--293},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-30885-7\_20},
  doi          = {10.1007/978-3-642-30885-7\_20},
  timestamp    = {Thu, 14 Oct 2021 10:31:49 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/CristiaF12.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}