Feedback on the formal verification of UML models in an industrial context: the case of a smart device life cycle management system.

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 informal properties it must comply with, were defined 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.