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.

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.

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.

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.

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.

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.

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.