Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages

Reona MINODA; Shin-ichi MINATO

doi:10.1587/transinf.2016FOP0009

Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages

Reona MINODA, Shin-ichi MINATO

Full Text Views

0

Share
Cite this

Summary :

This paper proposes a formal approach of verifying ubiquitous computing application scenarios. Ubiquitous computing application scenarios assume that there are a lot of devices and physical things with computation and communication capabilities, which are called smart objects, and these are interacted with each other. Each of these interactions among smart objects is called “federation”, and these federations form a ubiquitous computing application scenario. Previously, Yuzuru Tanaka proposed “a proximity-based federation model among smart objects”, which is intended for liberating ubiquitous computing from stereotyped application scenarios. However, there are still challenges to establish the verification method of this model. This paper proposes a verification method of this model through model checking. Model checking is one of the most popular formal verification approach 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. Finally, we discuss the advantages of our formal approach by showing the difficulties of our target problem experimentally.

Publication: IEICE TRANSACTIONS on Information Vol.E100-D No.6 pp.1172-1181

Publication Date: 2017/06/01

Publicized: 2017/03/07

Online ISSN: 1745-1361

DOI: 10.1587/transinf.2016FOP0009

Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)

Category: Formal techniques

Authors

Reona MINODA
Hokkaido University
Shin-ichi MINATO
Hokkaido University

Keyword

ubiquitous computing, catalytic reaction network, formal verification, model checking, smart object

Cite this

Copy

Reona MINODA, Shin-ichi MINATO, "Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages" in IEICE TRANSACTIONS on Information, vol. E100-D, no. 6, pp. 1172-1181, June 2017, doi: 10.1587/transinf.2016FOP0009.
Abstract: This paper proposes a formal approach of verifying ubiquitous computing application scenarios. Ubiquitous computing application scenarios assume that there are a lot of devices and physical things with computation and communication capabilities, which are called smart objects, and these are interacted with each other. Each of these interactions among smart objects is called “federation”, and these federations form a ubiquitous computing application scenario. Previously, Yuzuru Tanaka proposed “a proximity-based federation model among smart objects”, which is intended for liberating ubiquitous computing from stereotyped application scenarios. However, there are still challenges to establish the verification method of this model. This paper proposes a verification method of this model through model checking. Model checking is one of the most popular formal verification approach 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. Finally, we discuss the advantages of our formal approach by showing the difficulties of our target problem experimentally.
URL: https://globals.ieice.org/en_transactions/information/10.1587/transinf.2016FOP0009/_p

Copy

@ARTICLE{e100-d_6_1172,
author={Reona MINODA, Shin-ichi MINATO, },
journal={IEICE TRANSACTIONS on Information},
title={Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages},
year={2017},
volume={E100-D},
number={6},
pages={1172-1181},
abstract={This paper proposes a formal approach of verifying ubiquitous computing application scenarios. Ubiquitous computing application scenarios assume that there are a lot of devices and physical things with computation and communication capabilities, which are called smart objects, and these are interacted with each other. Each of these interactions among smart objects is called “federation”, and these federations form a ubiquitous computing application scenario. Previously, Yuzuru Tanaka proposed “a proximity-based federation model among smart objects”, which is intended for liberating ubiquitous computing from stereotyped application scenarios. However, there are still challenges to establish the verification method of this model. This paper proposes a verification method of this model through model checking. Model checking is one of the most popular formal verification approach 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. Finally, we discuss the advantages of our formal approach by showing the difficulties of our target problem experimentally.},
keywords={},
doi={10.1587/transinf.2016FOP0009},
ISSN={1745-1361},
month={June},}

Copy

TY - JOUR
TI - Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages
T2 - IEICE TRANSACTIONS on Information
SP - 1172
EP - 1181
AU - Reona MINODA
AU - Shin-ichi MINATO
PY - 2017
DO - 10.1587/transinf.2016FOP0009
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E100-D
IS - 6
JA - IEICE TRANSACTIONS on Information
Y1 - June 2017
AB - This paper proposes a formal approach of verifying ubiquitous computing application scenarios. Ubiquitous computing application scenarios assume that there are a lot of devices and physical things with computation and communication capabilities, which are called smart objects, and these are interacted with each other. Each of these interactions among smart objects is called “federation”, and these federations form a ubiquitous computing application scenario. Previously, Yuzuru Tanaka proposed “a proximity-based federation model among smart objects”, which is intended for liberating ubiquitous computing from stereotyped application scenarios. However, there are still challenges to establish the verification method of this model. This paper proposes a verification method of this model through model checking. Model checking is one of the most popular formal verification approach 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. Finally, we discuss the advantages of our formal approach by showing the difficulties of our target problem experimentally.
ER -