Using Z to support the design of interactive safety-critical systems
- 1 January 1995
- journal article
- Published by Institution of Engineering and Technology (IET) in Software Engineering Journal
- Vol. 10 (2) , 49-60
- https://doi.org/10.1049/sej.1995.0008
Abstract
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.Keywords
This publication has 5 references indexed in Scilit:
- The ‘problem’ with automation: inappropriate feedback and interaction, not ‘over-automation’Published by Oxford University Press (OUP) ,1990
- Temporal decision making in complex environmentsPublished by Oxford University Press (OUP) ,1990
- LCD-reification: a formal method for developing Prolog programsPublished by Association for Computing Machinery (ACM) ,1989
- Substitution Error Potential in Nuclear Power Plant Control RoomsProceedings of the Human Factors Society Annual Meeting, 1981
- Verification of Concurrent Programs. Part I. The Temporal Framework,Published by Defense Technical Information Center (DTIC) ,1981