MODELS 2022
Sun 23 - Fri 28 October 2022 Montréal, Canada
Wed 26 Oct 2022 14:37 - 15:00 at A-3502.1 - Validation & Verification I Chair(s): Marsha Chechik

This paper presents experience feedback on how we managed to formally verify properties on semi-formal models of a Life Cycle Management System (LCMS) for smart devices. These devices are typically structured around a System on Chip (SoC), which can provide built-in hardware security. They can offer the possibility to make the deployment of Product-Service Systems (PSSs) to consumers easier, through traceability and collaborative consumption rule enforcement. A PSS is a business model in which products and services are tightly connected. One of the main advantages of such a PSS is that it optimizes product use, with a positive environmental impact. Associating the LCMS with a blockchain-based protocol makes it possible to avoid centralization. Semi-formal UML models of such a LCMS, as well as the properties it must comply with, were created in order to explore its design space and evaluate the outcomes of specific design choices. However, the security of the LCMS implementation must be guaranteed, including protocols and architecture. For that purpose, these models and properties were later improved to be formally verifiable, which ensures the security of their implementation at the expense of added complexity. The verification was carried out using two available software tools: VerifPal for the protocol model, and AnimUML (developed by one of the authors) for the architecture model. This makes the procedure accessible for non-specialists in formal verification. Finally, our feedback on the whole process as well as on VerifPal is also provided.

Wed 26 Oct

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 15:00
Validation & Verification ITechnical Track at A-3502.1
Chair(s): Marsha Chechik University of Toronto
13:30
22m
Talk
Practical Multiverse Debugging through User-defined Reductions: Application to UML ModelsFT
Technical Track
Matthias Pasquier Ertosgener, Ciprian Teodorov ENSTA Bretagne, Frédéric Jouault ERIS Team, ESEO , France, Matthias Brun TRAME Team, ESEO, Luka Le Roux Lab-STICC CNRS UMR 6285, ENSTA Bretagne, Loïc Lagadec Lab-STICC CNRS UMR 6285, ENSTA Bretagne
13:52
22m
Talk
Modelling Program Verification Tools for Software EngineersP&I
Technical Track
Sophie Lathouwers University of Twente, Vadim Zaytsev University of Twente, Netherlands
File Attached
14:15
22m
Talk
Automatic Test Amplification for Executable ModelsFT
Technical Track
Faezeh Khorram IMT Atlantique, Nantes, France, Erwan Bousse Nantes Université, Jean-Marie Mottu Université de Nantes, LS2N, IMT Atlantique, Gerson Sunyé Université de Nantes, LS2N, Pablo Gómez-Abajo Universidad Autónoma de Madrid, Pablo C Canizares Autonomous University of Madrid, Spain, Esther Guerra Universidad Aut�noma de Madrid, Juan de Lara Autonomous University of Madrid
Pre-print
14:37
22m
Talk
Feedback on the Formal Verification of UML Models in an Industrial Context: The Case of a Smart Device Life Cycle Management SystemP&I
Technical Track
Maxime Méré STMicroelectronics, Frédéric Jouault ERIS Team, ESEO , France, Loïc Pallardy STMicroelectronics, Richard Perdriau ESEO