Formal Description and Validation of Graphical User Interfaces

Organisation:	Laboratoire d'Informatique de Grenoble (FRANCE)
Method:	LNT
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Human computer interaction.
Period:	2012-2015
Size:	n/a.
Description:	This work proposes a formal approach to ensure quality of user interfaces in safety-critical systems, by using the formal modeling languages and verification methods available in CADP. The LNT language is used to model formally the graphical user interface behaviour and some aspects of the system core, and the expected properties are expressed as MCL temporal logic formulas. The properties are checked on the formal model using the graph generation and model-checking tools available in CADP. This approach is applied to a system prototype of a nuclear power plant control room in the framework of a collaborative project involving major actors in the French industry of nuclear energy. The system aims at providing a general overview of the plant status, warning the control room operator in case of reactor malfunctions. The formal model comprises the different views of the graphical user interface, the dynamics between views, an abstract model of the reactor, and a model of the user. The checked properties concern the reachability of views. This approach is also extended to check the concept of plasticity, defined as the capacity for a graphical user interface to withstand variations of its context of use, such as the running platform (smartphone, PC, etc.), user (newcomer, expert, etc.), or environment, while preserving usability. Plasticity thus provides users with different versions of a graphical user interface, obtained by systematic transformations. The equivalence checking approach is used to check to which extent different versions of the same graphical user interface have the same interaction capabilities and appearance.
Conclusions:	Several functionalities of CADP are found convenient to check graphical user interfaces: LNT is much more intuitive than LOTOS, and LNT modules are a key for scalability; The rich data types of LNT and the support of value-passing formulas in MCL allow a realistic modeling of graphical user interfaces and of their properties, thus widening the range of verifications that are possible using other approaches; The generation of diagnostics is a great benefit as it provides a precise way to identify concrete problems; And at last, compositional verification is a powerful means to palliate state explosion. This work confirms that formal methods are useful to improve the quality of safety-critical graphical user interfaces.
Publications:	[Oliveira-DupuyChessa-Calvary-14] Raquel Oliveira, Sophie Dupuy-Chessa, and Gaelle Calvary. "Formal verification of UI using the power of a recent tool suite". In Proceedings of ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'14, pages 235-240. ACM, 2014. Available on-line at: http://dl.acm.org/citation.cfm?doid=2607023.2610280 or from the CADP Web site in PDF or PostScript [Oliveira-DupuyChessa-Calvary-15-a] Raquel Oliveira, Sophie Dupuy-Chessa, and Gaelle Calvary. "Equivalence checking for comparing user interfaces". In Proceedings of ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'15, pages 266-275. ACM, 2015. Available on-line at: http://dl.acm.org/citation.cfm?doid=2774225.2774844 or from the CADP Web site in PDF or PostScript [Oliveira-DupuyChessa-Calvary-15-b] Raquel Oliveira, Sophie Dupuy-Chessa, and Gaelle Calvary. "Plasticity of user interfaces: formal verification of consistency". In Proceedings of ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'15, pages 260-265. ACM, 2015. Available on-line at: http://dl.acm.org/citation.cfm?doid=2774225.2775078 or from the CADP Web site in PDF or PostScript [Oliveira-DupuyChessa-Calvary-15-c] Raquel Oliveira, Sophie Dupuy-Chessa, and Gaelle Calvary. "Verification of Plastic Interactive Systems", Journal of Interactive Media (i-com) 14(3):192-204, 2015. Available on-line at: http://www.degruyter.com/view/j/icom.2015.14.issue-3/icom-2015-0036/icom-2015-0036.xml or from the CADP Web site in PDF or PostScript [Oliveira-DupuyChessa-Calvary-Dadolle-16] Raquel Oliveira, Sophie Dupuy-Chessa, Gaelle Calvary, and Danielle Dadolle. "Using Formal Models to Cross Check an Implementation". In Proceedings of ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'16, pages 126-137. ACM, 2016. Available on-line at: http://dl.acm.org/citation.cfm?id=2933257 or from the CADP Web site in PDF or PostScript
Contact:	Raquel Oliveira Laboratoire d'Informatique de Grenoble Bâtiment IM2AG B 41, rue des mathématiques 38400 Domaine Universitaire de Saint-Martin-d'Hères FRANCE Email: Raquel.Oliveira@imag.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page