Formal specification of wireless and pervasive healthcare applications

Wireless and pervasive healthcare applications typically present critical requirements from the point of view of functional correctness, reliability, availability, security, and safety. In contrast to the case of classic safety critical applications, the behavior of wireless and pervasive applications is affected by the movements and location of users and resources. This article presents a methodology to formally express requirements in safety critical wireless and pervasive healthcare applications in order to achieve a higher degree of dependability. In particular, it will be shown how it is possible to formalize and constrict mobility characteristics by combining, and in some cases extending, several formal methods. The article also describes a rigorous specification process. Finally, it concludes with a case study of a real safety critical pervasive healthcare application that is going to be deployed in a city hospital.