Formal Specification and Verification of Ubiquitous and Pervasive Systems
Antonio Coronato, Giuseppe De Pietro · ACM Transactions on Autonomous and Adaptive Systems · 2011
This article presents a methodology to formally express requirements in safety-critical ubiquitous and pervasive 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 extending several formal methods. The article also discusses some issues concerning both static and dynamic verification.