ESpec Project

Online Tutorial
Contact Information

What is ESpec?

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.


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)


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)

What's New


Home | Downloads | Online Tutorial | Help | Resources | Members | Contact Information
 For problems or questions regarding this Web site contact [ProjectEmail].
Last updated: 2010-06-24.