The Case Study "Light Control System" of the Dagstuhl Seminar
"Requirements Capture / Documentation / Validation", to be held in June
1999, calls for the application of rigorous methods to the specification,
inspection, and testing of requirements.
To capture the requirements of the case study, we have applied the
This approach serves the following objectives:
- development of a precise description of the system requirements
- customer feedback on a natural language basis
- pattern-based formalisation of requirements
- provision of a starting point for the system development team
- traceability w.r.t. the original problem description
The following documentation is provided (postscript, pdf, or html):
Original problem description (ps,
Documentation of the FOREST-approach
A summary of the main description elements. Recommended reading before
studying any of the documents below.
Original problem description (in FOREST format) as well as the final
FOREST specification (formal and natural language specification) with references
To support traceability, the original problem description is extended by
references to the documentation of the FOREST-approach and vice versa.
Various perspectives of the final FOREST specification of the case
These documents are written in the style of a reference book, and provide
- Developer perspective with references
Formal and natural language specifications including references
within the document. This is the comprehensive document, from
which further perspectives are derived by projection.
- Developer perspective without references
Formal and natural language specifications.
- Customer perspective with signatures
Natural language specification including signatures.
- Customer perspective without signatures
Natural language specification for discussion with the customer.
This document represents the final agreement reached between
customer and analysis team.
Original problem description (in FOREST format)
Documentation of the formal description technique tRTTL
A description of the real time temporal logic used to formalise
Related publications (html)