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.

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.

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.

As a variant of Ant Colony Optimization, the EigenAnt algorithm finds the shortest path between a source node and a destination node based on negative feedback in the form of selective pheromone removal that occurs only on the path which is actually chosen for each trip. EigenAnt algorithm also could change quickly to reflect to the dynamic variety of initial pheromone concentrations and path length etc. However, in general, the solution of EigenAnt algorithm is not always convergent. In this paper, we propose an improved EigenAnt (iEigenAnt) algorithm in terms of both negative and positive feedback; that is, selective pheromone updates are decided by smart ants or stupid ones, which depends whether the amount of the pheromone at the selected path increases or not. The system modelled by our algorithm has a unique equilibrium as the shortest path. Besides, using mathematical analysis, we demonstrate that the equilibrium is global asymptotically stable, i.e., stable and convergent. Finally, we also implement the iEigenAnt algorithm under four different cases and apply it on travelling salesman problem problem, the simulation result shows that our iEigenAnt algorithm is faster convergent and more effective compared to the original EigenAnt algorithm, and some combinatorial optimisation problems can be effectively solved based on our iEigenAnt algorithm.

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.

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.

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.

Abstract. We introduce a comparative case study on the application of formal methods and techniques to the Tree Identify Protocol of the IEEE standard 1394 serial multimedia bus. The Tree Identify Protocol makes an ideal subject for this purpose because it is small yet complex, and may be modelled in a variety of ways. We provide an informal explanation of the protocol, describe how the case study was conducted, and give an overview of the results.

An operational semantics of a significant subset of the Verilog hardware description language (HDL) is presented. The semantics is encoded using the logic programming language Prolog in a literate programming style. This allows the associated documentation to be maintained in step with the semantics, and the printed version to be presented in a standard mathematical operational semantics style. It also enables the semantics to be directly animated using a Prolog interpreter. Using this approach allows the exploration of sometimes subtle behaviours of parallel programs and the possibility of rapid changes or additions to the semantics of the language covered that could be missed otherwise. In addition, it provides and extra check on the validity of the operational semantics.

Abstract Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category called rely-guarantee (or assumption-commitment) , in which a specification is explicitly (syntactically) split into two corresponding parts. This paper summarises existing work on the rely-guarantee method and gives a systematic presentation. A proof system for partial correctness is given first, thereafter it is demonstrated how the relevant rules can be adapted to verify deadlock freedom and convergence. Soundness and completeness, of which the completeness proof is new, are studied with respect to an operational model. We observe that the rely-guarantee method is in a sense a reformulation of the classical non-compositional Owicki & Gries method, and we discuss throughout the paper the connection between these two methods.