Home // UBICOMM 2016, The Tenth International Conference on Mobile Ubiquitous Computing, Systems, Services and Technologies // View article

Verifying Scenarios of Proximity-based Federations among Smart Objects through Model Checking

Authors:
Reona Minoda
Yuzuru Tanaka
Shin-ichi Minato

Keywords: ubiquitous computing; catalytic reaction network; formal verification; model checking; smart object.

Abstract:
In this paper, we show a formal approach of verifying ubiquitous computing scenarios. Previously, we proposed "a proximity-based federation model among smart objects", which is intended for liberating ubiquitous computing from stereotyped application scenarios. However, we faced challenges when establishing a verification method for this model. This paper proposes a verification method of this model through model checking. Model checking is one of the most familiar formal verification approaches and it is often used in various fields of industry. Model checking is conducted using a Kripke structure which is a formal state transition model. We introduce a context catalytic reaction network (CCRN) to handle this federation model as a formal state transition model. We also give an algorithm to transform a CCRN into a Kripke structure and we conduct a case study of ubiquitous computing scenario verification, using this algorithm and the model checking.

Pages: 65 to 71

Copyright: Copyright (c) IARIA, 2016

Publication date: October 9, 2016

Published in: conference

ISSN: 2308-4278

ISBN: 978-1-61208-505-0

Location: Venice, Italy

Dates: from October 9, 2016 to October 13, 2016