Modelling and Testing Requirements via Executable Abstract State Machines

We describe a method and tools for deriving specification models from requirements, and for validating that the final software product satisfies the requirements. ETF (Eiffel Testing Framework) is a tool for generating code from an abstract grammar specification of user interface actions derived from the requirements document. Mathmodels extends the classical Eiffel contracting notation with the use of mathematical models (based on sets, sequences, relations, functions, bags). The Mathmodels library has immutable queries (for specifications) as well as relatively efficient mutable commands (for describing executable abstract state machines). Models are developed and validated using the industrial strength Eiffel IDE, and the use of these tools thus scale up to the development of large systems in a way that supports the derivation of specification models from requirements, and seamlessness between models and code.

I. Introduction

Model Driven Engineering (MDE) holds the promise of raising the level of abstraction when designing systems by promoting domain specific modelling languages, model transformation techniques and code generation. The use of models above the code level is promoted as a method for handling the complexity of software development. Although there is a large body of research and industrial successes, there are still challenging issues especially with respect to keeping code in sync with the models [1]–[3].