The combination of edge and cloud brings new opportunities and challenges to the data placement problem. Expanding from cloud to edge allows data to be placed closer to user, which relieves bandwidth pressure on cloud and reduces latency. Factors such as varying request preferences and regional correlations are becoming increasingly evident. However, they are largely ignored by existing methods. To this end, we combine the distribution of user requests and server location to construct a spatial distribution vector of the request and propose a data placement strategy based on it. Within edge-cloud environment, the proposed strategy can adapt to different request distributions and place data in a targeted manner. Considering the impact of data volume, we assign different weights for placing data on different servers and update them dynamically in response to request fulfillment. To address the imbalance in requests and data volume in network traffic composition, we analyze the similarity of some data request distribution through the vectors, and co-place the data with high similarity to satisfy user demands. Through experiments on real base station distributions and Foursquare dataset, our proposed method reduces the latency by 17.98% to 38.72% and the log ratio of total cost ranges from 0.13 to 0.30 compared to SOTA algorithms.

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.

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.

Linear Temporal Logic over finite traces, or LTL f , is a popular logic to describe specifications with finite behaviors in AI scenarios such as motion planning.Satisfiability is one of the fundamental problems of LTL f and extensive studies have been conducted to speed up the process to check whether a given LTL f formula is satisfiable.This paper presents a new approach, namely LSCFP, to solve the problem of LTL f satisfiability checking by leveraging the formula progression technique.Compared to previous work, LSCFP utilizes formula progression to gather more information propagated along with the search path such that it can find satisfiable models more quickly if the input formula is satisfiable.A comprehensive experimental evaluation has been conducted to show the efficiency of LSCFP, and the results suggest that LSCFP is able to gain at least 15% performance improvement on checking satisfiable formulas when compared to the state-of-the-art LTL f satisfiability checker aaltaf.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.