publications([{ "lang": "en", "publisher": "ACM", "doi": "https://doi.org/10.1145/2933242.2933257", "title": "Using formal models to cross check an implementation", "abstract": "Interactive systems are developed according to requirements, which may be, for instance, documentation, prototypes, diagrams, etc. The informal nature of system requirements may be a source of problems: it may be the case that a system does not implement the requirements as expected, thus, a way to validate whether an implementation follows the requirements is needed. We propose a novel approach to validating a system using formal models of the system. In this approach, a set of traces generated from the execution of the real interactive system is searched over the state space of the formal model. The scalability of the approach is demonstrated by an application to an industrial system in the nuclear plant domain. The combination of trace analysis and formal methods provides feedback that can bring improvements to both the real interactive system and the formal model.", "authors": { "1": { "first_name": "Raquel", "last_name": "Oliveira" }, "2": { "first_name": "Sophie", "last_name": "Dupuy-Chessa" }, "3": { "first_name": "Gaëlle", "last_name": "Calvary" }, "4": { "first_name": "Danièle", "last_name": "Dadolle" } }, "year": 2016, "uri": "http://iihm.imag.fr/publication/ODC+16a/", "pages": "126-137", "bibtype": "inproceedings", "id": 776, "abbr": "ODC+16a", "address": "Brussels, Belgium", "date": "2016-06-27", "document": "http://iihm.imag.fr/publs/2016/oliveiraEICS16.pdf", "type": "Conférences internationales de large diffusion avec comité de lecture sur texte complet", "booktitle": "Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing System EICS 2016", "type_publi": "icolcomlec" }, { "lang": "en", "publisher": "ACM", "doi": "http://doi.acm.org/10.1145/2774225.2774844", "title": "Equivalence Checking for Comparing User Interfaces", "abstract": "Plastic User Interfaces (UIs) have the capacity to adapt to changes in their context of use while preserving usability. This exposes users to different versions of UIs that can diverge from each other at several levels, which may cause loss of consistency. This raises the question of similarity between UIs. This paper proposes an approach to comparing UIs by measuring to what extent UIs have the same interaction capabilities and appearance. We use the equivalence checking formal method. The approach verifies whether two UI models are equivalent or not. When they are not equivalent, the UI divergences are listed, thus providing the possibility of leaving them out of the analysis. In this case, the two UIs are said equivalent modulo such divergences. Furthermore, the approach shows that one UI can contain at least all interaction capabilities of another. We apply the approach to a case study in the nuclear power plant domain in which several UI versions are analyzed, and the equivalence and inclusion relations are demonstrated.", "authors": { "1": { "first_name": "Raquel", "last_name": "Oliveira" }, "2": { "first_name": "Sophie", "last_name": "Dupuy-Chessa" }, "3": { "first_name": "Gaëlle", "last_name": "Calvary" } }, "year": 2015, "uri": "http://iihm.imag.fr/publication/ODC15a/", "pages": "266-275", "bibtype": "inproceedings", "id": 721, "editor": "Jürgen Ziegler", "address": "Duisburg, Germany", "date": "2015-06-23", "document": "http://iihm.imag.fr/publs/2015/oliveiraEICS15.pdf", "type": "Conférences internationales de large diffusion avec comité de lecture sur texte complet", "booktitle": "Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2015)", "type_publi": "icolcomlec", "abbr": "ODC15a" }, { "lang": "en", "publisher": "De Gruyter publication", "type_publi": "irevcomlec", "title": "Verification of Plastic Interactive Systems", "bibtype": "article", "journal": "Journal of Interactive Media (i-com)", "year": 2015, "uri": "http://iihm.imag.fr/publication/ODC15c/", "pages": "192-204", "volume": 3, "id": 753, "abbr": "ODC15c", "authors": { "1": { "first_name": "Raquel", "last_name": "Oliveira" }, "2": { "first_name": "Sophie", "last_name": "Dupuy-Chessa" }, "3": { "first_name": "Gaëlle", "last_name": "Calvary" } }, "date": "2015-10-15", "document": "http://iihm.imag.fr/publs/2015/icom-2015-0036.pdf", "type": "Revues internationales avec comité de lecture", "abstract": "Interactive systems have largely evolved over the past years. Nowadays, different users can interact with systems on different devices and in different environments. The user interfaces (UIs) are expected to cope with such variety. Plastic UIs have the capacity to adapt to changes in their context of use while preserving usability. Such capability enhances UIs, however, it adds complexity on them. We propose an approach to verifying interactive systems considering this adaptation capability of the UIs. The approach applies two formal techniques: model checking, to the verification of properties over the system model, and equivalence checking, to compare different versions of a UI, thereby identifying different levels of UI equivalence. We apply the approach to a case study in the nuclear power plant domain in which several UI are analyzed, properties are verified, and the level of equivalence between them is demonstrated." }, { "lang": "en", "type_publi": "these", "doi": "https://tel.archives-ouvertes.fr/tel-01253619", "title": "Formal Specification and Verification of Interactive Systems with Plasticity: Applications to Nuclear-Plant Supervision", "url": "https://tel.archives-ouvertes.fr/tel-01253619", "abstract": "Plasticity provides users with different versions of a UI. Although it enhances UI capabilities, plasticity adds complexity to the development of user interfaces: the consistency between multiple versions of a given UI should be ensured. This complexity is further increased when it comes to UIs of safety-critical systems. Safety-critical systems are systems in which a failure has severe consequences. Given the large number of possible versions of a UI, it is time-consuming and error prone to check these requirements by hand. Some automation must be provided to verify plasticity. Formal verification provides a rigorous way to perform verification, which is suitable for safety-critical systems. Our main contribution is an approach to verifying safety critical interactive systems provided with plastic UIs using formal methods. Using a powerful tool support, our approach permits: (1) the verification of sets of properties over a model of the system. Using model checking, our approach permits the verification of properties over the system formal specification. Usability properties verify whether the system follows ergonomic properties to ensure a good usability. Validity properties verify whether the system follows the requirements that specify its expected behavior; (2) the comparison of different versions of UIs. Using equivalence checking, our approach verifies to which extent UIs present the same interaction capabilities and appearance. We can show whether two UI models are equivalent or not. When they are not equivalent, the UI divergences are listed, thus providing the possibility of leaving them out of the analysis. We also present three industrial case studies in the nuclear power plant domain to which the approach was applied.", "year": 2015, "uri": "http://iihm.imag.fr/publication/O15a/", "id": 754, "bibtype": "phdthesis", "abbr": "O15a", "authors": { "1": { "first_name": "Raquel", "last_name": "Oliveira" } }, "date": "2015-12-03", "type": "Thèses et habilitations", "pages": "250" }, { "lang": "en", "publisher": "ACM", "doi": "http://doi.acm.org/10.1145/2774225.2775078", "title": "Plasticity of user interfaces: formal verification of consistency", "bibtype": "unpublished", "abstract": "Plastic user interfaces have the capacity of adapting themselves to their context of use while preserving usability. This property gives rise to several versions of the same UI. This paper addresses the problem of verifying UI adaptation by means of formal methods. It proposes three approaches, all of them supported by the CADP toolbox and LNT formal language. The first approach permits the reasoning over the adaptation output, i.e. the UI versions: some properties are verified over the UI models thanks to model checking. The second solution proposes to verify the plasticity engine. The last approach compares UI versions thanks to equivalence checking. These approaches are discussed and compared on an example of a system in the nuclear power plant domain.", "authors": { "1": { "first_name": "Raquel", "last_name": "Oliveira" }, "2": { "first_name": "Sophie", "last_name": "Dupuy-Chessa" }, "3": { "first_name": "Gaëlle", "last_name": "Calvary" } }, "year": 2015, "uri": "http://iihm.imag.fr/publication/ODC15b/", "pages": "260-265", "note": "Late Breaking Results", "id": 741, "editor": "Jürgen Ziegler", "address": "Duisburg, Germany", "date": "2015-06-23", "document": "http://iihm.imag.fr/publs/2015/oliveiraEICS15short.pdf", "type": "Autres publications", "booktitle": "Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2015)", "type_publi": "autre", "abbr": "ODC15b" }, { "lang": "en", "publisher": "ACM", "doi": "https://doi.org/10.1145/2933242.2933257", "title": "Formal Verification of UI Using the Power of a Recent Tool Suite", "bibtype": "unpublished", "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.\r\n", "authors": { "1": { "first_name": "Raquel", "last_name": "Oliveira" }, "2": { "first_name": "Sophie", "last_name": "Dupuy-Chessa" }, "3": { "first_name": "Gaëlle", "last_name": "Calvary" } }, "year": 2014, "uri": "http://iihm.imag.fr/publication/ODC14a/", "pages": "235-240", "note": "Late Breaking Results", "id": 686, "editor": "Fabio Paterno", "address": "Rome, Italy", "date": "2014-06-03", "document": "http://iihm.imag.fr/publs/2014/oliveiraEICS14.pdf", "type": "Autres publications", "booktitle": "Proceedings of the 2014 ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2014)", "type_publi": "autre", "abbr": "ODC14a" }]);