Light Control

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 FOREST-approach. 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, pdf)

• Documentation of the FOREST-approach (ps, html)
  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 (ps, html)
  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 study
  Authors: Martin Kronenburg, Christian Peper
  

  These documents are written in the style of a reference book, and provide navigation support.

  • Developer perspective with references (ps, html)
    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 (ps, html)
    Formal and natural language specifications.
  • Customer perspective with signatures (ps, html)
    Natural language specification including signatures.
  • Customer perspective without signatures (ps, html)
    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) (ps, html)
  

• Documentation of the formal description technique tRTTL (html)
  A description of the real time temporal logic used to formalise properties.

• Related publications (html)