The rapid development of the Internet of Things (IoT) spurs strong global demand for related applications and technologies, especially in enhancing system reliability and security. Communication security, mobility, and real-time are the three vital features for constructing secure and reliable IoT systems. Formal methods, based on rigorous mathematical theory, are widely used to describe, analyze, model, and verify software and hardware systems, significantly improving their security and reliability. However, the current research mainly focuses on the practical applications of IoT, and there are still few studies on applying formal methods to IoT systems. As a response, our recent work has proposed the SMrCaIT calculus, which is the only process calculus currently designed for IoT that can comprehensively describe the security, real-time, and mobile features of IoT. Applying the SMrCaIT calculus enables us to model and verify IoT systems before their actual implementation, thereby providing a solid theoretical foundation for building secure and reliable IoT systems. To verify the correctness of the SMrCaIT programs, this article presents a proof system for SMrCaIT calculus, based on the extended Hoare Logic considering time. Additionally, we explore the cooperation test between isolated proofs to further ensure that messages are delivered correctly between IoT entities. The soundness of the proof system is also confirmed. A Vehicle Ad Hoc Network case and a Multi-Unmanned Aerial Vehicle case demonstrate the usability of our proof system in analyzing IoT scenarios.

Business Process Model and Notation (BPMN) has been widely adopted as the international standard for business process modeling in enterprise applications. However, existing BPMN models lack rigorous semantic definitions, leading to significant challenges in correctness verification, including deadlock detection and data conflict analysis. Divergent implementations across execution engines further exacerbate such ambiguities. To address these gaps, this paper proposes BDafny: a formal execution and verification framework for BPMN 2.0. Based on Dafny, the verification-aware language, BDafny provides: (1) Executable formalization of BPMN 2.0 semantics for Hoare-logic based behavioral reasoning. (2) Automated and proven detection of practical modeling errors. (3) Multi-target code generation for portable process deployment. By bridging formal methods with industrial standards, BDafny contributes a mechanically verified foundation for BPMN semantics, supporting correct-by-construction automation of business processes.

Communicating Sequential Processes (CSP) is a formal language used in modeling and verifying concurrent systems and protocols. However, manually constructing a CSP model is typically time-consuming. Recent advancements in Large Language Models (LLMs) show potential for automatically transforming requirements in natural language into formal specifications. In this paper, we propose the first datasets of CSP: CSP#-PAT-84 and CSP#-Handwrite-45, containing a total of 129 models and 1375 processes in a machine-readable syntax CSP#. The CSP#-PAT-84 dataset comprises CSP models from examples in the Process Analysis Toolkit (PAT) and covers five categories. The CSP#-Handwrite-45 dataset consists of CSP models extracted from research papers focusing on practical protocols, algorithms, and systems. Moreover, we introduce NL2CSP, a multi-stage approach designed to improve the performance of LLMs in generating codes in CSP#. Experiments are conducted on both the process generation and model generation tasks to evaluate the capability of LLMs to generate correct CSP processes and models, as well as to establish a benchmark for future research. The results demonstrate that with the capability of in-context learning, LLMs can understand most of the requirements written in natural language and generate corresponding CSP processes and models.

The Web Application Messaging Protocol (WAMP) is a routed protocol designed to connect components in distributed applications through Publish/Subscribe and Remote Procedure Call messaging patterns.It defines a Basic Profile for core interactions and an Advanced Profile to extend its functionality.With its flexibility, scalability, and ability to support various communication patterns, WAMP has gained significant attention in distributed systems.However, existing studies on the communication and security properties of WAMP remain limited.In this paper, we employ the Communicating Sequential Processes (CSP) to model the two patterns of WAMP formally and verify several properties using Process Analysis Toolkit (PAT), including deadlock-freedom, data reachability, concurrency and ordering consistency.Verification results confirm that the model satisfies these properties, ensuring the reliability of interactions under various scenarios.Furthermore, by incorporating an intruder model and WAMP's optional authentication mechanisms from the Advanced Profile, we demonstrate improved security guarantees.

The Advanced Message Queuing Protocol (AMQP), an application-layer protocol based on the publish/subscribe model, is widely used in the field of distributed communication.To verify the correctness of its messaging mechanism and crashhandling mechanism, this paper employs the Multiparty Session Types (MPST) theory and the mpstk toolkit to formally model and verify the AMQP protocol.This paper introduces crash scenarios into the AMQP protocol and verifies the safety, deadlockfreedom, and liveness of both the protocol's messaging mechanism and crash-handling mechanism.The verification results demonstrate that the messaging mechanism and crash-handling mechanism of the AMQP protocol satisfy the aforementioned properties, proving its reliability.

XMPP is an open-standard communication protocol, offering services including near-real-time messaging, presence information and request-response.Owing to its exceptional openness, flexibility and scalability, it has been extensively adopted in cloud computing and the Internet of Things (IoT).Consequently, ensuring the reliability and security of the XMPP protocol is of great importance.In this paper, we employ process algebra CSP (Communicating Sequential Processes) to model the communication mechanism of the XMPP system.Additionally, the model checking tool PAT (Process Analysis Toolkit) is utilized to verify six critical properties: deadlock freedom, client faking, server faking, data reachability, key leakage and data leakage.The verification results demonstrate that the XMPP communication mechanism guarantees reliability and security.

Verilog is a hardware description language (HDL) that has become an industry-standard HDL of IEEE. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. Previously, we have studied the operational semantics and denotational semantics for MDESL. This article investigates the soundness and completeness of the operational semantics for MDESL based on the denotational semantics. We introduce the concepts of transitional condition and phase semantics for each transition to show the relationship between a transition and variables in the denotational model. Then, we give the definition for the soundness and completeness of the operational semantics for MDESL. Based on our definition of the operational semantics of MDESL, we investigate the detailed theoretical proof for the soundness and completeness. Finally, a practical approach complements the theoretical one. We apply the proof assistant Coq to verify the soundness and completeness of the operational semantics for MDESL. Our research demonstrates the consistency between operational and denotational semantics for MDESL through theoretical and practical approaches.

Cloud communication, as a core component of the cloud computing architecture, relies on the communication mechanism of TCP/UDP protocols. However, with the popularity of cloud communication, the security threats that it faces are also becoming increasingly severe. Graphene is a new cloud communication security architecture that targets both TCP and UDP communication. It provides security assurance during data transmission and authentication for cloud users and cloud service providers, effectively addressing some of the shortcomings of traditional security protocols. In light of Graphene’s advantages, it is gaining increasing attention from industries. Hence, ensuring the reliability of Graphene becomes paramount. In this paper, we first utilize process algebra CSP to model the TCP-based communication processes within the Graphene architecture. Subsequently, we model the UDP-based communication processes as well. Then, we employ the model checker PAT to run the CSP models for both protocols and subsequently verify six properties: Deadlock Freedom, Divergence Freedom, Data Reachability, Cloud User Faking, Cloud Instance Faking, and Central Key Server Faking. According to the verification results, our models for both TCP and UDP satisfy all of the aforementioned properties. Therefore, we can conclude that the communication execution processes for both TCP and UDP in the Graphene architecture fulfill the anticipated security standards, thus indicating the reliability of the system.

AMQP, serving as the application layer standard protocol for advanced message queuing systems, has garnered widespread adoption in middleware systems, including Rab-bitMQ, ActiveMQ, and Qpid. However, the key properties and security of AMQP's messaging mechanism remain unverified. Hence, in this paper, we employ process algebra CSP to formalize the AMQP and verify properties such as deadlock freedom, data reachability, concurrency, sequence consistency, and scala-bility. The verification results indicate that AMQP satisfies these properties, demonstrating the reliability in message transmission. Moreover, to further analyze the security of AMQP messaging mechanism, the intruder model and SSL protocol model are introduced in this work. Meanwhile, the comparison of the verification results with and without SSL is also presented, showing an improvement of the AMQP messaging mechanism security.

Contemporary multiprocessor systems often use weak memory models (WMMs), including Partial Store Order (PSO) in some SPARC implementations. PSO relaxes the store-store constraint by allowing individual cores to use a write buffer for different memory locations. This paper employs the Unifying Theories of Programming (UTP) framework to investigate PSO's trace semantics, acting in the denotational semantics style. In this context, a trace is represented as a sequence of snapshots that track changes in registers, write buffers, and shared memory. Our approach generates the complete set of valid execution outcomes, including potential reorderings, while adhering to proper principles. This paper also introduces a set of algebraic laws tailored for PSO utilizing the concept of ‘head normal form{\prime}. With the introduction of guarded choice, every program can be represented by head normal form. This representation models program execution in the presence of reorderings within the PSO model. Additionally, we also explores the relationship between trace semantics and algebraic semantics, establishing a connection by deriving trace semantics from algebraic semantics.

OpenStack Swift is an object storage system that is part of the open-source cloud platform OpenStack. It adopts a fully symmetric architecture design and is extensively employed in production environments to offer users highly available storage services. In this paper, we model OpenStack Swift's basic architecture, as well as its replication service using communication sequential processes (CSP). Additionally, we extend the audit service in Swift and provide a formal model of it. Various properties of our model are subsequently verified using the model checker PAT. The properties include Deadlock Freedom, Data Reachability, Consistency, Availability, Partition Tolerance (CAP), Basically Available, Soft State, Eventually Consistent (BASE), and Data Integrity. The verification results show that the design of OpenStack Swift satisfies both the CAP and the BASE theories and it achieves Data Integrity. In light of our results, it can be safely concluded that OpenStack Swift provides users with highly available and fault-tolerant services.

Percolator is a distributed transaction model pro-posed by Google to deal with large-scale incremental data of search engines. Based on timestamps, it achieves the snapshot isolation level of multi-version concurrency control. Percolator also inspired distributed transaction models for many databases such as TiDB. In this paper, we model the architecture of Percola-tor using process algebra CSP and implement it with the help of the Process Analysis Toolkit (PAT). Subsequently, we verify and analyze several properties, including deadlock-free, divergence-free, consistency, and snapshot isolation. The verification results show that Percolator satisfies the above properties, but is not serializable, which may lead to data anomalies in some cases.

With the booming development of Internet of Things (IoT), the LoRaWAN protocol, a crucial technology in Low Power Wide Area Network (LPWAN), has attracted academic attention. Numerous studies on the security of LoRaWAN have been proposed, and some of these studies have been rigorously verified. However, there is a lack of a unified verification framework for the LoRaWAN protocol. In this paper, we present a unified, comprehensive, and systematic security verification framework for the LoRaWAN protocol. The framework facilitates the construction of CSP model for the LoRaWAN protocol and enables the implementation of these CSP models in PAT with C#. Additionally, it supports the formal verification of the models. By integrating C# into PAT, our framework gains extensibility, flexibility, and broad applicability. Simultaneously, we introduce intruders in our CSP model to simulate five different types of attacks (Replay attacks, DoS attacks, ACK Spoofing attacks, Bit Flipping attacks, and MITM attacks) to evaluate LoRaWAN’s performance in vulnerable environments. To demonstrate the applicability of our framework, we extend it to higher versions of LoRaWAN and apply it in the manufacturing industry. We not only verify the fundamental properties but also validate the security properties by simulating attacks in PAT. Our work would help to diversely analyze the security aspects related to the LoRaWAN protocol, and provide the foundation for the analysis of enhancing its security and robustness.

With the development of Industry 4.0 (I4.0), the demand for a protocol to unify communication between different devices is dramatically increasing.OPC Unified Architecture (OPC UA) is a protocol that can be used to accomplish information interoperability in manufacturing and its usage is expanding.Some research has been conducted on the implementation approaches for aggregating server pattern OPC UA in vertical integration.However, few efforts have been made on the formal verification of OPC UA as a vertical communication protocol to facilitate manufacture.In this paper, we design an aircraft parts production use case where vertical communication between the management layer and shop floor devices is achieved via OPC UA aggregating server architecture.Information Model and Services are two fundamental contents of the OPC UA protocol.With the help of process algebra Communicating Sequential Processes (CSP), we build the use case OPC UA model and realize both the Information Model and Services using a verification tool, Process Algebra Toolkit (PAT).We verify the general properties of the system (Divergence Freedom and Deadlock Freedom) and functional properties of OPC UA (Service Read Success, Service Call Success, Monitor Variable Success and Monitor Event Success).The results demonstrate the feasibility of the OPC UA protocol in vertical communication.

Cloud communication, as a core component of the cloud computing architecture, relies on the communication mechanism of TCP/UDP protocols.However, with the popularity of cloud communication, the security threats that it faces are also becoming increasingly severe.Graphene is a new cloud communication security architecture that targets both TCP and UDP communication.It provides security assurance during data transmission and authentication for cloud users and cloud service providers, effectively addressing some of the shortcomings of traditional security protocols.In light of Graphene's advantages, it is gaining increasing attention from industries.Hence, ensuring the reliability of Graphene becomes paramount.In this paper, we first use process algebra CSP to model the TCP-based communication process of the Graphene architecture.Then, we use the model checker PAT to run the CSP model of Graphene and subsequently verify six properties, including Deadlock Freedom, Divergence Freedom, Data Reachability, Cloud User Faking, Cloud Instance Faking, and Central Key Server Faking.According to the verification results, our model satisfies all the above six properties.Therefore, we can conclude that the TCP communication execution process in the Graphene architecture fulfills the anticipated security standards, thus indicating that the system is reliable.

Apache Pulsar is a distributed publish-subscribe messaging system that employs a compute-storage separation architecture, which is well-suited for cloud-native environments.Message delivery mechanism is the core function in Pulsar, mainly for transferring data between different objects.The reliability of the message delivery mechanism of Pulsar raises extensive concerns for better application.In this paper, we use process algebra CSP to model the components of Pulsar.By implementing the model using model checker PAT, we mathematically examine the message delivery mechanism of Pulsar.We verify six properties: deadlock freedom, divergence freedom, data consistency, sequentiality, reliability and persistent storage.The verification results indicate that Pulsar satisfies all these properties, demonstrating that it has good performance and can provide robust message transmission services.

The C and C++ languages introduced the relaxed-memory concurrency into the language specification for efficiency purposes in 2011. Trace semantics can provide the mathematical foundation for the proposed C++11 memory model, and there is a lack of investigation of trace semantics for C++11. The Promising Semantics (PS) of Kang et al. provides the standard SC-style operational semantics for the C++11 concurrency model, where “SC” refers to “Sequential Consistency”. Inspired by PS, in this article we first investigate the trace semantics for the relaxed read and write accesses under C++11, acting in the denotational semantics style. In our semantic model, a trace is in the form of a sequence of snapshots, and the snapshots record the modification in the relevant global or local variables, and the thread view. Moreover, the trace semantics for the release/acquire accesses under C++11 is also explored, based on the separated thread views and newly added message views. When considering this trace model, different accesses bring in their unique snapshots, and make distinguished effects on the production of the sequences. For any given program, the proposed trace semantics in this article produces all the valid traces directly. Furthermore, our trace semantics, together with that for TSO and MCA ARMv8, has the possibility to be the foundation of the meta model of the trace semantics for weak memory models.

With the flourish of the Internet of Things (IoT), the group communication Constrained Application Protocol (CoAP) emerged at the historic moment, enabling homogeneous devices with constrained computing ability to communicate with ease. CoAP is widely used in transportation, health care and many other aspects. Hence, it is prominent to propose a flexible and efficient architecture for usage in such scenarios and study the data security and consistency of the architecture from the perspective of formal methods. In this paper, we extend the group communication CoAP model to the enhanced group communication CoAP by the introduction of smart gateways and binding to new security suites. We make further improvements to increase the scalability and flexibility of the architecture, making it more applicable in a healthcare scenario or smart home scenario. And we adopt process algebra Communicating Sequential Processes (CSP) with real-time extension to model the enhanced group communication CoAP. We use model checker PAT to verify eight properties of our model on an abstract level, including four basic properties and four security properties. We also conduct a simulation on the local machine for validation of the above properties on a more detailed level. Despite some simplifications of physical properties, both results of the verification and simulation show that the proposed architecture can satisfy those requirements and demonstrate a good possibility of being securely put into service.

Abstract With the rapid popularization of smart devices, the applications and technologies of the Internet of Things (IoT) are in high demand worldwide, especially in improving development efficiency and ensuring system quality, reliability, and security. Formal methods have been successfully used to specify, verify, and analyze software and hardware systems, effectively alleviating the above problems in these systems. However, most of the existing works mainly focus on the practical applications of IoT, and there is a lack of research on modeling and analyzing IoT systems from the perspective of formal methods. In this paper, we first propose a secure mobile real‐time process calculus for specifying and reasoning about IoT systems, called SMrCaIT, which supports not only value‐passing communication but also name‐passing communication. In addition, this calculus can strictly separate process actions and mobility modeling by providing parametric mobility models. Subsequently, we present the operational semantics of this calculus, in particular, the rules on how to secure channel communication by closing the scope of a channel and handling scope extrusion. Taking vehicle ad hoc network (VANET) as a case, the application details of SMrCaIT and its operational semantics are fully demonstrated. By using the rewrite engine Real‐Time Maude, we further implement SMrCaIT and its operational semantics and verify some properties of the VANET case to indicate the effectiveness of our calculus in real‐world scenes.

Nowadays, the utilization of online auction platforms is becoming increasingly prevalent.Online auction provides a common and practical way for global buyers to compete fairly.Nevertheless, the anonymous environment may bring collusion among entities with effects on results.Compared with traditional mechanisms which rely on third-party platforms, the data auction based on smart contract can create a decentralized environment to avoid the occurrence of collusion.Meanwhile, there exists few research on the verification of its reliability and safety which is worth investigating from the perspective of formal methods.In this paper, we apply Process Algebra CSP in modeling the data auction communicating system among five key entities.In addition, we use Process Analysis Toolkit (PAT) to realize the mechanism and verify five crucial properties, including deadlock freedom, data reachability, data correctness, anti-collusion capability and data security.The verification results indicate that the architecture of data auction based on smart contract can satisfy all the above requirements.Especially, the design of asymmetric encryption for the fundamental information ensures the non-occurrence of collusion in the auction.Additionally, the digital signature generated by private key attached to the message guarantees the safety of the interaction.

As IoT in a multi-server environment increases resources’ utilization, more and more problems of IoT authentication and key agreement are being revealed. The Authentication and Key Agreement (AKA) protocol plays an important role in solving these problems. Many AKA protocols have been proposed, and some of them support their own verifications. However, a unifying verification framework for multi-server IoT is lacking. In this article, we propose a formal verification framework of AKA protocols for multi-server IoT (FVF-AKA). It supports the construction of CSP models for the AKA protocol, the implementation of the CSP models in PAT with C#, and the verification of formal models. With the help of C#, many complex functions in the AKA protocol can be implemented. We also design an algorithm to support automatic conversion from the CSP model to the PAT model. FVF-AKA can verify four fundamental properties (deadlock freedom, entity legitimacy, timeout delay, and session key consistency). It also supports the verification of security properties for the AKA protocol suffering from four different attacks (relay attacks, denial of service attacks, server spoofing attacks, and session key attacks). Our approach can be applied to most AKA protocols for multi-server IoT generally. By applying FVF-AKA to two AKA protocols, we can verify whether they satisfy the fundamental properties and analyze their security properties in vulnerable environments. Our work would help to analyze the AKA protocol for multi-server IoT and provide the foundation for the analysis of enhancing its security and robustness.

Abstract Named Data Networking (NDN) is a new promising architecture of information‐centric networking, which supports multicast of data and adopts the publish/subscribe model in the network. The features of NDN, including name‐based data and in‐network caching, make it a promising Internet architecture for cyber‐physical systems (CPSs). Named‐Data Link State Routing (NLSR) protocol is the routing protocol for NDN, which is designed to disseminate link state advertisements (LSAs) to both build a network topology and distribute all the name prefixes to every node in the network. In this paper, we make the very first attempt to formally model and verify some fundamental properties of the NLSR protocol using model checker UPPAAL. We validate the NLSR protocol modeled into timed automata with simulator in UPPAAL. We verify our model with four fundamental properties (termination, reachability of Sync Interest , reachability of Sync Data , and digest synchronization). The first synchronization problem is found in a scenario with two nodes topology. We give the improved model that owns a valid result in digest synchronization verification. To capture more problems, we make the model to support the simulation of temporary network crash. The second synchronization problem is also exposed in two comparative scenarios. We also propose a mechanism implemented in our model, which has a valid result in digest synchronization verification. We hope that our study and preliminary results would help enhancing the adaptability and robustness of NLSR protocol.

Transactional memory is designed for developing parallel programs and improving the efficiency of parallel pro-grams. PSTM (python software transactional memory) mainly supports multi-core parallel programs based on the python language. In order to better adapt to the developing requirements of distributed concurrent programs and enhance the safety of the system, DPSTM (distributed python software transactional memory) was developed. Compared with PSTM, DPSTM has the advantages of higher operating efficiency and stronger fault tolerance. In this paper, we apply CSP (Communicating Sequential Processes) to formally analyze the components of DPSTM v2 architecture, the data exchange process between components, and two different transaction processing modes. We use the model checker PAT (Process Analysis Toolkit) to model the DPSTM v2 architecture and verify eight properties, including deadlock freedom, ACI (atomicity, isolation, and consistency), sequential consistency, data server availability, read tolerance, and crash tolerance. The verification results show that the DPSTM v2 archi-tecture can guarantee all of the above properties. In particular, the normal operation of the system can be maintained when some of the data servers are crashed, ensuring the safety of a distributed system.

The C++11 standard introduced a language level weak memory model (i.e., the C++11 memory model) to improve the performance of the execution of C/C++ programs. Algebra is well-suited for direct use by engineers in symbolic calculation of parameters. It is a challenge to investigate the algebraic semantics for the C++11 memory model. Inspired by the promising semantics, in this paper, we explore the algebraic laws for the C++11 memory model, including a set of sequential and parallel expansion laws. We introduce the concept of guarded choice, and every program under the C++11 memory model can be converted into the head normal form of guarded choice. In addition, the proposed algebraic laws are implemented in the rewriting engine Maude.

The cyber-physical system (CPS) is a dynamic system that contains both continuous and discrete behaviors. It has a wide range of applications in fields such as health care equipment, intelligent traffic control and environmental monitoring. However, the combination of continuous physical behavior and discrete control behavior may complicate the design of systems further. It is of great necessity to give an explicit formal language and its semantics for CPS. In this paper, we elaborate the modeling language for CPS based on our previous work. This language supports shared variables to model the interaction between the physical and the cyber. Additionally, we give it denotational semantics and algebraic semantics, especially focus on the continuous behavior and its composition with the discrete behavior. Throughout this paper, we also present some examples to illustrate the feasibility of the language and its semantics.

In the era of 5G, users are extremely sensitive to time delay and have strict reliability requirements. The architecture of MEC can effectively reduce or even eliminate the impact of return delay, whose core idea is to localize the data reasonably. Actually, most of the work still concentrated on the balance between the efficiency and energy consumption of task offloading strategy, but few work analyzed and expounded its offloading characteristics from the perspective of formal methods. Henceforth, In this paper, we propose a real-time secure hierarchical process calculus rMECal of task offloading for MEC. Then we show the operational semantics of this calculus from the process and network levels to describe how the program works, especially the parallel composition rule for many-to-many broadcast communication. In addition, we formalize the calculus and rules with real-time Maude, and adopt the example of Internet of Vehicles to illustrate the availability of the calculus and operational semantics. Moreover, we give the denotational semantics of this calculus to express what the program executes based on the Unifying Theories of Programming (UTP) approach, and show the fundamental algebraic properties. We believe that this paper can provide a guidance for exploring the formal theories in MEC.

Nowadays, many applications are built on distributed databases for scalability and high availability.Therefore, the architecture design of distributed databases needs to satisfy some functional properties to ensure that the database can perform transactions reliably and efficiently.COCO is a distributed OLTP database that supports epoch-based commit and replication and two variants of optimistic concurrency control which use physical time or logical time.In this paper, we first use process algebra CSP to model COCO's architecture.Then we use model checker PAT to verify seven properties, including deadlockfree, consistency, availability, partition tolerance (CAP), and basically availability, soft state, eventual consistency (BASE).The results show COCO's commit and replication protocol satisfy the CAP theorem, and two optimistic concurrency control variants satisfy the BASE theorem.

The Internet of Things (IoT) is an important technology in IT industries.The wide adoption of IoT raises concerns about security and privacy.The Authenticated Publish/Subscribe (AUPS) model is an IoT system which aims to address the security and privacy issues in the IoT environment.AUPS is attracting more and more attention from industries.Hence, the reliability of AUPS is worth investigating.In this paper, we model AUPS using Communicating Sequential Processes (CSP).Five properties (Deadlock Freedom, Data Availability, Data Leakage, Device Faking and User Privacy Leakage) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT).The verification results demonstrate that AUPS cannot ensure the security of critical data.To solve the problem, we improve the model by using a digital certificate.The verification results of the improved model indicate that our study can enhance the security and reliability of the AUPS model.

Abstract As a crucial component of intelligent transportation system, Internet of Vehicles (IoV) plays an important role in the smart and intelligent cities. However, current Internet architectures cannot guarantee efficient data delivery and adequate data security for IoV. Therefore, Named Data Networking (NDN), a leading architecture of Information‐Centric Networking (ICN), is introduced into IoV. Although problems about data distribution can be resolved effectively, the combination of NDN and IoV causes some new security issues. In this paper, we apply Communicating Sequential Processes (CSP) to formalize NDN‐based IoV. We mainly focus on its data access mechanism and model this mechanism in detail. By feeding the formalized model into the model checker Process Analysis Toolkit (PAT), we verify four vital properties, namely, deadlock freedom, data reliability, PIT deletion faking, and CS caching pollution. According to verification results, the model cannot ensure the security of data with the appearance of intruders. To solve these problems, we construct a blockchain‐based mechanism by creating a blockchain‐based distribution trusted platform on top of NDN‐based IoV. Through the analysis of the improved model, the blockchain‐based mechanism can truly guarantee the security of NDN‐based IoV.

Mobile Edge Computing (MEC), as an emerging technology, is proposed to solve the time delay problem in 5G era, especially in the field of autonomous driving. The core idea of MEC is to offload the task to the nearest device/server for computation, i.e., sinking the computation, so as to reduce the delay and congestion. Actually, there are lots of researches on MEC offloading strategy, but there is little research on the computation of its offloading characteristics. Therefore, in this paper, we first propose a secure hierarchical calculus SC4MEC to describe the features of MEC. We also give the syntax and operational semantics of this calculus from the process and network levels, and simulate the calculus in Maude. Meanwhile, local ecology is applied to the communication channel to further reduce the authentication delay of the device with the same identity and ensure the security of the transmission data. We also propose to extend the communication radius of MEC server or cloud server by rule Enlarge, in order to ensure the mobile devices's connectivity while the consumption of resources is minimized. Finally, we employ SC4MEC calculus to a small example about device to device communication with automated implementation.

Dubbo is a high-performance, lightweight Java Remote Procedure Call (RPC) framework developed by Alibaba, which provides interface-oriented remote method call, intelligent fault tolerance and automatic service registration.Since Dubbo is extensively applied recently as an excellent representative RPC framework, it is of great significance to formally analyze Dubbo.In this paper, we use Communicating Sequential Processes (CSP) to model and formalize Dubbo.In order to enhance the reliability of the call, we use token authentication mechanism in the modeling process.Moreover, we put the CSP description of the established model into the model checker Process Analysis Toolkit (PAT) for simulation and verification.We verify whether the four properties are valid, including Deadlock Freedom, Connectivity, Robustness and Parallelism.Our final verification results show that the model can satisfy these properties, thus we can conclude the framework can guarantee the highly available remote call.

As a key technology of the Internet of Things (IoT), middleware plays an important role in managing virtualized resources and services.However, traditional Internet architectures cannot ensure adequate data security and efficient data delivery for IoT middlewares.Therefore, Information-Centric Networking (ICN), a paradigm of the future network, is introduced into IoT middlewares.Since ICN-IoT middleware is attracting more and more attentions, its security is worth discussing.In this paper, we adopt Communicating Sequential Processes (CSP) to model the ICN-IoT middleware architecture.Five properties (deadlock freedom, data availability, action keys leakage, device faking and user faking) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT).According to the verification results, the model cannot guarantee the security of data.To solve the problems, we encrypt messages with the receiver's public key, and improve the model by introducing a method similar to the digital signature.The new verification results demonstrate that our study can assure the security of the ICN-IoT middleware architecture.

Hybrid systems are composed of physical components with continuous variables and discrete control components. Over time, the interacting laws of discrete and continuous dynamics manage the transition of states in hybrid systems. The operation of hybrid systems needs the combinations of computation and control. However, those combinations add the complexity of the system design and modelling. Therefore, a hybrid relational modelling language (HRML) was proposed to capture the features of hybrid systems.In this paper, we formulate a proof system for HRML to prove the correctness of hybrid systems. In our proof system, the specification and verification are based on Hoare Logic. To express the timing of observable actions, we extend the classical assertion language by adding primitives to it. Both terminating and non-terminating computations can be described in our proof system. In addition, some detailed examples are given to illustrate the application of our proof system.

With the popularization and development of 5G, it is vital to guarantee the security of the whole data while transmitting them at high speed. Data Distribution Service (DDS), as the core technology of network data communication, is one of the most significant protocols. The Real Time Publish Subscribe (RTPS) protocol is part of DDS, which emphasizes data publishing and receiving.In this paper, we focus on the Behavior module of the RTPS protocol, where the reliable modes are always to ensure the reliability of data. Thus, we adopt CSP to model eight core components and add corresponding intruders to attack the model in order to verify and detect the potential risks of the design. Specifically, we also improve our model by utilizing digital signature and digital certificate. Five properties abstracted from the specification have been verified through the model checker PAT. The result shows that once adding the digital signature and digital certificate together, there is no situation that publisher and subscriber are unauthorized; in addition, due to multiple encryption, data cannot be faked or intercepted. However, the history-cache still can be faked for it has no identity authentication. That is to say, to be highly trustworthy, developers need to ensure mutual authentication between modules as much as possible. Consequently, we hope this method makes sense for researches on security of data distribution protocol and gives a meaningful guide for DDS middleware development.

The combination of D2D (Device to Device) communication and MEC (Mobile Edge Computing) architecture is adopted to reduce the communication delay in 5G. With the extensive use of HPS (high performance switch) as the main medium of data distribution in the device layer, the holistic power consumption and delay can be guaranteed stably, mainly because HPS has the mechanism of Master-Slave scheme to ensure the robustness. However, as far as we know, there are fewer studies to verify the safety validation of the design using formal methods. Hence, we study it through timed automata and model checking. This paper integrates HPS into D2D communication design in MEC, selects the Master-Slave synchronization and switchover scheme in HPS as the research object, describes the scheme based on timed automata, and then verifies seven fundamental but essential properties through the model checker UPPAAL. Through verification, comparison and analysis of possible scenarios in our constructed model, it can be concluded that the design of the HPS in MEC can conform to its required specification. Further, it can not only enhance the safety validation of the combination of D2D communication and MEC architecture, but also provide a guide for the newest subsequent high safety primary-backup design in industry.

Summary Software Defined Networking (SDN) with multiple controllers draws more attention for the increasing scale of the network. Multi‐controller architectures can handle what SDN with single controller is not able to address. In order to understand what these architectures can accomplish and face precisely, we analyze them with formal methods. In this paper, we apply Communicating Sequential Processes (CSP) to model the routing service of SDN under multi‐controller architectures, in particular the HyperFlow architecture and the Kandoo architecture based on OpenFlow protocol. By using model checker Process Analysis Toolkit (PAT), we verify that the models satisfy three properties, namely deadlock freeness, consistency, and fault tolerance. In addition, for studying the security of those models, some extension is added. We find that the extended models are capable of coping with Denial of Service and may suffer from Information Disclosure. Moreover, a fake path and a tampered message could be present in SDN.

Abstract In this paper, we present a process calculus called BigrTiMo that combines the rTiMo calculus and the Bigraph model. BigrTiMo calculus is capable of specifying a rich variety of properties for structure-aware mobile systems. Compared with rTiMo, our BigrTiMo calculus can specify not only time, mobility and local communication, but also remote communication. We then investigate the operational semantics of the BigrTiMo calculus and develop an executable formal specification of our BigrTiMo calculus in a declarative language called Maude. In addition, we verify safety properties and liveness properties of the mobile systems described by BigrTiMo using state exploration and LTL model checking in Maude. Based on Hoare and He's Unifying Theories of Programming (UTP), we study the semantic foundation of this highly expressive modelling language and propose a denotational semantic model and a set of algebraic laws for it. The semantic model in this paper covers time, location, communication and global shared variable at the same time. We also demonstrate the proofs of some algebraic laws based on our denotational semantics. Moreover, we explore how the algebraic semantics relates with the operational semantics and denotational semantics, which is conducted by the study of deriving the operational semantics and denotational semantics from algebraic semantics. We prove the equivalence between the derived transition system (e.g., the operational semantics) and the derivation strategy, which indicates that the operational semantics is sound and complete.

Abstract In the effort to develop critical cyber‐physical systems, it is tempting to extend existing computing formalisms to include continuous behaviour. This may happen in a way that neglects elements necessary for correctly expressing continuous properties of the mathematics and correct physical properties of the real‐world physical system. A simple language is taken to illustrate these possibilities. Issues and risks latent in this kind of approach are identified and discussed under the umbrella of ‘healthiness conditions’. Modifications to the language in the light of the conditions discussed are elaborated, resulting in the language Combined Discrete and Physical Programmes in Parallel (CDPPP). An example air conditioning system is used to illustrate the concepts presented, and it is developed both in the original ‘unhealthy’ language and in the modified ‘healthier’ CDPPP. The formal semantics of the improved language is explored.

As a leading architecture of Information-Centric Networking (ICN), Named Data Networking (NDN) plays an important role in the future network construction. NDN retrieves and identifies a data packet according to the packet's name instead of its IP address. Conventional protocols of TCP/IP Internet are unsuitable for NDN. Therefore, Named-data Link State Routing protocol (NLSR) is proposed as an intra-domain routing protocol for NDN. Although NLSR applies a five-layer trust model to guarantee its data security, there are still a lot of security issues in its data access mechanism, such as the fake and leakage of data. In this paper, we apply Communicating Sequential Processes (CSP) to formalize this mechanism. Using Process Analysis Toolkit (PAT), we verify four properties, including deadlock freedom, data availability, data security and data decryption. According to the verification results, the trust model cannot protect the data from fake and leakage once intruders appear. We adopt a method similar to digital signature in the first improved model. However, the process of obtaining keys still needs to be executed multiple times during the verification of a data packet. To further accelerate the key fetching and verification process, all the keys, needed to validate a data packet, are packaged in a special packet of the second improvement.

BigrTiMo [1], a process algebra that combines the rTiMo calculus [2] and the Bigraph model [3], is capable of specifying a rich variety of properties for structure-aware mobile systems. Compared with the rTiMo model, our BigrTiMo calculus can specify not only time, mobility and the local communication (the two communication components should be at the same location), but also the remote communication (the two communication components can be at the different locations). In this paper, we present an axiomatic approach to BigrTiMo program language verification based on Hoare-style [4] proof rules. In order to describe the timing of observable actions and the state of the bigraph, we extend the assertion language with primitives. Moreover, we prove the soundness of our proof rules and show the application of the proof rules via an example.

RabbitMQ is a very popular message middleware, which is an implementation of AMQP (Advanced Message Queuing Protocol) using the Erlang language. It supports concurrency and guarantees the sequential consistency of messages. Additionally, RabbitMQ provides the message acknowledgement mechanism to ensure that messages can be delivered reliably to the consumer from the broker. However, these crucial properties have not been verified with formal methods. In this paper, we model the architecture of RabbitMQ with timed automata. By utilizing the model checker UPPAAL, RabbitMQ is abstracted to five timed automata. Based on the formalized model, we verify whether RabbitMQ meets some essential properties, including Reachability of Data, Concurrency, Sequence Consistency and Message Acknowledgement. Consequently, it can be found that RabbitMQ can totally satisfy these properties according to the verification results via UPPAAL.

Abstract The hardware description language Verilog has been standardized and widely used in industry. Multithreaded Discrete Event Simulation Language (MDESL) is a Verilog-like language and it contains a rich variety of interesting features such as the event-driven computation and shared-variable concurrency as well as the realtime feature. In this paper, we present the denotational semantics for MDESL based on UTP. First a discrete time semantic model is proposed to describe the observation-oriented semantics for MDESL. The observations record the change of variables of atomic actions over time. Then the healthy formulae are defined to denote all different behaviors of programs and the semantics of programs is expressed in terms of healthy formulae. In addition, we demonstrate some interesting properties about the MDESL programs expressing as algebraic laws and their proofs are supported by our formalized denotational semantics. Our theoretical approach is complemented by a practical one, we use the theorem proof assistant Coq to formalize the UTP-based semantics for MDESL. The correctness of the algebraic laws is also verified via the mechanical approach in Coq. Our work provides a novel way to verify the correctness of UTP-based semantics forMDESL both in a theoretical approach and in a practical approach. It is also a new attempt for the application of Coq in the mechanized semantics.

Starting with the analysis of the source codes of the Python Software Transactional Memory (PSTM) architecture, this paper applies process algebra CSP to formally verify the architecture at a fine-grained level. We analyze the communication process and components of the architecture from multiple perspectives and establish models describing the communication behaviors of the PSTM architecture. We use model checker PAT to automatically simulate and verify the established model. After adapting the traditional transactional properties to the PSTM architecture, we analyze and verify five properties for the PSTM architecture, including deadlock freeness, atomicity, isolation, consistency and optimism. The verification results indicate that all the properties are valid. Based on the judgement of the execution logic of the communication procedure in the PSTM architecture, we can conclude that the architecture can have a proper communication and can guarantee atomicity, isolation, consistency and optimism. Besides, we also provide a case study with an application scenario and propose a corollary that the value of the shared counter is equal to the number of parallel processes. We verify whether the case study system can satisfy all the conditions of corollary from both positive and negative perspectives. The results show that the corollary is tenable.

Model Driven Engineering (MDE) uses models to represent the core part of the software systems. The Unified Model Language (UML) is a widely accepted standard for modeling software systems. Although UML provides numbers of concepts and diagrams to describe the system, there is still an unsolved problem that the semantics and refinement relations of models are not formally defined. In this paper, we apply the constructive type theory to formalize the class diagrams and object diagrams. A suitable subset of UML static models is identified and formally defined. The theorem assistant Coq is applied to encode the semantics of class diagrams. Moreover the refinement relations are also formalized in Coq. The whole approach is supported by tools that do not constrain the semantic definition's expressiveness and flexibility while making it machine-checkable. Our approach offers a novel way for giving a precise foundation in UML and contributes to the goal of improving the overall trustworthy software systems by combining theoretical and practical techniques.

The Unified Modeling Language (UML) provides a number of diagrams to describe the modeling system from different perspectives, which contain overlapping information about the systems.However, it does not provide any means of meticulously checking consistencies among the overlapping elements.In this study, we propose an approach for consistency checking of UML class diagrams and object diagrams using Prolog.First we formalize the model elements based on metamodel and convert the models into Prolog facts.Then we define some consistency rules that are encoded into Prolog.The Prolog's reasoning engine automatically checks the consistencies of models.In addition, we provide interfaces to query models for properties, elements and submodels.The design errors can be effectively avoided and the correctness of code-generalization can be guaranteed according to our approach.

Cloud computing is an emerging computing paradigm in IT industries.The wide adoption of cloud computing is raising concerns about management of data in the cloud.Access control and security are two critical issues of cloud computing.Time efficient secure access control (TESAC) model is a new data access control scheme which can minimise many significant problems.This scheme has better performance than other existing models in a cloud computing environment.TESAC is attracting more and more attentions from industries.Hence, the reliability of TESAC becomes extremely important.In this paper, we apply Communication Sequential Processes (CSP) to model TESAC, as well as their security properties.We mainly focus on its data access mechanism part and formalize it in detail.Moreover, using the model checker Process Analysis Toolkit (PAT), we have verified that the TESAC model cannot assure the security of data with malicious users.For the purpose of solving this problem we introduce a new method similar to digital signature.Our study can improve the security and robustness of the TESAC model.

The Real Time Publish Subscribe protocol (RTPS), as a Data Distribution Service (DDS) protocol for computer systems, is composed of several modules.We focus on RTPS StatefulWriter Module which has two patterns, reliable pattern and best-effort pattern.As the main module of sending and receiving messages, its security and reliability are of great concern.The formal method can analyze whether it is a highly credible model from the mathematical point of view.Our research pays attention to the reliable pattern.Thus it is of great importance to model and verify whether the pattern is reliable through formal methods.In this paper, we model seven components of the module using Communicating Sequential Processes (CSP).By feeding the models into the model checker Process Analysis Toolkit (PAT), we verify four properties, divergence free, acknowledgement mechanism, data consistency and sequentiality.Consequently, it can be apparently concluded that the pattern of this module is reliable, which totally caters for its specification.

Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as an atomic block. Python Software Transactional Memory (PSTM) is an STM implementation in Python language. Its presentation fills a gap that Python lacks an applicable and reliable software transactional memory. PSTM satisfies the basic transaction properties, however it does not satisfy opacity, which defines conditions for serialising concurrent transaction. To alleviate this issue, we modify the PSTM implementation and present a new PSTM called PSTM-M. Based on PSTM-M, we verify opacity of this implementation. We present the formalization of opacity which is based on the history model of transaction. Further, we explain why PSTM does not satisfy opacity and present a modified PSTM called PSTM-M. Finally, we give a machine-checked proof for the opacity of PSTM-M based on the theorem prover Coq.

Transaction Memory (TM) is designed for simplifying parallel programming, while some key problems exist in it, such as starvation and reduced performance with high contention among transactions. In order to improve the performance of TM, researchers have designed several transaction scheduling algorithms and given their experimental results. However, the evaluations on the algorithms given by these researches are rather partial and lack of generality. Since these experimental results ignore the verification of properties which are necessary for transaction scheduling and could be greatly affected by the execution environment, thus it is still challenging for us to judge the quality of the algorithms for TM. In this paper, we provide a formal approach to evaluate transaction scheduling algorithms in a more comprehensive and strict way. We choose three recently proposed algorithms as motivating examples and formalize them using the process algebra CSP. We also use a model checker PAT to verify the properties (e.g., deadlock freeness and starvation freeness) of the models. Besides, it is also easier to compare the performance of the algorithms, from the perspective of makespan, speedup, aborts time and throughput, based on the statistics given by PAT. Consequently, a formal approach can be achieved to evaluate transaction scheduling algorithms, which is also a good guide for the further design of the algorithms for TM.

The Clock Constraint Specification Language (CCSL) is a clock-based formalism for formal specification and analysis of real-time embedded systems. Previous approaches for the schedulability analysis of CCSL specifications are mainly based on model checking or SMT-checking. In this paper we propose a logical approach mainly based on theorem proving. We build a dynamic logic called 'clock-based dynamic logic' (cDL) to capture the CCSL specifications and build a proof calculus to analyze the schedule problem of the specifications. Comparing with previous approaches, our method benefits from the dynamic logic that provides a natural way of capturing the dynamic behaviour of CCSL and a divide-and-conquer way for 'decomposing' a complex formula into simple ones for an SMT-checking procedure. Based on cDL, we outline a method for the schedulability analysis of CCSL. We illustrate our theory through one example.

Cloud computing is an emerging computing paradigm in IT industries. The wide adoption of cloud computing is raising concerns about management of data in the cloud. Access control and data security are two critical issues of cloud computing. Time-efficient secure access control (TESAC) model is a new data access control scheme which can minimize many significant problems. This scheme has better performance than other existing models in a cloud computing environment. TESAC is attracting more and more attentions from industries. Hence, the reliability of TESAC becomes extremely important. In this paper, we apply Communication Sequential Processes (CSP) to model TESAC, as well as their security properties. We mainly focus on its data access mechanism part and formalize it in detail. Moreover, using the model checker Process Analysis Toolkit (PAT), we have verified that the TESAC model cannot assure the security of data with malicious users. For the purpose of solving this problem, we introduce a new method similar to digital signature. Our study can improve the security and robustness of the TESAC model.

In a mobile system, mobility refers to a change in position of a mobile object with respect to time and its reference point, whereas isolation means the isolation relationship between mobile objects under some scheduling policies. Inspired by event-based formal models and the ambient calculus, we first propose the two types of special events, entering and exiting an ambient, as movement events to model and analyze mobility. Based on mobility, we then introduce the notion of the isolation of mobile objects for ambients. To ensure the isolation, a priority policy needs to be used to schedule the movement of mobile objects. However, traditional scheduling policies focus on task scheduling and depend on the strong hypothesis: The scheduled tasks are independent—that is, the scheduled tasks do not affect each other. In a practical mobile system, mobile objects and ambients interact with each other. It is difficult to separate a mobile system into independent tasks. We finally present an automatic approach for generating a priority scheduling policy without considering the preceding assumption. The approach can guarantee the isolation of the mobile objects for ambients in a mobile system. Experiments demonstrate these results.

Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. It contains interesting features such as event-driven computation and shared-variable concurrency. This article considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. First, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Second, we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, and we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.

In automobile industry, it is a common approach to develop automobile real-time operating systems under some standards. For instance, OSEK/VDX is a world-wide adopted open standard. Traditional workflow is to first understand the standard, design and develop a system, then test its conformance to the standard, and finally deploy. There are several issues with the traditional workflow, e.g., ambiguities in standards may lead to incorrect design and implementation of real-world systems; the conformance of real-world systems to standards is difficult to check; and bug fixing after implementation is costly. To remedy the situation, in this paper, we present a unified executable formal automobile kernel under OSEK/VDX standard by defining the operational semantics of the system services in the standard using a rewrite-based executable semantic framework called$\mathbb {K}$. The formal kernel isunifiedin that it serves multiple purposes such as: 1) formal modeling of the OSEK/VDX standard helps detect ambiguities in the standard; 2) the executable kernel is essentially a formal model of the standard, which can be used to verify the correctness of automobile applications; and 3) verified applications can be used as test cases to check the conformance of a real-world automobile operating system against the OSEK/VDX standard. Using the formal kernel, we identify several ambiguities in the OSEK/VDX standard and a potential deadlock vulnerability in an industrial automobile application.

Moose File System (MooseFS) is an Open-source, POSIX-compliant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Its high performance, high availability and fault-tolerant features have drawn huge interest from industry. However, the correctness of the dominate parts including reading and writing files of MooseFS has not got much attention of academia, which is the main concern of industry. In this paper, we use the process algebra Communicating Sequential Process (CSP) to model and analyze MooseFS. We mainly focus on the dominant parts which include reading and writing files in MooseFS and formalize them in detail. On that basis, we use the model checker Failures Divergence Refinement (FDR) to automatically simulate the developed model and verify whether the model is consistent with the specification and exhibits relevant secure properties including deadlock freedom, divergence-free, mutual exclusion and backup scheme.

OpenFlow is considered as one of the first standard of software defined networking (SDN). The OpenFlow scheduled bundle mechanism is a latest mechanism proposed in OpenFlow protocol to guarantee the completeness and consistency of messages transimitted between SDN switches and controllers during the communication process. Due to the requirement of reliability and security, it is of great significance to formally analyze and verify the mechanism. In this paper, we apply Communication Sequential Processes (CSP) and use the model checker Process Analysis ToolKit (PAT) to model and verify the OpenFlow scheduled bundle mechanism. We verify the main property of the mechanism, schedulability. In addition, we analyze and verify the security of the mechanism and find that it suffers from some kinds of possible attacks.

BigTiMo calculus is for structure-aware mobile systems and it combines the TiMo calculus and the Bigraph model. Compared with TiMo, BigTiMo can model not only the locations of the components but also the connectivity of the components. Thus, our BigTiMo process can communicate not only locally with other process, but also remotely with other process. In this paper, we introduce the syntax and the operational semantics of the BigTiMo calculus. We also develop an executable formal specification of our Big-TiMo calculus in a declarative language called Maude. In addition, we verify safety properties of the mobile systems described by BigTiMo using state exploration and LTL model checking in Maude.

Leader election is a fundamental problem in distributed systems and has a variety of applications in wireless networks, such as key distribution, routing coordination, and general control.The main statement of the leader election problem is to eventually elect a unique leader from a fixed set of nodes.As the wireless network is becoming more and more important in daily life, leader election algorithm plays a vital important role in wireless network, which makes the correctness and robustness of such algorithms become evermore important and challenging to establish.In this paper, firstly, we study an election algorithm LE for MANETs (Mobile Ad Hoc Network) designed by Vasudevan et al.Then we present a formal model for LE based on process algebra CSP (Communicating Sequential Process).Modeling algorithm like LE sometimes pose non-trivial challenges, time, geometry, communication delays and failures, mobility and bi-directionality can interact in unforeseen ways that are hard to model and analyze by automatic formal methods, but we will take on these challenges.On that basis, we use the model checker FDR (Failures Divergence Refinement) to automatically simulate the developed model and verify whether the model is consistent with the specification and exhibits relevant secure properties.Our results show the correctness and safety of LE in this respect.

Named Data Networking (NDN) is a new promising architecture of information-centric networking.For its caching property, traditional mechanisms of access control can no longer work.Hamdane et al. propose a new access control solution for both closed and open environments.In this paper, we make the very first attempt to formally analyze this access control solution.Inspired by the basic BAN logic which is often used to describe protocols by logical formulas, we present our BAN-like logic by adding some new notions to make it suitable for the access control solution.Using the BAN-like logic, the procedures of the access control solution is idealized in the form of the beliefs of principals.Then the idealized procedures are analyzed under several security goals with a set of logical postulates.Several unsatisfied goals may lead the access control solution to be vulnerable to intruders.We give the modification in the idealized procedures to archive more goals.We also present the related modification in the implementation of the access control solution.Our study helps to improve security and protect against various attacks for the access control solution.

Software Defined Network (SDN) is an emerging architecture of computer networking.The most important feature of SDN is that it separates the control plane from the data plane.OpenFlow is considered as the first and currently most popular standard southbound interface of SDN.It is a communication protocol which enables the SDN controller to directly interact with the forwarding plane.The widespread use makes the reliability of OpenFlow important.The OpenFlow bundle mechanism is a new mechanism proposed by OpenFlow protocol to guarantee the completeness and consistency of the messages transmitted between SDN switches and controllers during the communication process.Due to the requirement of reliability and security of OpenFlow, we think that it is of great significance to formally analyze and verify the safety-relevant properties of the mechanism.In this paper, we apply Communication Sequential Processes (CSP) and the model checker Process Analysis ToolKit (PAT) to model and verify the OpenFlow bundle mechanism.Our formalization and verification show that the mechanism can satisfy four properties: deadlock freeness, parallelism, atomicity and order property, from which we can conclude that the mechanism offers a better way to guarantee the completeness and consistency.

The paper investigates a notion of sub asynchronous pi-calculus in asynchronous communication. The emphasises of the research are the basic operation and encoding theory of this novel subcalculus. We focus on behavioural equivalences, accurately on barbed congruence and bisimilarity. The congruence of bisimilarity and characterisation of barbed congruence in sub asynchronous pi-calculus are novel and directly proved. The encoding from pi-calculus to sub asynchronous pi-calculus is validated to be complete and sound. Consequently, the results in this paper bring out theoretical foundations for constructing fully abstract encodings from synchronous to asynchronous.

Named Data Networking (NDN) is a new promising architecture of information-centric networking, which supports multicast of data and adopts the publish/subscribe model in the network. NDN could not reuse the existing routing protocols designed for the IP architecture due to their fundamental difference of design. As a result, the Named-data Link State Routing (NLSR) protocol has been proposed for NDN. At the heart of the NLSR protocol is to disseminate Link State Advertisements (LSAs) to both build a network topology and distribute all the name prefixes to every node in the network. Each router stores the latest version of the LSAs in a Link State Database (LSDB). In this paper, we make the very first attempt to formally model and verify a few fundamental properties of the NLSR protocol using UPPAAL, a model checker for modeling and verifying real-time systems as networks of timed-automata. We validate our model by running the simulator in UPPAAL and verify crucial properties of the protocol under simple yet non-trivial test configurations differing in network topologies and message exchanging scenarios. We capture two situations that may risk synchronization failures and discuss some countermeasures. We also testify the proposal by verifying the revised model with addressing the design issues. We hope that our study and preliminary results would help enhancing the adaptability and robustness of NLSR protocol.

Software Defined Networking (SDN) is an emerging networking paradigm, which provides flexible network programmability and eases the complexity of network control and management. The OpenFlow protocol is the best-known southbound interface of SDN. As the core of a software-defined network, a controller collects topology information of the entire network in order to manage the network as well as provide services to topology-dependent applications. The accuracy of topology information gained by a controller is utmost important. However, most of the mainstream OpenFlow controllers suffer from two kinds of topology poisoning attacks: Link Fabrication Attack and Host Hijacking Attack. TopoGuard is the most famous security extension to traditional OpenFlow controllers, providing detection of the two attacks. In this paper, we model TopoGuard, OpenFlow switches, hosts and two kinds of attackers using Communication Sequential Processes (CSP). Moreover, we encode the proposed model into Process Analysis Toolkit (PAT), a model checker. Finally, we use PAT to verify whether TopoGuard is able to detect the two attacks in some specific scenarios.

Abstract rTiMo is a real-time version of TiMo (Timed Mobility), which is a process algebra for mobile distributed systems. In this paper, we investigate the denotational semantics for rTiMo. A trace variabletris introduced to record the communications among processes as well as the location where the communication action takes place. Based on the formalized model, we study a set of algebraic laws, especially the laws about the migration and communication with real-time constraints. In order to facilitate the algebraic reasoning about the parallel expansion laws, we enrich rTiMo with a form ofguardedchoice. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.

Software-Defined Networking (SDN) is an emerging architecture of computer networking. OpenFlow is considered as the first and currently most popular standard southbound interface of SDN. It is a communication protocol which enables the SDN controller to directly interact with the forwarding plane, which makes the network more flexible and programmable. The promising and widespread use makes the reliability of OpenFlow important. The OpenFlow bundle mechanism is a new mechanism proposed by OpenFlow protocol to guarantee the completeness and consistency of the messages transmitted between SDN devices like switches and controllers. In this paper, we use Communication Sequential Processes (CSP) to formally model the OpenFlow bundle mechanism. By adopting the models into the model checker Process Analysis Toolkit (PAT), we verify the relevant properties of the mechanism, including deadlock freeness, parallelism, atomicity, order property and schedulability. Our formalization and verification show that the mechanism can satisfy these properties, from which we can conclude that the mechanism offers a better way to guarantee the completeness and consistency.

Abstract The POSIX threads (Pthreads) library is a thread API for C/C++ to control parallel threads and spawn concurrent process flows. Programming in Pthreads usually suffers from undesirable deadlock, data race, and race condition problems due to the potential nondeterministic execution behaviors between parallel threads. Dthreads, as another multithreading model that re‐implements Pthreads, was proposed by Liu et al for efficient deterministic multithreading. They found out that, under specific test cases, Dthreads can effectively prevent data races. However, no comparison test has been made with Pthreads. To perform a formal comparison between Pthreads and Dthreads over deadlocks, data races, and race conditions, in this paper, we adopt CSP (communicating sequential processes) as a formal model for specifying part of API functions in Pthreads and Dthreads and illustrate the model construction using 4 classical example programs. By feeding the models into the model checker PAT (process analysis toolkit), we have verified that deadlocks and data races exist in Pthreads, but do not exist in Dthreads, for the considered programs. We have also found that neither of them can prevent race conditions. Our comparative modelling and verification of Pthreads and Dthreads show that though Dthreads cannot prevent all the deadlock situations, shown by verification results of another 2 example programs, Dthreads is better than Pthreads on eliminating data races and preventing deadlocks. Considering limited scalability of Dthreads, we have introduced a new programming model to support coarse granularity in bank transfer. Our modelling is also extended by covering the synchronization operations in Liu et al work.

In safety verification of hybrid systems, barrier certificates are generated by solving the verification conditions derived from non-negative representations of different types. This paper presents a new computational method, sequential linear programming projection, for directly solving the set of verification conditions represented by the Krivine-Vasilescu-Handelman's positivstellensatz. The key idea is to decompose it into two successive optimization problems that refine the desired barrier certificate and those undetermined multipliers, respectively, and solve it in an iterative scheme. The most important benefit of the proposed approach lies in that it is much more effective than the LP relaxation method in producing real barrier certificates, and possesses a much lower computational complexity than the popular sum of square relaxation methods, which is demonstrated by the theoretical analysis on complexity and the experiment on a set of examples gathered from the literature.

Python Software Transactional Memory (PSTM), was proposed to break the limiting factors which restrict diffusion of the TM paradigm into more application fields. Since the widespread use of the PSTM, it is of great significance to formally analyze and verify relevant transactional properties of this architecture. In this paper, we apply Communicating Sequential Processes (CSP) to model the PSTM. Moreover, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for some relevant properties, e.g. ACID. Our modeling and verification show that the PSTM can guarantee some transactional properties.

As one of the most popular software framework for distributed storage of big data, HDFS has lots of good features, such as high throughput and high fault-tolerance. However, with its rapid development, potential data security risks are exposed and founding the security mechanism for HDFS clusters has become an important issue. In this paper, we investigate the identity authentication problem on HDFS and select Kerberos protocol as corresponding security mechanism to deal with the problem. We use the process algebra CSP to model HDFS and HDFS with security mechanism, as well as their security properties. Moreover, we also use a model checking tool PAT to verify these properties. The verification results illustrate the existence of authentication problems on HDFS and Kerberos can effectively solve these problems. Consequently, a better understanding of HDFS and its security properties can be achieved and the establishment of security mechanism for HDFS can benefit from it. Besides, it is also a guide for the formalization of HDFS with security mechanism.

The security protocol is proposed as a security solution for end-to-end communication between smart grid applications in the EU FP7 project C-DAX. Since the importance and widespread use of the security protocol, it is of great significance to formally analyze and verify relevant security properties of this security protocol. In this paper, we apply Communicating Sequential Processes (CSP) to model the security protocol. Further, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for the specification and relevant secure properties, e.g. reachability of the fake goal. Our modeling and verification show that a risk may exist in the security protocol.

Node mobility, as one of the most important features of Wireless Sensor Networks (WSNs), may affect the reliability of communication links in the networks, leading to abnormalities and decreasing the quality of service provided by WSNs. The mCWQ calculus (i.e., CWQ calculus with mobility) is recently proposed to capture the feature of node mobility and increase the communication quality of WSNs. In this paper, we present a proof system for the mCWQ calculus to prove its correctness. Our specifications are based on Hoare Logic. In order to describe the timing of observable actions, we extend the assertion language with primitives. And terminating and non-terminating computations both can be described in our proof system.

IEEE 802.16m, aiming at providing secure communication pathways between the base station (BS) and the mobile station (MS), is a broadband wireless MAN (Metropolitan Area Network) standard. Its security sublayer contains a Privacy Key Management (PKM) protocol, which achieves authentication and key management in the communication process. In this paper, we apply Communicating Sequential Processes (CSP) to formally analyze the latest version of the PKM (PKMv3) protocol. Both communication entities, i.e., the mobile station and the base station, are modelled as processes in our modelling framework. Besides, we introduce intruders in our formalization who have capabilities of intercepting, faking and overhearing. Furthermore, we employ the Process Analysis Toolkit (PAT), a model checker for CSP, to implement the entire model and then verify some non-trivial properties, such as secrecy violation and timeout freedom. With respect to the verification results, we discuss some cases where intruders may take place. Consequently, through our framework, a better understanding of the PKMv3 protocol can be achieved.

In this paper, we present a process algebra for structure-aware mobile systems called BigrTiMo by combining rTiMo process algebra and Bigraph model. Compared with rTiMo model, our BigrTiMo calculus can model not only the location of components but also the connectivity of components. Thus, our BigrTiMo process can communicate not only locally with other process, but also remotely with other process (If they share a communication link). In addition, a BigrTiMo process can migrate from one location to another location, observe the bigraph and change the bigraph. We also investigate the operational semantics and algebraic semantics of the BigrTiMo calculus.

Fault localization is a well-received technique for helping developers to identify faulty statements of a program. Research has shown that the coverages of faulty statements and its predecessors in program dependence graph are important for effective fault localization. However, app executions in Android split into segments in different components, i.e., methods, threads, and processes, posing challenges for traditional program dependence computation, and in turn rendering fault localization less effective. We present RunDroid, a tool for recovering the dynamic call graphs of app executions in Android, assisting existing tools for more precise program dependence computation. For each exectuion, RunDroid captures and recovers method calls from not only the application layer, but also between applications and the Android framework. Moreover, to deal with the widely adopted multi-threaded communications in Android applications, RunDroid also captures methods calls that are split among threads. Demo : https://github.com/MiJack/RunDroid Video : https://youtu.be/EM7TJbE-Oaw

Mobility is a critical issue that must be considered during the modeling and analyzing of a mobile system. At a high abstract level, event-based models can directly specify a mobile system without the introduction of additional mechanisms. In this article, we first propose two types of special events, entering and exiting an ambient, as movement events. Next, based on the movement events, we introduce the notion of a movement path and propose a feasible movement criterion (deciding whether a given movement path of a mobile object (agent) is feasible or not in terms of spatiotemporal topological relationships of ambients). Then, we investigate how a message movement--based communication model represents synchronous communication, asynchronous communication, and broadcast communication in a unified way. Finally, we use movement event sequences to discuss the exclusivity of ambients (an ambient only allows one mobile object to occupy (enter) it at any moment) and show that a priority scheduling control policy can guarantee exclusivity. Accordingly, we propose a correct movement criterion—that is, a correct movement path is feasible and satisfies the exclusivity of ambients. Case studies demonstrate these results.

Model-based engineering has emerged as a key set of technologies to engineer software systems. While system source code is expected to match with the designed model, legacy systems and workarounds during deployment would undoubtedly change the source code, making the actual running implementation mismatch with its model. Such mismatch poses a challenge of maintaining the conformance between the model and the corresponding implementation. Prior techniques, such as model checking and model-based testing, simply assumed the sole correctness of the model or the implementation, which is naive since they both could contain correct information (e.g. representing either the software requirements or the actual running environment).In this paper, we aim to address this problem through model-based continuous verification (ConV), an iterative verification process that links the traditional model checking phase with the software testing phase to a feedback loop, ensuring the conformance between the system model and its implementation. It allows to execute the abstract test cases over the implementation through a semi-automatic binding mechanism to guide the update of the code, and augments system properties from the actually running system to guide the update of the model through model checking. Based on these techniques, we implemented Eunomia, a conformance verification system, to support the continuous verification process. Experiments show that Eunomia can effectively detect and locate inconsistencies both in the model and the source code.

Hadoop Distributed File System (HDFS) is a high fault-tolerant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Since HDFS is widely used, analysis on it in a formal framework is of great significance. In this paper, we use Communicating Sequential Processes (CSP) to model and analyze HDFS. We mainly focus on the dominant parts which include reading files and writing files in HDFS and formalize them in detail. Moreover, we use the model checker Process Analysis Toolkit (PAT) to simulate the model constructed and verify whether it caters for the specification and some important properties, including Deadlock-freeness, Minimal Distance Scheme, Mutual Exclusion, Write-Once Scheme and Robustness.

Swarm robotic system is a complex system comprising a large number of distributed robots. Although a single robot has limited ability of computation and communication, their microscopic behaviors can finally lead to a macroscopic system behavior. Such phenomenon is called emergent behavior which is significantly useful but difficult to engineering due to its indecompositionality over time and scale. In this paper, we propose a formal framework to specify and verify the causality between the macroscopic emergent property and microscopic behaviors of robots. The framework supports hybrid specification of both continuous dynamics of robots and their discrete control programs. A refinement notion is defined in this framework which provides a formal development and verification approach to guide the design of a swarm robotic system satisfying expected emergent properties. We demonstrate the framework on a simple robot swarm consensus scenario.

In viewing the common unreliability problem in wireless communications, the CWQ calculus (a Calculus for Wireless sensor networks from Quality perspective) was recently proposed for modeling and reasoning about WSNs(Wireless Sensor Networks) and their applications from a quality perspective. The CWQ calculus ensures that sensor nodes, even though in an unreliable communication network, can behave in a reasonable manner. Nevertheless, in CWQ calculus, the topological structure is considered at the network level and it is tightly coupled with the processes and other configurations, this may limit its flexibility. In this paper, to make the CWQ calculus more flexible to be able to model and reason about networks of different topological structures, we extend it to be a parametric framework. In the parametric framework, we extract the topological structure of a network and make it to be a configuration such that all topological structure-changes can be captured by this framework. Moreover, in this paper we also develop a SAT-based analysis of the-extended calculus to avoid reaching error configurations due to unreliable communications in WSNs and use the SAT-solver Z3 to check the vulnerability of the whole network. Finally, we give a real-world case study with the scenario of refueling a car to demonstrate the applicability of the extended calculus and the SAT-based analysis.

WiMax (Worldwide Interoperability for Microwave Access, IEEE 802.16) is a standard-based wireless technology, which uses Privacy Key Management (PKM) protocol to provide authentication and key management. Three versions of PKM protocol have been released and the third version (PKMv3) strengthens the security by enhancing the message management. In this paper, a formal analysis of PKMv3 protocol is presented. Both the subscriber station (SS) and the base station (BS) are modeled as processes in our framework. Discrete time describes the lifetime of the Authorization Key (AK) and the Transmission Encryption Key (TEK), which are produced by BS. Moreover, the PKMv3 model is constructed through the discrete-time PROMELA (DT-PROMELA) language and the tool DT-Spin implements the PKMv3 model with lifetime. Finally, we simulate communications between SS and BS and some properties are verified, i.e. liveness, succession and message consistency, which are extracted from PKMv3 and specified using Linear Temporal Logic (LTL) formulae and assertions. Our model provides a basis for further verification of PKMv3 protocol with time characteristic.

Abstract As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It also has real-time and shared-variable features. Previously we have studied an operational semantics for SystemC Peng et al. (An operational semantics of an event-driven system-level simulator, pp 190–200, 2006 ) and bisimulation has been introduced based on some aspects of reasonable abstractions. The denotational method is another approach to studying the semantics of a programming language. It provides the mathematical meaning to programs and can predict the behaviour of programs. Due to the novel features of SystemC, it is challenging to study the denotational semantics for SystemC. In this paper, we applyUnifying Theories of Programming(abbreviated asUTP) Hoare and He (Unifying theories of programming, 1998 ) in exploring the denotational semantics. Two trace variables are introduced, one to record the state behaviours and another to record the event behaviours. The timed model is formalized in a threedimensional structure. A set of algebraic laws is explored, which can be proved via the presented denotational semantics. In this paper, we also consider the linking between denotational semantics and algebraic semantics. The linking is obtained by deriving the denotational semantics from algebraic semantics for SystemC. A complete set of parallel expansion laws is explored, where the location status of an instantaneous action is studied. The location status indicates an instantaneous action is due to which exact parallel component. We introduce the concept of head normal form for each program and every program is expressed in the form of guarded choice with location status. Based on this, the derivation strategy for deriving denotational semantics from algebraic semantics is provided.

The traditional research on scheduling focuses on task scheduling and schedulability analysis in concurrent reactive systems. In this article, we dedicate ourselves to event-based scheduling. We first formally define an event-based scheduling policy and propose the notion of the correctness of a scheduling policy in terms of weak termination. Then we investigate the correctness of the decomposition of scheduling controls and finally obtain a decentralized scheduling method. The method can automatically decompose the scheduling policies of a concurrent reactive system into atomic scheduling policies. Every atomic scheduling policy corresponds to one subsystem. Each of the subsystems is a completely independent system, which may be developed and deployed independently. An experiment demonstrates these results that may help engineers to design correct and efficient schedule policies for a concurrent reactive system.

In the design of dependable software for real-time and embedded systems, the quantitative analysis of program behavior and system performance is a crucial but extremely difficult issue, the challenge of which is exacerbated due to the random city and nondeterminism of interrupt events and the corresponding handling behaviors. Moreover, time analysis is also need to be taken into account for such kinds of systems. Thus the research on a theory which integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we propose an interrupt modeling language pIML including the probabilistic feature to describe the programs with interrupts. We explore a probabilistic operational semantics to depict the actions of pIML. Meanwhile, we also implement this operational semantics we proposed on Maude platform, which fill the gap between the theory and practice. Maude supports rewriting logic, equational logic, and etc. The rewrite rules of rewriting logic can very well implement the transition rules of probabilistic operational semantics. Based on this implementation, it is very convenient to simulate the program written in pIML and analyze the behaviors of program in the presence of interrupts quantitatively.

As one of the most interesting features of mobile ad hoc networks (MANETs), mobility may significantly affect the performance of network protocols. Realistic mobility models are not only decided by individual node movements, but also depend on node coordinations, such as group mobility. In this paper, we propose a process calculus for MANETs in which the motion path of a node is determined by both group mobility models and relative mobility models based on the reference point of the group it belongs to. Due to most of MANETs protocols are evaluated by simulation, a parametric framework is introduced to describe the mobility patterns, which can be used in the network simulation. Moreover, we develop an operational semantics to enable transitions in which the nodes may change their mobility patterns as computation proceeds or delay for some time, and we also give some semantic properties of our calculus based on these semantic rules. A weak bisimulation is provided to investigate the behavioral equivalence of the networks. Finally, a real-world case study about wireless hierarchical routing protocol with group mobility (WHIRL) is given to illustrate the applicability of our calculus.

Virtualization is fundamental to cloud computing. It allows abstraction centred on services and isolation of lower level functionalities and underlying hardware. Modeling, analyzing and verifying cloud systems necessarily involve virtualization and services. However, there exist few efforts to effectively formalizing virtualization in cloud computing. In this paper, based on services we present an approach for defining virtualization. We discuss some properties of service virtualization under some operations and the correctness of virtual services (virtual services without abnormal behavioral problems). Moreover, we investigate automatic configuration of a service based on virtualization, that is, given a virtualized service, how can we automatically obtain all possible correct virtual services of such a service? The configuration process is to first separate a virtualized service into atomic and correct virtual services and then merge these atomic virtual services into all possible correct virtual services of such a virtualized service. The obtained theoretical results help to formally analyze, verify and configure cloud systems.

As one of the most practical protocols, Time-Triggered CAN protocol (TTCAN), which is time triggered to ensure the real-time capability required by embedded systems, has been widely used in the automotive electric system development. In this paper, we present a formal model of the TTCAN protocol using Timed Communicating Sequential Processes (Timed CSP). All the components in the protocol are abstracted as CSP processes, thus the basic transmission in TTCAN is converted into the communication between different CSP processes. Besides, an error handling model is also proposed to capture the exception in the protocol. Finally, we use model checker Process Analysis Toolkit (PAT) to verify whether we can achieve model caters for some properties, which are specified using Linear Temporal Logic (LTL) formulas. Based on the verification results, our TTCAN model turns out to match the specification.

Abstract A very simple model for train stopping is used as a vehicle for investigating how the development of a control system, initially designed in the continuous domain and subsequently discretized, can be captured within a formal development process compatible with standard model based refinement methodologies. Starting with a formalized requirements analysis using KAOS, an abstract model of the continuous system is created in the ASM formalism. This requires extensions of the KAOS and ASM formalisms, capable of dealing with quantities evolving continuously over real time, which are developed. After considering how the continuous system, described as a continuous control system in the state space framework, can be discretized, a discrete control system is created in the state space framework. This is re-expressed in the ASM formalism. The rigorous results on the relationship between continuous and discrete control system models that are needed to establish provable properties of the discretization, then become the ingredients of a retrenchment between continuous and discrete ASM models, and are thus fully integrated into the formal development. The discrete ASM model can then be further refined towards implementation.

The cardiac pacemaker system, proposed as a problem topic in the Verification Grand Challenge, offers a range of difficulties to address for formal specification, development, and verification technologies. We focus on the sensing problem, the question of whether the heart has produced a spontaneous heartbeat or not. This question is plagued by uncertainties arising from the often unpredictable environment that a real pacemaker finds itself in. We develop a time domain tracking approach to this problem, as a complement to the usual frequency domain approach most frequently used. We develop our case study in the continuous ASM (Abstract State Machine) formalism, which is briefly summarised, through a series of refinement and retrenchment steps, each adding new levels of complexity to the model.

Web services have become more and more important in these years. It is of key importance for enterprise web applications to combine different services available to accomplish complex business process. BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. We have already studied the semantics for BPEL, including the operational semantics, algebraic semantics and their linking theory. This paper considers the mechanical approach to linking the operational semantics and algebraic semantics for BPEL. Our approach is to generate operational semantics from algebraic semantics, and to use equational and rewriting logic system Maude to mechanize the linking between the two semantics. Firstly, we investigate the algebraic laws in the Maude approach. Based on the algebraic semantics, the generation of head normal form is explored. Secondly, we consider the Maude approach to deriving the operational semantics from algebraic semantics, where the derivation strategy is based on the concept of head normal form. Our mechanical approach using Maude can visually show the head normal form of each program, as well as the execution steps of a program based on the derivation strategy. Finally, we also mechanize the derived operational semantics. The results mechanized from the second and third exploration indicate that the transition system of the derived operational semantics is the same as the one based on the derivation strategy.

Web services have become more and more important in these years. It is of key importance for enterprise web applications to combine different services available to accomplish complex business processes. BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. We have already studied the semantics for BPEL, including the operational semantics, algebraic semantics and their linking theory. This paper considers the mechanical approach to linking the algebraic semantics and operational semantics for BPEL. Our approach is to generate operational semantics from algebraic semantics, and to use equational and rewriting logic system Maude to mechanize the linking between the two semantics. Firstly, we investigate the algebraic laws in the Maude approach. Based on the algebraic semantics, the generation of head normal form is explored. Secondly, we consider the Maude approach to deriving the operational semantics from algebraic semantics, where the derivation strategy is based on the concept of head normal form. Our mechanical approach using Maude can visually show the head normal form of each program, as well as the execution steps of a program based on the derivation strategy.

Wireless systems have a wide range of applications recently. To explore complex features of such systems, formalisms are proposed to specify and reason about them. This paper presents a case study of routing protocol in wireless networks. We formalize the route discovery process of AODV routing protocol using Object-Z. Network topology and local variables of nodes are defined by relations and functions. The broadcast communication is modelled by operations which change local variables of the sender and all of its connected receivers simultaneously. We show the proof of loop freedom property for established routes based on the specification. Further, the specification is modified by adding mobility of nodes and loop freedom under a dynamic network topology is discussed, showing the scalability of our approach.

Mobile Ad-hoc Networks (MANETs) are increasingly deployed in infrastructureless scenarios. Routing protocol is a crucial solution for MANETs to establish network connections. This paper presents a formal description of the AODV routing protocol and analyzes its properties using relyguarantee method. In our approach the network is specified as a shared variable concurrent program, where communication is modelled by assignment on shared variables. Each parallel component of this program is a specification of route discovery process. The rely-guarantee method allows us to express and verify properties of the protocol on the basis of specifications of its constituent components.

The AUTOSAR (AUTomotive Open System ARchitecture) is an open standard in automotive industry, aiming at unifying the methodology of the automotive software development. It is drawing increasing attention because of its great concern about the safety of automotive electronics. The safety of automotive electronics greatly depends on the Operating System (OS) components, which fully implement the functionality part of automotive applications. However, taking the complex timing protection mechanism of AUTOSAR OS and random occurrences of interrupt requests (IRs) into consideration, it is hard for the developers to design and configure the OS components correctly or even reconcilably. In this paper, we focus on the timing properties and propose an automatic verification framework, in which developers could analyze the timing behaviors and devise the OS components configuration. Furthermore, three important timing properties are expressed and can be verified in our framework, namely, schedulability, non-fault-propagation, and consistency. As a reduced version of AUTOSAR OS and auxiliary analysis modules have been implemented based on Real-Time Maude, developers could easily employ the tool to experiment with different configurations of OS components.

For hybrid systems, hybrid automata based tools are capable of verification while Matlab Simulink/Stateflow is proficient in simulation. In this paper, a methodology is developed in which the formal verification tool PHAVer and simulation tool Matlab are integrated to analyze and verify hybrid systems. For application of this methodology, a Platform Screen Doors System (abbreviated as PSDS), a subsystem of the subway, is modeled with formal verification techniques based on hybrid automata and Matlab Simulink/Stateflow charts, respectively. The models of PSDS are simulated by Matlab and verified by PHAVer. It is verified that the sandwich situation can be avoided under time interval conditions. We conclude that this integration methodology is competent in verifying Platform Screen Doors System.

Interrupt mechanism is indispensable in embedded software due to lots of factors such as switching context and enhancing efficiency. In this context, the traditional way to ensure the correctness of software will not remain in force. Having the interrupt is envolved, the complicated and nondeterminism environment should be taken into consideration during the verification process. In this paper, we propose a novel way to verify the interrupt safety properties based on low-level binary code. At first, an Abstract xBIL is transformed from the xBIL with the time and interrupt properties reserved. xBIL [1] is a binary intermediate language we proposed to represent the machine instructions on multiple architectures. Afterwards, we present an automatic way to construct the Discrete-Time Markov Chains [2] from the Abstract xBIL code. After that, the properties can be easily generated and quantitative analysis could be performed. To prove the feasibility of our approach, we have applied our method to the verification of a commercial automotive operating system and it is proved to be of great help with the development of software.

Cyber-physical systems integrate information and communication technology functions to the physical elements of a system for monitoring and controlling purposes. The conversion of traditional power grid into a smart grid, a fundamental example of a cyber-physical system, raises a number of issues that require novel methods and applications. In this context, an important issue is the verification of certain quantitative properties of the system. In this paper, we consider a specific Chinese Smart Grid implementation as a case study and address the verification problem for performance and energy consumption. We employ stochastic model checking approach and present our modelling and analysis study using PRISM model checker.

As an automotive industry standard of operating system specification, OSEK/VDX is widely applied in the process of designing and implementing the static operating system and the corresponding interfaces for automotive electronics. It is challenging to explore an effective method to support large-scale correctness verification of OSEK/VDX specification. In this paper, we employ process algebra CSP to describe and reason about a real code-level OSEK/VDX operating system. Thus the whole system is formally modeled as a CSP process which is encoded and implemented in process analysis toolkit (PAT). Furthermore, the expected properties are described and expressed in terms of the first-order logic. The properties are also established and verified in our framework. The result indicates that the whole system is deadlock-free and the scheduling scheme is sound with respect to the specification.

In this paper we present a probabilistic calculus for formally modeling and reasoning about Mobile Ad Hoc Networks (MANETs) with unreliable connections and mobility of nodes. In our calculus, a MANET node can locally broadcast messages to a group of nodes within its physical transmission range. The group probability is also introduced since two distinct nodes within different groups should receive messages from the same sender with different possibilities. Our calculus naturally captures essential features of MANETs, i.e., local broadcast, mobility and probability. Moreover, we give a formal operational semantics of the calculus in terms of the labeled transition system and define the notion of open bisimulation. Finally, we illustrate our calculus with a toy example.

JavaScript as a Web scripting language has been widely used following the fast growth of Internet. Due to the flexible and dynamic features offered by the JavaScript language, it has become a challenging problem to statically reason about code written in JavaScript. As a first step towards building a mechanised verification system for JavaScript, we present, in this paper, an axiomatic verification system for a core subset of JavaScript based on a variant of separation logic. We have also defined a big-step operational semantics with respect to which we have demonstrated the soundness of our verification system.

In this paper, we investigate the μTESLA protocol and analyze its broadcast authentication property using process algebra CSP. All the communication entities of the protocol involving the base station, the sensors and the intruder are modeled as CSP processes respectively. Besides, we also produce a CSP description of the protocol specification in our framework. Our verification result demonstrates the correctness of the protocol and the satisfaction toward the broadcast authentication property.

OSEK/VDX Operating System Specification is a standard in automotive industry with a long history. Dozens of mature industrial operating systems are based on this specification and widely applied in the products of major automotive manufacturers. The verification of the operating system products is always a hard nut to crack. In this paper, we propose a formal specification of OSEK/VDX Operating System based on Hoare Logic, which helps us to get rid of the confusion and ambiguities of the informal specification. In this framework, the formalization of all the Application Programming Interfaces are made. As a case study, we link our framework to the formal verification tool VCC. Some errors are detected in a market-upcoming operating system product based on our framework. We conclude that our framework is feasible in verification of operating system.

The paper completely formalizes the concept of system survivability on the basis of Knight's research in \cite{Knight03}. We present a computable probabilistic model of survivable system which is divided into two layers, i.e. the function and service. The probabilistic refinement is introduced to reason about the survivable system, which is modeled by a probabilistic choice of accepted services with respect to the operating environment. Furthermore, we present an elegant survivability specification and the differences with Knight's related works are discussed. The command-and-control example is also revisited in our framework.

The service choreography gives a global view on the collaboration among a collection of services involving multiple different organizations or independent processes. In this paper, a formal model for service choreography based on WS-CDL language is proposed. This model explores the key concepts related to choreography, such as passing channel, fault handling and finalization mechanisms. This study brings us the insights for the analysis, synthesis and verification of service choreography. For instance, the choreography synthesis is discussed based on our trace semantics achieved.

The web environment creates risks together with benefits for web services. Web services often engage attacks from hackers or anyone having hostile intensions. The behavior of services is often effected by the environment changes which should be included in its specifications. In addition, services usually have some mechanisms provided by the developers to deal with the environment changes, especially attacks. However, common specifications of services seldom contain such information. This paper provides a formal behavioral model based on the service behaviors related to its environments and environment changes. A refinement relation is also provided in the behavior model. This model can form a view to analyze the environment influence to the service and compare them according to their defending mechanisms.

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. We have integrated probability, time and concurrency in one single model (called PTSC), where the concurrency feature is modelled using shared-variable based communication. Meanwhile, we have also explored the link between the operational semantics and algebraic semantics, where our approach was started from algebraic laws via head normal form. This paper considers the animation of the link between operational semantics and algebraic semantics for PTSC. Our approach is by using Prolog as the development language. Firstly we explore the animation of the operational semantics for PTSC. The link of the two semantics is proceeded via the concept of head normal form. Secondly the generation of head normal form is explored, especially the animation of parallel expansion laws. Finally we consider the animation of deriving operational semantics by a provided derivation strategy via head normal form. The results animated from the first and the third exploration indicate that our operational semantics is sound and complete with respect to head normal form (or algebraic laws in general).

Competitions of shared Web resources have been widely concerned today. Under the circumstances of networks, no central supervisor can be implemented, which makes it more complicated to avoid deadlock problems. This paper describes the interactions of Web services and shared web resources using CSP method. Deadlocks can be analyzed based on the formal model.

As a programming model, MapReduce is implied for easier processing and generating large cluster of distributed data sets. We use CSP framework to model MapReduce system through which the parallelization of the computation and the distribution of data across multiple machines can be reflected. Some properties of MapReduce can be verified based on the achieved model.

rCOS, the abbreviation of Refinement Calculus for Object Systems, is designed to present mathematical characterization of essential object-oriented concepts for an object-based language with a rich variety of features including subtypes, inheritance, type casting, dynamic binding and polymorphism. This paper represents an operational semantics for the rCOS language based on labeled transition systems. The result semantics shows the process of how the effects of an rCOS program are produced. It can be a secure guide for the implementation of the rCOS language, which is being carried out by our group. For the purpose of extending verifiability and functionality, a set of auxiliary language features is introduced to the rCOS language. Concurrent execution structure is designed to specify multi-threaded programs. Also the simulation is introduced to specify the observable behaviors of objects, and it can be regarded as the refinement relation defined in denotational domain to some extent.

Different from traditional transactions, a compensable transaction relies on compensations to amend partial execution whenever an error occurs. The compensation is preserved on successful completion of its forward transaction for possibly later use. In this paper, we pay attention to the compositional structure of compensable transactions. Except for sequential and parallel compositions, other useful compositional constructs, such as speculative choice, exception handling, alternative forwarding and programmable compensation, are also investigated. All these constructs are not only devised to describe distinct business flow but also used to enhance the capability for dealing with errors, t-calculus is such a transactional language that involves a variety of primitives for composing compensable transactions in a wise way. We present a clear operational semantics for this language and the corresponding concept of bisimulation is defined, which is used to derive equational laws for compensable transactions.

Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the Web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault handling mechanism. We have considered the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models respectively. In this paper, we consider the inverse work, deriving the operational semantics and denotational semantics from algebraic semantics for BPEL. In our model, we introduce four types of typical programs, by which every program can be expressed as the summation of these four types. Based on the algebraic semantics, the strategy for deriving the operational semantics is provided and a transition system is derived by strict proof. This can be considered as the soundness exploration for the operational semantics based on the algebraic semantics. Further, the equivalence between the derivation strategy and the derived transition system is explored, which can be considered as the completeness of the operational semantics. Finally, the derivation of the denotational semantics from algebraic semantics is explored, which can support to reason about more program properties easily.

The Web Services Choreography Description Language (WS-CDL) is a newly developed specification for Web services composition to describe the observable behavior across multiple participants from a global perspective. However, this specification does not provide a formal semantics, whose informal description can lead to ambiguous understanding and different implementations. Hence, it causes difficulties for the engineering community to analyze the business behavior and ensure the correctness. In this paper, we present the semantics of WS-CDL in terms of process algebra CSP which has great advantages in designing and verifying concurrent processes. Therefore, all the properties we want to check within a WS-CDL document can be verified automatically in the CSP framework correspondingly. In addition, the exception and compensation handling mechanism, an important concept of long running transactions, is demonstrated clearly through our formalization work.

Nowadays the B/S (browser/server) architecture has become one of the most popular approaches to implement the Web service. Because of the instability of the Web environment, keeping the consistency of the data is of essential importance. Consequently we turn to formal methods intending to avoid inconsistencies in the B/S architecture. This paper describes a service-oriented system with the B/S architecture using the CSP (communicating sequential processes) method. We define the processes in the system and the behaviors of them. After the definition, we analyze the causes of inconsistencies and demonstrate that the formal definition and mechanism we made can implement an inconsistency free system, which means the inconsistency can be avoided or fixed.

Referring to the design and implementation of large service oriented systems, two different approaches, choreography and orchestration, need to be concerned and studied. Choreography is a specification protocol defining a global picture of the way services interact with each other. Whereas orchestration is a local view focusing on the behavior of a single service. A critical issue, the so called conformance problem, is to validate whether a specific orchestration can play as a participant whose observable behavior is required by a given choreography. In this paper, we introduce two languages for describing choreography and orchestration respectively. Based on the two languages, we give a definition of endpoint projection which is used for automatic generation of orchestrations. Therefore, conformance validation is reduced to verification of process refinement between two orchestrations. Further, we mention that not all choreography models can be locally implementable. In other words, some global models cannot be translated into sets of orchestrations satisfying the global behavioral rules. To ensure that a choreography model is locally implementable, some conditions are required to be satisfied. As a consequence of our work, the skeleton codes for service implementations can be automatically generated, on the other hand, the interoperability between collaborating services is guaranteed.

In the paper, we proposed a language called BPEL0 with its formal semantics as the foundations of WSBPEL. In this paper, we follow the way Van der Aalst proposed on pattern analysis in workflow languages (2003), and present the patterns for BPEL0. Moreover, the expressiveness of BPEL0 is also embodied by means of putting these patterns in the program environment composed of other programming operators. Those properties about the patterns with its environment are captured by the algebraic laws, which can be proven in the framework of BPEL0 semantic domain.

As a system-level modelling language, SystemC possesses some new and interesting features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It is challenging to formalise SystemC. In this paper, we first select a kernel subset of SystemC and study its operational semantics. Based on the operational semantics we define a bisimulation relation, from which program equivalence is explored. Finally, we present a set of algebraic laws for the subset language, which can be proved based on the operational semantics model via bisimulation

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. In this paper, we integrate probability, time and concurrency in one single model, where the concurrency feature is modelled using shared-variable based communication. The probability feature is represented by a probabilistic nondeterministic choice, probabilistic guarded choice and a probabilistic version of parallel composition. We formalize an operational semantics for such an integration. Based on this model we define a bisimulation relation, from which an observational equivalence between probabilistic programs is investigated and a collection of algebraic laws are explored. We also implement a prototype of the operational semantics to animate the execution of probabilistic programs

This paper presents the derivation of an operational semantics from a denotational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build equivalence between the operational and denotational semantics. We propose a discrete denotational semantic model for Verilog. A phase semantics is provided for each type of transition in order to derive the operational semantics.