LITERATE SPECIFICATION - USING DESIGN RATIONALE TO SUPPORT FORMAL METHODS IN THE DEVELOPMENT OF HUMAN-MACHINE INTERFACES

The design of safety-critical user interfaces is typically very differ ent from that of many other applications. Reactor control systems and aircraft cockpits are complex and dynamic, open to input from many dif ferent users and devices. A number of formal notations, including Z an d temporal logic, have been developed to address these problems. They provide precise and concise means of representing a potential design b efore designers incur the expense of implementation. Consequently, gov ernment bodies and commercial organizations have recommended that thes e techniques be used when tendering for their contracts. However, ther e are a number of limitations that restrict the use of mathematical sp ecifications for interface development in large scale projects. In par ticular, formal notations cannot easily be used to coordinate the acti vities of human factors and systems engineering teams. This creates pa rticular difficulties if some group members have only a limited unders tanding of discrete mathematics. A further problem is that the develop ment of a safety-critical application may take many months, or even ye ars, to complete. This creates difficulties because abstract mathemati cal specifications cannot be used easily by new members of a developme nt team to understand past design decisions. To avoid these limitation s I have developed a literate approach to interface specification. Thi s technique uses a formal development language and a semiformal design rationale to support the design of safety-critical user interfaces.