Plasticity of User Interfaces: Formal Verification of Consistency

International audiencePlastic user interfaces have the capacity of adapting themselves to their context of use while preserving usability. Thisproperty gives rise to several versions of the same UI. Thispaper addresses the problem of verifying UI adaptation bymeans of formal methods. It proposes three approaches, allof them supported by the CADP toolbox and LNT formallanguage. The first approach permits the reasoning over theadaptation output, i.e. the UI versions: some properties areverified over the UI models thanks to model checking. Thesecond solution proposes to verify the plasticity engine. Thelast approach compares UI versions thanks to equivalencechecking. These approaches are discussed and compared onan example of a system in the nuclear power plant domain