Automating reasoning support for design

Formalised design supported by automated reasoning can assist in the management of requirements -a particular problem for large, detailed systems. Designers developing an initial requirements into more detail and then producing a system specification must show not only that all the requirements have been met but also demonstrate how that has been achieved. This is especially important in safety-critical systems where sections of the requirements will be regulations or guidelines. Using real life examples from emergency shutdown systems for drilling rigs1, we show how lightweight (and therefore less time-consuming) formalisation supports validation in an engineering approach to requirements management. We have developed a requirements assistant -an interactive system for formalising and managing information about requirements including guideline requirements. As a design proceeds, relevant requirements are found automatically and checked before being notified to the designer with an accompanying explanation of whether or not they are currently satisfied. Progress in satisfying requirements is monitored automatically and contributing choices are recorded. Such evidence of adherence to guidelines is an assurance of the validity of the design. During any subsequent system modification, reference to this evidence can aid designers by drawing attention to the implications changes will have on maintaining guideline satisfaction. This paper describes how this automated reasoning support works using the demonstrator we have built.