The embedded software of an electricity meter: An experience in using formal methods in an industrial project

This article presents how various formal methods have been involved, first on their own, then coupled, in the different steps of the industrial development of an embedded software for an electricity meter. Synchronized transition systems have been used to conceive and implement some rendezvous mechanisms for the distributed kernel, and the physical link protocol supporting communication between processors. The rate monotonic analysis model has been completed to suit some features of the product; however it appeared too rough to reach a positive issue. So we coupled both (synchronized transition systems and rate monotonic analysis) to achieve a fine analysis of the temporal properties of the system under development. This can be considered a first step towards formal methods engineering.