Model checking

Formal verification

Automaton

Distributed computing

Economy

Business

Artificial intelligence

Economics

Marketing

Work in process

Programming language

Consistency (knowledge bases)

Model transformation

Service (business)

Web service

Computer science

Business Process Execution Language

Service-oriented architecture

Theoretical computer science

Business process

Mobile Networks and Applications

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.

SDTIOA: Modeling the Timed Privacy Requirements of IoT Service Composition: A User Interaction Perspective for Automatic Transformation from BPEL to Timed Automata