Article Title: Modeling and Verification of Mobile and Communication Behavior for IoT Devices
All Authors: Jingyu Liu, Xuansong Li, Zhifei Chen, Haibo Ye, Wei Song
First Institution: Nanjing University of Science and Technology, School of Computer Science and Engineering
Publication Time: 2024, 35(11): 4993-5015
The application range of IoT devices is continuously expanding. Model checking is an effective means to enhance the reliability and security of such devices, but commonly used model checking methods cannot effectively characterize the common cross-space mobility and communication behaviors of these devices. Therefore, we propose a modeling and verification method for the mobility and communication behavior of IoT devices to achieve verification of the spatiotemporal properties of such devices. By incorporating pull and push actions and global communication mechanisms into ambient calculus, we propose the Global Communication Mobile Environment Calculus (ACGC) and provide the model checking algorithm for ACGC against ambient logic; based on this, we introduce a mobile communication modeling language (MLMC) to describe the mobility and communication behavior of IoT devices and provide a method to convert MLMC descriptions into ACGC models; furthermore, we implement the model checking tool ACGCCk to verify whether the properties of IoT devices are satisfied and accelerate the detection speed through some optimizations; finally, we demonstrate the effectiveness of the proposed method through case studies and experimental analysis.
1 Method Overview
In order to characterize the passive mobility of devices and users and their cross-space communication from the level of atomic operations, we introduce the push and pull actions and the global communication mechanism into AC, proposing the Global Communication Mobile Environment Calculus ACGC. ACGC is a relatively abstract process algebra that is difficult for users to use directly; therefore, this paper proposes MLMC to assist users in modeling the behavior of IoT devices. MLMC can clearly describe the mobility and communication behavior of IoT devices while supporting the conversion of its model to ACGC models.
First, construct an ambient corresponding to each entity based on the entity declaration. The name of the ambient is the same as that of the entity, and its internal ACGC process is initially set to an empty process. Then, define the action rules to add ACGC processes representing the behaviors of the entity into the ambient representing the entity. Each process of each entity must be converted into a corresponding ACGC process. The method to convert a process into an ACGC process is: according toTable 1 the conversion rules, convert each statement in the process into the corresponding capability or communication prefix in sequence and concatenate them, then add them before an empty process. If the action rules of an entity consist of multiple parallel processes, then the ACGC processes converted from these processes are also added to the ambient representing the entity in parallel. Finally, nest the ambients representing the entities according to the initial location definitions. For a given entity, move all ambients of the entities that are nested one layer deep in the initial location definitions into the ambient of that entity, and the ACGC processes representing its behavior in that entity’s ambient run in parallel with the ambient of the entities nested one layer deep. For those entities that are not nested by any other entities, their ambients are run in parallel and merged into one ACGC process.
Table 1 Conversion Rules from MLMC Statements to Capabilities or Communication Prefixes
This paper designed and implemented the model checking tool ACGCCk for ACGC against AL. Figure 1 shows the basic structure of ACGCCk. Input an ACGC process converted from MLMC and an AL formula, the process lexical analysis module and the formula lexical analysis module convert the strings representing processes and formulas into token sequences, then the process syntax analysis module and the formula syntax analysis module parse the token sequences of processes and formulas respectively and construct corresponding process trees and formula trees, finally the recursive detection module recursively calls the model checking algorithm on the process tree and formula tree and provides the detection results.
The process tree and formula tree are tree data structures representing ACGC processes and AL formulas. This paper expands and improves upon the AC process tree structure representation method to design process trees suitable for representing ACGC processes and formula trees for AL formulas. Figure 2 shows the structure of the process tree and formula tree. In the process tree, all nodes except the root node RootNode represent a capability, communication primitive, or ambient in the process; in the formula tree, each node represents an operator in the formula. Total order: All honest nodes confirm (submit) the same block in the same order.
Figure 2 Structure of Process Tree and Formula Tree
In this scenario, we are mainly concerned with whether two properties can be satisfied.
Property 1: Food1 and Food2 are ultimately delivered to R206 and R702, respectively.
Figure 5 Entity Declaration of Robot Meal Delivery Scenario
Figure 7 Action Rule Definition of Robot Meal Delivery Scenario
Question 1. How does the structure scale of the process affect the time overhead of detection.
For Question 1, this paper mainly measures the structural scale of the process by the number of ambients contained in it. In combination with actual situations, this paper constructs several processes composed of nested and parallel ambients, with the nesting depth of these processes being 3, and the number of ambients ranging from 100 to 1000, which are non-reducible; for each process, efforts are made to ensure that the internal nesting relationships are evenly distributed (i.e., the number of child ambients nested one layer deep in most parent ambients is similar).
Figure 8 Performance Evaluation Experimental Results of ACGCCk
3 Conclusion and Outlook
To address the issue that some existing model checking methods cannot be effectively applied to the formal verification of IoT devices with mobility and communication behaviors, this paper integrates push and pull actions and global communication mechanisms based on AC, proposes the Global Communication Mobile Environment Calculus ACGC, and provides the model checking algorithm for ACGC against AL, proposes the mobile communication modeling language MLMC and provides the conversion method from MLMC models to ACGC models, implements the model checking tool ACGCCk, and demonstrates through experiments that ACGCCk has practical application value. Our next step is to further expand upon ACGC to better characterize the behaviors of IoT devices; at the same time, we will continue to study optimization strategies to further reduce time and space overhead, achieving performance optimization of ACGCCk.
Jingyu Liu, Master’s student, CCF student member, main research area is formal technology.
Xuansong Li, Ph.D., Associate Professor, CCF professional member, main research areas are software methodology, formal technology, ubiquitous computing technology, IoT security.
Zhifei Chen, Associate Professor, CCF professional member, main research areas are program analysis, software testing, software maintenance.
Haibo Ye, Associate Professor, CCF professional member, main research areas are ubiquitous computing, IoT.
Wei Song, Professor, Doctoral supervisor, CCF distinguished member, main research areas are software engineering and methodology, formal methods, service computing.