USING Z TO SUPPORT THE DESIGN OF INTERACTIVE SAFETY-CRITICAL SYSTEMS

Mathematically-based specification techniques are increasingly being r ecruited to support the development of safety-critical systems. Formal notations, such as Z and VDM, provide precise and concise means of re presenting a design without forcing commitment to implementation strat egies during the early stages of development. Unfortunately, interface requirements are not normally considered within formal specifications . This threatens user-centred design. A prime objective in the use of formal methods is to minimise the modifications that are necessary onc e a specification has been refined towards implementation. Usability c onsiderations therefore run the risk of being relegated to an aftertho ught in the development process. The paper argues that temporal and pr esentation issues must be represented within formal specifications of interactive systems.