Computing at Glasgow University
Paper ID: 9244

Towards the Verification of Pervasive Systems
Arapinis,M. Calder,M. Denis,L. Fisher,M. Gray,P. Konur,S. Miller,A. Ritter,E. Ryan,M. Schewe,S. Unsworth,C. Yasmin,R.

Publication Type: Conference Proceedings
Appeared in: Proceedings of Third International Workshop on Formal Methods in Interactive Systems (FMIS 2009). Electronic Communications of the EASST.
Page Numbers :
Publisher: N/A
Year: 2009
ISBN/ISSN: 1863-2122

Pervasive systems, that is roughly speaking systems that can interact with their environment, are increasingly common. In such systems, there are many dimensions to assess: security and reliability, safety and liveness, real-time response, etc. So far modelling and formalizing attempts have been very piecemeal approaches. This paper describes our analysis of a pervasive case study (MATCH, a homecare application) and our proposal for formal (particularly verification) approaches. Our goal is to see to what extent current state of the art formal methods are capable of coping with the verification demand introduced by pervasive systems, and to point out their limitations

Keywords: Pervasive systems, modelling, formalizing, verification

Bibtex entry Endnote XML