Using Z to support the design of interactive safety-critical systems

Mathematically-based specification techniques are increasingly being recruited to support the development of safety-critical systems. Formal notations, such as Z and VDM, provide precise and concise means of representing a design without forcing commitment to implementation strategies 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 once a specification has been refined towards implementation. Usability considerations therefore run the risk of being relegated to an afterthought in the development process. The paper argues that temporal and presentation issues must be represented within formal specifications of interactive systems