Paper Info
Title
SDTIOA: Modeling the Timed Privacy Requirements of IoT Service Composition: A User Interaction Perspective for Automatic Transformation from BPEL to Timed Automata
Abstract
With the development of the Internet of Things (IoT) and the Internet, new kinds of services based on IoT devices will benefit everyone. As a key step in achieving a complex business structure based on a massive number of IoT devices, establishing an effective service composition is extremely important. The emerging architecture of composition is related to process management and is subject to security risks, such as privacy leaks. Traditional service composition methods have difficulty verifying the timed privacy requirements of an IoT service composition. Therefore, this paper proposes an automatic method of transforming Business Process Execution Language (BPEL) into timed automata for formal verification, with the aim of formalizing timed privacy requirements for the IoT service composition and verifying the formal model returned to the UPPAAL supporting tool. First, a privacy requirement template is introduced to analyze the structure of the IoT service composition. Then, a timed computation tree logic (TCTL) property formula template is used to describe the privacy requirements, especially time constraints. Second, an extended timed I/O automata model, namely, the Sensitive Data Timed I/O Automata (SDTIOA) model, is proposed to formalize communication behavior, sensitive data treatment, and service time. Third, the corresponding transformation rules and algorithms are designed for BPEL and SDTIOA. These models can be adjusted through user interaction. Next, as a practical engineering application, we develop a prototype to show how to work with UPPAAL and generate UPPAAL code from SDTIOA code. Finally, a case study is discussed to illustrate the processes of modeling and timed verification for an IoT service composition.
Year
DOI
Venue
2021
10.1007/s11036-021-01846-x
MOBILE NETWORKS & APPLICATIONS
Keywords
DocType
Volume
IoT service composition, Privacy requirements, BPEL verification, Timed automata, User interactions, UPPAAL
Journal
26
Issue
ISSN
Citations 
6
1383-469X
4
PageRank 
References 
Authors
0.42
0
5
Name
Order
Citations
PageRank
Honghao Gao121745.24
Yida Zhang240.42
Huaikou Miao345168.03
Ramón J. Durán Barroso440.42
Xiaoxian Yang561.47