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.

With the emergence of connected and autonomous vehicles along with their growing integration of available services, in-vehicle electronic architecture is no longer able to work up to its full potential. Each new service demands processing and computation traditionally handled by a new Electronic Control Unit (ECU). Modern vehicle design tends to be architected around ECU gathered either by feature or by physical location to minimize wiring. Both architectures cannot exploit capabilities of Processing Units (PU) in term of resources such as MIPS and memories.In this paper, we propose a novel approach for the management of these resources by introducing multi-agent systems. This concept consists of integrating IoT-A architectures (implementing agents as close as possible to the hardware), and Avatar architectures (virtualizing the representation of the hardware in high level: Cloud and Edge computing). The result of this work is the emergence of a new EdgeAgent architectural proposal to extend vehicle management and functionalities while considering the environment for vehicles of the future.