Formal Specification of a Safety Critical Pervasive Application for a Nuclear Medicine Department

In case of safety critical pervasive applications classic designing tools can not be applied as they are. As a matter of fact, the behavior of such a kind of applications relies on the location of resources and users and, eventually, on their movements. Unfortunately, classic formal methods take into account neither the concept of location, nor the possibility of movements. This paper presents a set of tools to specify formally requirements for safety critical pervasive applications. In particular, we show how its possible to formalize and constraint the mobility characteristics by combining and extending several formal methods. The paper focuses on a real case study, which consists in a pervasive application for the department of nuclear medicine of a city hospital.