Raquel Oliveira
Sophie Dupuy-Chessa
ABSTRACT
This paper presents an approach to verify the quality of user interfaces in the context of a critical system for nuclear power plants. The technique uses formal methods to perform verification. The user interfaces are described by means of a formal language called LNT and ergonomic properties are formally defined using temporal logics written in MCL language. Our approach moves towards the powerfulness of formal verification of user interfaces, thanks to recent tools to support the process.
- Abowd, G. D., Coutaz, J., and Nigay, L. Structuring the space of interactive system properties. In Proceedings of the IFIP TC2/WG2.7 Working Conference on Engineering for Human-Computer Interaction, North-Holland Publishing Co. (Amsterdam, The Netherlands, The Netherlands, 1992), 113--129. Google Scholar
Digital Library
- Bastien, J. C., and Scapin, D. L. Ergonomic criteria for the evaluation of human-computer interfaces. Tech. Rep. RT-0156, INRIA, June 1993.Google Scholar
- Chériaux, F., Galara, D., and Viel, M. Interfaces for nuclear power plant overview. In 8th International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies 2012 (NPIC & HMIT 2012): Enabling the Future of Nuclear Energy, NPIC & HMIT 2012, Curran Associates, Inc. (2012), 1002--1012.Google Scholar
- Coutaz, J. Pac, an object oriented model for dialog design. In Proceedings Interact, vol. 87 (1987), 431--436.Google Scholar
- Degani, A., Heymann, M., Meyer, G., and Shafto, M. Some formal aspects of human-automation interaction. NASA Technical Memorandum 209600 (2000).Google Scholar
- Galitz, W. O. The essential guide to user interface design: an introduction to GUI design principles and techniques. John Wiley & Sons, 2007. Google ScholarDigital Library
- Garavel, H., Lang, F., Mateescu, R., and Serwe, W. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. International Journal on Software Tools for Technology Transfer 15, 2 (2013), 89--107.Google ScholarDigital Library
- Markopoulos, P., Johnson, P., and Rowson, J. Formal architectural abstractions for interactive software. Int. J. Hum.-Comput. Stud. 49, 5 (Nov. 1998), 675--715. Google ScholarDigital Library
- Masci, P., Ayoub, A., Curzon, P., Harrison, M. D., Lee, I., and Thimbleby, H. Verification of interactive software for medical devices: Pca infusion pumps and fda regulation as an example. In Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS '13, ACM (New York, NY, USA, 2013), 81--90. Google ScholarDigital Library
- Mateescu, R., and Thivolle, D. A Model Checking Language for Concurrent Value-Passing Systems. In FM 2008, J. Cuellar and T. Maibaum, Eds., vol. 5014 of Lecture Notes in Computer Science, Springer Verlag (Turku, Finlande, 2008), 148--164. Google ScholarDigital Library
- Miller, S. P., Whalen, M. W., and Cofer, D. D. Software model checking takes off. Commun. ACM 53, 2 (Feb. 2010), 58--64. Google ScholarDigital Library
- Navarre, D., Palanque, P. A., Ladry, J.-F., and Barboni, E. Icos: A model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability. ACM Trans. Comput.-Hum. Interact. 16, 4 (2009). Google ScholarDigital Library
- Nielsen, J., and Molich, R. Heuristic evaluation of user interfaces. In Proceedings of the SIGCHI conference on Human factors in computing systems, ACM (1990), 249--256. Google ScholarDigital Library
- Paternó, F. Formal reasoning about dialogue properties with automatic support. Interacting with Computers 9, 2 (1997), 173--196.Google ScholarCross Ref
- Paternó, F., and Santoro, C. Support for reasoning about interactive systems through human-computer interaction designers' representations. Comput. J. 46, 4 (2003), 340--357.Google ScholarCross Ref
- Sighireanu, M., Chaudet, C., Garavel, H., Herbert, M., Mateescu, R., and Vivien, B. Lotos nt user manual. INRIA, june (2004).Google Scholar
- Sousa, M., Campos, J., Alves, M., and Harrison, M. Formal verification of safety-critical user interfaces: a space system case study. In Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium, AAAI Press, AAAI Press (Stanford, 26 March 2014), 62--67.Google Scholar
- Vanderdonckt, J. Guide ergonomique des interfaces homme-machine. No. 13 in Collection "Travaux de l'Institut d'Informatique". Presses Universitaires, Namur, 1994.Google Scholar
Index Terms
- Formal verification of UI using the power of a recent tool suite
Recommendations
Formal verification of SystemCFLspecifications using SPIN
MINO'06: Proceedings of the 5th WSEAS international conference on Microelectronics, nanoelectronics, optoelectronicsThe formal language SystemCFL is the formalization of SystemC. The language semantics of SystemCFL was formally defined in a standard structured operational semantics (SOS) style. For verification purposes, in this paper, we present an approach to use ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Formal specification at model-level of model-driven engineering using modelling techniques
Nowadays Model-Driven Engineering (MDE) is gaining more popularity due to high-level development leading to a faster generation of executable code, which reduces manual intervention. Verification is crucial at different levels of model-based development. ...
Comments