|
A design
specification is the artifact intermediate between
implemented code and the customer
requirements. ESpec is
a Software Quality Workbench that allows customer requirements and
design specifications to be tested and tested early in the design
cycle leading to early detection of requirement and specification
errors. The core idea behind early testable requirements is that the
problem is described before we search for a solution that can be tested
against the problem description. We also want the problem description to
drive the design.
ESpec allows for the description of testable
requirements via Fit tables
as well as testable design specifications via
contracts written in Eiffel using
mathematical models
following the
single model principle. The tool can mechanically check the
requirements and specifications.
ESpec is a combination of three main components:
-
ES-Fit: A Requirements Testing tool for capturing
and testing customer requirements in the form of HTML tables used
for Validation.
-
ES-Test: A Unit Testing framework for testing
specifications. A combination of Unit tests and Contracts are used
for lightweight Verification.
-
ES-Verify: A translator from Eiffel to Perfect
language used for full Verification.
We focus on Unit Tests and Contracts as testable
specifications and Fit Tables as testable requirements.
Papers
Jonathan
Ostroff, Faraz Ahmadi Torshizi: Testable Requirements and
Specifications, Invited Paper, LNCS 4454, Tests and Proofs (TAP 2007)
Jonathan Ostroff, Chen-Wei Wang, Eric Kerfoot, and Faraz Ahmadi
Torshizi: Automated Model-based Verification of Object-Oriented Code, (VSTTE
2006)
Posters
Jonathan
Ostroff, Chen-Wei Wang, Faraz Ahmadi Torshizi, and Eric Kerfoot:
ES-Verify: A Tool for Automated Model-based Verification of
Object-Oriented Code, Posters & Research Tool Demonstrations, (FM'06) |
