is a tool for model-based testing (MBT). The tool receives a Z specification and generates test cases derived from the specification, almost automatically.
The current version just generates abstract test cases (i.e. test cases written in Z), and it does not implement all of the Z language (just the core of it), but it's still useful enough.
Fastest implements the Test Template Framework (TTF) described in:
P. Stocks and D. Carrington, "A framework for specification-based
testing", IEEE Transactions on Software Engineering, vol. 22, no. 11,
pp. 777--793, Nov. 1996.
P. Stocks, "Applying formal methods to software testing", Ph.D.
dissertation, Department of Computer Science, University of Queensland,
H. M. Hörcher and J. Peleska, "Using formal specifications to support
software testing", Software Quality Journal, vol. 4, pp. 309--327, 1995.
Additionally it implements a client/server, implicit invocation architecture, which implies a better performance and the capability of introducing changes in a simple way. Fastest uses the CZT Framework
Fastest works on both Linux
environments. It requires a Java SE Runtime Environment 1.6
or newer. To install the tool, just uncompress and unarchive the file Fastest.tar.gz. The distribution includes a small user manual in English.
# The Fastest User's Guide (pdf)
# Modified version of the Z specification of the steam-boiler control software (pdf)
# Certified elimination theorems (tex)
+ SHA-256 Hash