The Control System Specification

Task

The task of team 1 during this phase was the specification of a control system in the application domain building automation using three different formal methods: NRL/SCR, SDL, and statecharts. The problem description given to team 1 had to be analysed especially with regard to consistency.

Goals

The overall goal is to find out which strengths and weaknesses each of the methods reveals with respect to the proposed task and to compare the proposed methods.

Work done

The starting point was an informal problem description for an instance of the control system (Problemdescription Building Automation System (37 KB, english, gzipped postscript)) developed by the project D1 which should be used by all other groups.

The team proceeded in the following way:

Defining a reference model of the world (Constraint Model (23 KB, english, gzipped postscript)) based on a dictionary (Dictionary (138 KB, german, gzipped postscript))
Customizing the problem description to the available resources. (Modified Problemdescription Building Automation System (31 KB, english, gzipped postscript))
Development of three specifications by three subgroups of the team:
- NRL/SCR-Specification (NRL/SCR-Spezifikation des Control-Systems (104 KB, german, gzipped postscript))
- statecharts-Specification consisting of:
  - Corrections of and additions to the problemdescription (Supplement to the Problemdescription (14 KB, english, gzipped postscript))
  - statecharts specification itself (Specification of the control system using statecharts (222 KB, unix-tar-file))
  - List of references from items of the problemdescription to the according charts (References from the problemdescription to the activity- and statecharts (15 KB, english, gzipped postscript))
- SDL-Specification

Work to be done

The current task is to compare the different methods with respect to structure, traceability of decisions, ease of change, and readability.

deiss@informatik.uni-kl.de