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

Minoda Reona; Minato Shin-ichi

タイトル	en Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages
作成者	en Minoda, Reona en Minato, Shin-ichi NRID 1000010374612
アクセス権	open access
権利情報	en Copyright ©2017 The Institute of Electronics, Information and Communication Engineers
主題	Other en ubiquitous computing Other en catalytic reaction network Other en formal verification Other en model checking Other en smart object NDC 549
内容注記	Abstract en 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.
出版者	ja 電子情報通信学会 en The Institute of Electronics, Information and Communication Engineers / IEICE
日付	Issued2017-06
言語	eng
資源タイプ	journal article
出版タイプ	VoR
資源識別子	HDL http://hdl.handle.net/2115/67036
関連	URI https://search.ieice.org/ isIdenticalTo DOI https://doi.org/10.1587/transinf.2016FOP0009
収録誌情報	PISSN 1745-1361 en IEICE transactions on information and systems 巻E100 号6 開始ページ1172 終了ページ1181
ファイル	fulltext E100.D_2016FOP0009.pdf 1.53 MB (application/pdf) Issued2017-06
コンテンツ更新日時	2023-07-26