Formal specification of dependable pervasive applications

Wireless and pervasive 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 such applications is affected by the movements and location of users and resources. This paper presents some formal tools that enable designers to specify the software requirements of a pervasive application in an unambiguous and verifiable way. A real safety critical pervasive application for the department of nuclear medicine of a city hospital is also presented as a case study.