Abstract
Our approach for modelling interactive systems has been to develop models for the interface and interaction which are lightweight but with an underlying formal semantics. Combined with traditional formal methods to describe functional behaviour, this provides the ability to create a single formal model of interactive systems and consider all parts (functionality, user interface and interaction) with the same rigorous level of formality. The ability to convert the different models we use from one notation to another has given us a set of models which describe an interactive system (or parts of that system) at different levels of abstraction in ways most suitable for the domain but which can be combined into a single model for model checking, theorem proving, etc. There are, however, many benefits to using the individual models for different purposes throughout the development process. In this chapter, we provide examples of this using the nuclear power plant control system as an example.
The original version of the book was revised: For detailed information please see Erratum. The erratum to the book is available at 10.1007/978-3-319-51838_21
An erratum to this chapter can be found at http://dx.doi.org/10.1007/978-3-319-51838-1_21
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
Of course, in order to ensure this is actually true, we must also consider the preservation of these properties in the final implementation, but we will not go into a discussion about refinement here.
- 4.
Note that these two transitions happen at every clock tick since their guards are true, denoted by convention by the absence of any guard.
- 5.
References
Bolton ML, Bass EJ (2010) Formally verifying human-automation interaction as part of a system model: limitations and tradeoffs. Innov Syst Softw Eng A NASA J 6(3):219–231
Bowen J, Reeves S (2006a) Formal models for informal GUI designs. In: 1st international workshop on formal methods for interactive systems, Macau SAR China, 31 October 2006. electronic notes in theoretical computer science, Elsevier, vol 183, pp 57–72
Bowen J, Reeves S (2006b) Formal refinement of informal GUI design artefacts. In: Australian software engineering conference (ASWEC’06). IEEE, pp 221–230
Bowen J, Reeves S (2008) Formal models for user interface design artefacts. Innov Syst Softw Eng 4(2):125–141
Bowen J, Reeves S (2013) Modelling safety properties of interactive medical systems. In: 5th ACM SIGCHI symposium on engineering interactive computing systems, EICS’13. ACM, pp 91–100
Bowen J, Reeves S (2014) A simplified Z semantics for presentation interaction models. In: FM 2014: formal methods—19th international symposium, Singapore, pp 148–162
Courtney A (2003) Functionally modeled user interfaces. In: Interactive systems. design, specification, and verification. 10th international workshop DSV-IS 2003. Lecture notes in computer science, LNCS. Springer, pp 107–123
Derrick J, Boiten E (2014) Refinement in Z and object-Z: foundations and advanced applications. Formal approaches to computing and information technology, 2nd edn. Springer
Dix A, Runciman C (1985) Abstract models of interactive systems. Designing the interface, people and computers, pp 13–22
Duke DJ, Harrison MD (1995) Interaction and task requirements. In: Palanque P, Bastide R (eds) Eurographics workshop on design, specification and verification of interactive system (DSV-IS’95). Springer, pp 54–75
Duke DJ, Faconti GP, Harrison MD, Paternò F (1994) Unifying views of interactors. In: Advanced visual interfaces, pp 143–152
Duke DJ, Fields B, Harrison MD (1999) A case study in the specification and analysis of design alternatives for a user interface. Formal Asp Comput 11(2):107–131
Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231–274
Harrison MD, Dix A (1990) A state model of direct manipulation in interactive systems. In: Formal methods in human-computer interaction. Cambridge University Press, pp 129–151
Henson MC, Deutsch M, Reeves S (2008) Z Logic and its applications. Monographs in theoretical computer science. An EATCS series. Springer, pp 489–596
Hussey A, MacColl I, Carrington D (2000) Assessing usability from formal user-interface designs. Technical report, TR00-15, Software Verification Research Centre, The University of Queensland
ISO, IEC 13568 (2002) Information technology-Z formal specification notation-syntax, type system and semantics. International series in computer science, 1st edn. Prentice-Hall, ISO/IEC
Jacob RJK (1982) Using formal specifications in the design of a human-computer interface. In: 1982 conference on human factors in computing systems. ACM Press, pp 315–321
Limbourg Q, Vanderdonckt J, Michotte B, Bouillon L, López-Jaquero V (2004) UsiXML: a language supporting multi-path development of user interfaces. In: 9th IFIP working conference on engineering for human-computer interaction jointly with 11th international workshop on design, specification, and verification of interactive systems, EHCI-DSVIS’2004, Kluwer Academic Press, pp 200–220
Paternò FM (2001) Task models in interactive software systems. Handbook of software engineering and knowledge engineering
Paternò FM, Sciacchitano MS, Lowgren J (1995) A user interface evaluation mapping physical user actions to task-driven formal specification. In: Design, specification and verification of interactive systems. Springer, pp 155–173
Philipps J, Scholz P (1998) Formal verification and hardware design with statecharts. In: Prospects for hardware foundations, ESPRIT working group 8533. NADA—new hardware design methods, survey chapters, pp 356–389
Puerta A, Eisenstein J (2002) XIML: a universal language for user interfaces. In: Intelligent user interfaces (IUI). ACM Press, San Francisco
Reeve G (2005) A refinement theory for \(\mu \)charts. PhD thesis, The University of Waikato
Reeve G, Reeves S (2000a) \(\mu \)-charts and Z: examples and extensions. In: Proceedings of APSEC 2000. IEEE Computer Society, pp 258–265
Reeve G, Reeves S (2000b) \(\mu \)-charts and Z: hows, whys and wherefores. In: Grieskamp W, Santen T, Stoddart B (eds) Integrated formal methods 2000: proceedings of the 2nd international workshop on integrated formal methods. LNCS, vol 1945. Springer, pp 255–276
Reichart D, Dittmar A, Forbrig P, Wurdel M (2008) Tool support for representing task models, dialog models and user-interface specifications. In: Interactive systems. Design, specification, and verification: 15th international workshop, DSV-IS’08. Springer, Berlin, pp 92–95
Scholz P (1996) An extended version of mini-statecharts. Technical report, TUM-I9628, Technische Univerität München. http://www4.informatik.tu-muenchen.de/reports/TUM-I9628.html
Thimbleby H (1990) Design of interactive systems. In: McDermid JA (ed) The software engineer’s reference book. Butterworth-Heineman, Oxford, Chap, p 57
Thimbleby H (2004) User interface design with matrix algebra. ACM Trans Comput Hum Interact 11(2):181–236
Woodcock J, Davies J (1996) Using Z: specification, refinement and proof. Prentice Hall
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Bowen, J., Reeves, S. (2017). Combining Models for Interactive System Modelling. In: Weyers, B., Bowen, J., Dix, A., Palanque, P. (eds) The Handbook of Formal Methods in Human-Computer Interaction. Human–Computer Interaction Series. Springer, Cham. https://doi.org/10.1007/978-3-319-51838-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-51838-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-51837-4
Online ISBN: 978-3-319-51838-1
eBook Packages: Computer ScienceComputer Science (R0)