Search

[EN] Reversibility enables a program to be executed both forwards and backwards. This ability allows programmers to backtrack the execution to a previous state. This is essential if the computation is not deterministic because re-running the program forwards may not lead to that state of interest. Reversibility of sequential programs has been well studied and a strong theoretical basis exists. Contrarily, reversibility of concurrent programs is still very young, especially in the practical side. For instance, in the particular case of the Communicating Sequential Processes (CSP) language, reversibility is practically missing. In this article, we present a new technique, including its formal definition and its implementation, to reverse CSP computations. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. The technique proposes different forms of reversibility, including strict reversibility and causal-consistent reversibility. On the practical side, we provide an implementation of a system to reverse CSP computations that is able to highlight the source code that is being executed in each forwards/backwards computation step, and that has been optimized to be scalable to real systems., A preliminary version of this work was presented at the 12th Conference on Reversible Computation [31]. The authors would like to thank the anonymous reviewers for their useful comments and constructive feedback that helped them to improve this work. This work was supported in part by the EU (FEDER) and the Spanish MCI/AEI under Grant TIN2016-76843-C4-1-R and Grant PID2019-104735RB-C41, in part by the Generalitat Valenciana under Grant Prometeo/2019/098 (DeepTrust), in part by JSPS KAKENHI under Grant JP17H01722, and in part by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA 952215.

There are many paradigms available to address the unique and complex problems introduced with parallel programming. These complexities have implications for computer science education as ubiquitous multi-core computers drive the need for programmers to understand parallelism. One major obstacle to student learning of parallel programming is that there is very little human factors evidence comparing the different techniques to one another, so there is no clear direction on which techniques should be taught and how. We performed a randomized controlled trial using 88 university-level computer science student participants performing three identical tasks to examine the question of whether or not there are measurable differences in programming performance between two paradigms for concurrent programming: threads compared to process-oriented programming based on Communicating Sequential Processes. We measured both time on task and programming accuracy using an automated token accuracy map (TAM) technique. Our results showed trade-offs between the paradigms using both metrics and the TAMs provided further insight about specific areas of difficulty in comprehension.

A statically typed version of the data driven functional parallel computing model is proposed. It enables a representation of dynamically changing parallelism by means of asynchronous serial data flows. We consider the features of the syntax and semantics of the statically typed data driven functional parallel programming language Smile that supports asynchronous sequential flows. Our main idea is to apply the Hoar concept of communicating sequential processes to the computation control on the data readiness. It is assumed that on the data readiness a control signal is emitted to inform the processes about the occurrence of certain events. The special feature of our approach is that the model is extended with the special asynchronous containers that can generate events on their partial filling. These containers are a stream and a swarm, each of which has its own specifics. A stream is used to process data which have identical type. The data comes sequentially and asynchronously at arbitrary time moments. The number of the incoming data elements is initially unknown, so the processing completes on the signal of the end of the stream. A swarm is used to contain independent data of the same type and may be used for the massive parallel operations performing. Unlike a stream, the swarm’s size is fixed and known in advance. General principles of the operations with the asynchronous sequential flows with an arbitrary order of data arrival are described. The use of the streams and the swarms in various situations is considered. We propose the language constructions which allow us to operate the swarms and streams and describe the specifics of their application. We provide the sample functions to illustrate the use of the different approaches to description of the parallelism: recursive processing of the asynchronous flows, processing of the flows in an arbitrary or predefined order of operations, direct access and access by the reference to the elements of the streams and swarms, pipelining of calculations. We give a preliminary parallelism assessment which depends on the ratio of the rates of data arrival and their processing. The proposed methods can be used in the development of the future languages and tool-kits of architecture-independent parallel programming.

Android faces an increasing threat of malware attacks. The few existing formal detection methods have drawbacks such as complex code modeling, incomplete and inaccurate expression of family properties, and excessive manual participation. To this end, this paper proposes a formal detection method, called DroidFDR, for Android malware classification based on communicating sequential processes (CSP). In this method, the APK file of an application is converted to an easy-to-analyze representation, namely Jimple, in order to model the code behavior with CSP. The process describing the behavior of a sample is inputted to an FDR model checker to be simplified and verified against a process that is automatically abstracted from the malware to express the property of a family. The sample is classified by detecting whether it has the typical behavior of any family property. DroidFDR can capture the behavioral characteristics of malicious code such as control flow, data flow, procedure calls, and API calls. The experimental results show that the automated method can characterize the behavior patterns of applications from the structure level, with a high family classification accuracy of 99.06% in comparison with another formal detection method.

The efficient design of safety-critical cyber-physical systems (CPS) requires the co-modeling and -verification of its physics, architecture and functionalities. Existing co-modeling formalisms do not account for these three design aspects into account uniformly. AADL is a precise formalism for modeling architecture and prototyping real-time hardware platforms, but it delegates co-modeling physical and software behaviors to so-called annexes. By contrast, Simulink/Stateflow (S/S) is strong for modeling interacting physical and software behaviors, but weak for modeling architecture and hardware platforms. To address this issue, this paper considers the combination of AADL and S/S to co-model CPSs and presents a method to uniformly analyze and verify this combination. AADL ⊕ S/S provides a unified graphical co-modeling environment for CPS design and supports simulation through C code generation. We present a formal semantics of AADL ⊕ S/S by translating it to Hybrid Communicating Sequential Processes (HCSP), which yields a deductive verification framework for AADL ⊕ S/S models based on Hybrid Hoare Logic (HHL). We also prove the correctness of the translation of AADL ⊕ S/S to HCSP. The effectiveness of our approach is illustrated by the realistically-scaled case study of an automatic cruise control system.

In model-driven design of embedded systems, how to generate code from high-level control models seamlessly and correctly is challenging. This is because hybrid systems are involved with continuous evolution, discrete jumps, and the complicated entanglement between them, while code only contains discrete actions. In this article, we investigate the code generation from Hybrid Communicating Sequential Processes (HCSP), a formal hybrid control model, to SystemC. We first introduce the notion of approximate bisimulation as a criterion to check the consistency between two different systems, especially between the original control model and the final generated code. We prove that it is decidable whether two HCSPs are approximately bisimilar in bounded time and unbounded time with some conditions, respectively. For both the cases, we present two sets of rules correspondingly for discretizing HCSPs and prove that the original HCSP model and the corresponding discretization are approximately bisimilar. Furthermore, based on the discretization, we define a transformation function to map a discretized HCSP model to SystemC code such that they are also approximately bisimilar. We finally implement a tool to automatically realize the translation from HCSP to SystemC code and illustrate our approach through some case studies.

As a storage system architecture optimized for Facebook’s photo application, Haystack has four main advantages than before, including high throughput and low latency, fault-tolerance, cost-effectiveness and simplicity. With its widespread use, its validity and other major properties abstracted from the architecture need to be analyzed in a formal framework. However, to the best of our knowledge, there is nearly no research conducted to describe the communications and properties in Haystack. In this paper, we focus on the internal design of serving and uploading a photo of Haystack architecture and apply Communicating Sequential Processes (CSP) to formalize them in detail. By feeding the models into the model checker Process Analysis Toolkit (PAT), we have verified some crucial properties, including basic property and supplementary properties. Basic property contains Deadlock Freedom. Supplementary properties include synchronous concurrent access, asynchronous concurrent access, synchronous concurrent access with the same client, synchronous concurrent upload and synchronous concurrent upload with the same client. Finally, according to the verification results, we believe that from the CSP’s perspective, the properties of Haystack architecture is valid, which means that it meets the requirements of the documents of Facebook.

This paper presents the ontology of the concurrent processes close to Hoare communicating sequential processes. It is a part of an intellectual system for supporting verification of behavioral properties of such processes. Our ontological representation of the processes is oriented both to the application of formal verification methods and to the extraction of information from technical documentation (by our previously developed system of information extraction from a natural language text). We describe the ontology classes and domains that define communicating concurrent processes. These processes are characterized by sets of local and shared variables, a list of actions on these variables which change their values, a list of channels for the process communication (which, in turn, are characterized by the type of reading messages, capacity, modes of writing and reading, and reliability), and also a list of communication actions for sending messages. In addition to the formal mathematical definition of classes and domains of the ontology, examples of descriptions of some ontological classes, as well as typical properties and axioms for them, are specified in the editor Protege in the OWL language with the use of the inference rules in the SWRL language. We define the formal operational semantics of communicating processes for their ontological representation. This semantics is a labeled transition system. It is reduced to the local operational semantics of separate process instances in the interleaving model. We specialize several types of processes from the subject domain of automatic control systems that model the typical functional elements of the automatic control system (sensors, comparators and regulators), as well as their combinations. The concepts of the specialized ontology are illustrated by the example of a control part of a bottle-filling system.

In this paper, new contributions for model-based testing using Communicating Sequential Processes (CSP) are presented. For a finite non-terminating CSP process representing the reference model, finite test suites for checking the conformance relations traces and failures refinement are presented, and their completeness (that is, capability to uncover conformity violations) is proven. The fault domains for which complete failure detection can be guaranteed are specified by means of normalised transition graphs representing the failures semantics of finite-state CSP processes. While complete test suites for CSP processes have been previously investigated by several authors, a sufficient condition for their finiteness is presented here for the first time. Moreover, it is shown that the test suites are optimal in two aspects: (a) the maximal length of test traces cannot be further reduced, and (b) the nondeterministic behaviour cannot be tested with smaller or fewer sets of events, without losing the test suite's completeness property.

The C.A.R. Hoare’s theory of Communicating Sequential Processes (CSP) is a strong basis for analysis and synthesis of concurrent computer systems. Its manifestation as abstraction, a parallel systems specification language and a parallel programming language is unique. If the absence of a protected address space is ignored, the std::thread class could be regarded near close to CSP process semantics. Unfortunately, in the standard C++ library there is not type even approximately close to CSP channel. Hence, the main goal set: proposal of suitable implementation of CSP semantics of inter-process communications through the C++ 11 standard library means in seek of higher degree of structuring of communications of objects of type std::thread. As a result, a compact C++ template library named csp is developed. It encapsulates the means of messaging and synchronization between objects of type std::thread. The csp namespace defined includes csp::chan, csp::mux, csp::sink and csp::forks classes. The csp::chan class is strong implementation of CSP channel semantics, with two methods csp::chan::send() and csp::chan::recv() corresponding to CSP communications commands for output and for input. The CSP alternative command for nondeterministic selection is implemented by the method csp::mux::recv() using multiple wait on std::condition_variable and randomized choice between true guards. By practical reasons, through the additional classes, csp::sink and csp::fork supported the communication schemes and too. The code of the developed library and examples of its use are placed in the GitHub under MIT license.

RoboSim is a tool-independent notation for modeling software simulations of robots, and it can be verified by a variety of techniques and tools, including model checking and theorem proving. RoboSim has a formal tock-CSP (Communicating Sequential Processes) semantics, and so refinement checkers, such as FDR, can be used for verification of models. In this paper, we explore the use of UPPAAL, as a well-established tool for verification of time-dependent properties. We propose a model-transformation strategy to translate RoboSim models into NTA (Network of Timed Automata) based on some patterns and mapping rules. We implement our strategy as a plug-in for the RoboSim modeling and verification tool. Using examples, we compare the verification results of UPPAAL and FDR for a series of safety, reachability, and liveness properties. Moreover, we use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our approach can be extended to the verification of stochastic and hybrid systems using UPPAAL SMC. Such an extension cannot be easily conceived for The original tock-CSP semantics of RoboSim.

Apache Kafka is a popular open source and commercially supported distributed publish-subscribe messaging system, which achieves high throughput, low latency and good load balancing. As a widely used messaging system, message delivery between producers and consumers is one of core functions in Kafka, and the reliability and correctness of message delivery are important and concerned. The formal methods can analyze whether it is a highly credible model. Therefore, it is significant to analyze the communication between producers and consumers from the perspective of formal methods. In this paper, we model the communication between producers and consumers in Kafka by the process algebra CSP (Communicating Sequential Processes). Moreover, we also apply the model checking tool PAT (Process Analysis Toolkit) to verify five properties of our system namely Deadlock Freedom, Acknowledgement Mechanism, Parallelism, Sequentiality and Fault Tolerance. The results of verification show the model of message transmission in Kafka messaging system caters for its specification, from which this system can be concluded that it is reliable.

We give an introduction to the MARS toolchain for formal modeling and verification of hybrid systems. It consists of translators from Simulink/Stateflow models to Hybrid Communicating Sequential Processes (HCSP), and tools for simulation, code generation, and deductive verification of an HCSP model. We apply the toolchain to model the descent guidance control phase of the recently launched Tianwen I mars lander, and verify that it correctly controls the velocity of the lander.

With concurrency being integral to most software systems, developers combine high-level concurrency models in the same application to tackle each problem with appropriate abstractions. While languages and libraries offer a wide range of concurrency models, debugging support for applications that combine them has not yet gained much attention. Record & replay aids debugging by deterministically reproducing recorded bugs, but is typically designed for a single concurrency model only. This paper proposes a practical concurrency-model-agnostic record & replay approach for multi-paradigm concurrent programs, i.e. applications that combine concurrency models. Our approach traces high-level nondeterministic events by using a uniform model-agnostic trace format and infrastructure. This enables orderingbased record & replay support for a wide range of concurrency models, and thereby enables debugging of applications that combine them. In addition, it allows language implementors to add new concurrency models and reuse the model-agnostic record & replay support. We argue that a concurrency-model-agnostic record & replay is practical and enables advanced debugging support for a wide range of concurrency models. The evaluation shows that our approach is expressive and flexible enough to support record & replay of applications using threads & locks, communicating event loops, communicating sequential processes, software transactional memory and combinations of those concurrency models. For the actor model, we reach recording performance competitive with an optimized special-purpose record & replay solution. The average recording overhead on the Savina actor benchmark suite is 10% (min. 0%, max. 23%). The performance for other concurrency models and combinations thereof is at a similar level. We believe our concurrency-model-agnostic approach helps developers of applications that mix and match concurrency models. We hope that this substrate inspires new tools and languages making building and maintaining of multi-paradigm concurrent applications simpler and safer.

In this paper, we present the denotational semantics for channel mobility in the Unifying Theories of Programming (UTP) semantics framework. The basis for the model is the UTP theory of reactive processes, precisely, the UTP semantics for Communicating Sequential Processes (CSP), which is extended to allow the mobility of channels—the set of channels that a process can use for communication (its interface), originally static or constant (set during the process's definition), is now made dynamic or variable: it can change during the process's execution. A channel is thus moved around by communicating it via other channels and then allowing the receiving process to extend its interface with the received channel. We introduce a new concept, the capability of a process, which allows separating the ownership of channels from the knowledge of their existence. Mobile processes are then defined as having a static capability and a dynamic interface. Operations of a mobile telecommunications network, e.g., handover, load balancing, are used to illustrate the semantics. We redefine CSP operators and in particular provide the first semantics for the renaming and hiding operators in the context of channel mobility.

Concurrency in evolutionary algorithms allow researchers to leverage the performance of powerful multi-core desktop architectures by parallelizing tasks using a high-level interface. However, concurrency also introduces additional complexity at the model and the implementation level. In this paper we describe how using parallel execution monitoring tools to check the effective parallelism of the implementation, can help to work out some of said complexities at the implementation-level, which in turn, are translated into improvements at the algorithmic-level. The performance gain is noticeable from an evaluations/seconds point of view to the possible scaling that can be achieved in the running machine, up to a superlinear scaling in an off-the-shelf platfonn. We show that the design using communicating sequential processes implemented in the language Raku is the basis for these improvements.

Modern level of dependable systems engineering process organization is tightly interwoven with formal methods application. Those are typically the model checkers, bringing in the automation. Despite the significant developments in this direction, the aspect of formal specifications synthesis automation is still lagging behind. To this end, a technique is proposed, covering the aspects of diminishing the breach between the analytical interpretation of formal specification and its implementation on the basis of the formalism chosen. The technique is grounded on Communicating Sequential Processes calculus, Hoare triples and Temporal Logic of Actions. To prove the technique proposed, a case study, demonstrating the Message Queuing Telemetry Transport protocol specification synthesis, has been conducted.

Demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms for formal modelling. In contrast with its demonic counterpart, in an angelic choice failure is avoided whenever possible. Although it has been extensively studied in refinement calculi, in the context of process algebras, and of the Communicating Sequential Processes (CSP) algebra for refinement, in particular, it has been elusive. We show here that a semantics for an extended version of CSP that includes both demonic and angelic choice can be provided using Hoare and He's Unifying Theories of Programming (UTP). Since CSP is given semantics in the UTP via reactive designs (pre and postcondition pairs) we have developed a theory of angelic designs and a conservative extension of the CSP theory using reactive angelic designs. To characterise angelic nondeterminism appropriately in an algebra of processes, however, a notion of divergence that can undo the history of events needs to be considered. Taking this view, we present a model for CSP where angelic choice completely avoids divergence just like in the refinement calculi for sequential programs.

No doubt, a person of modern society relying on Embedded Systems (ESs) has increased rapidly and the era of digital machines is gaining popularity among users and also systems providers. At the same time, such instruments face substantial security challenges because they usually operate in a physically unprotected environment, and thus attract the attackers to gain unauthorized access for utilizing the system functions. Accordingly, system integrity is important and hence there is a need to propose a technique/tool to verify that the original/pure systems codes have been used in those devices. In this research, our main objective is to design a system architecture with a secure communication for code integrity attestation of an ES. Indeed, the study presents the proposed system architecture for ESs integrity attestation which includes two main phases: fetching an ES code at a server site and examining the ES at a remote site (using a designed user application). Essentially, the hash function (SHA-2) with a random key to calculate a unique digest value for a targeted system have been utilized. Also, the study used timestamps and nonce values, two secure keys, and public key algorithm to design a secure protocol in-order to prevent potential attacks during data and the associated values transfer between the server and the remote user application. As many researchers state that the formal methods are very precise and accurate for presenting system specifications; this study modeled and analyzed the proposed attestation protocol using the Communicating Sequential Processes (CSP) formal method approach. Besides, the Compiler for the Analysis of Security Protocols (Casper) has been used to translate the protocol description into the corresponding process algebra CSP model. Then, the researcher used the Failures Divergences Refinement (FDR) to evaluate the proposed protocol. Those formal method tools are considered as a reliable verification measurement in-order to figure-out potential flaws and correct them. Overall, the final output of checking all the defined secrecy and authentication assertions using FDR 4.2.0, and thus all the secrecy and authentication specifications defined in the developed Casper script are passed.

Software-Defined Networking (SDN) is an emerging networking paradigm that provides flexible network programmability and reduces the complexity of network management and control. OpenFlow Protocol is the best-known southbound interface of SDN. As one of the most popular OpenFlow controllers, Floodlight is famous for its excellent basic modules, which are used by many other mainstream controllers. Due to the popularity and widespread use of the Floodlight’s modules, it is important to analyze them in a formal framework. In this paper, we focus on six modules of Floodlight that are mainly responsible for pushing decisions and discovering topology. In order to verify whether these modules meet two important requirements, including Decision Pushed Correctly and Rule Installed Once, we propose a system model that formalizes these modules as well as hosts and switches using Communicating Sequential Processes (CSP). Moreover, we add two types of attacks: Link Fabrication and Host Hijacking, which aim at poisoning the topology information collected by a controller, to construct a second system model. Finally, we implement these two system models in Process Analysis Toolkit (PAT), a model checker, to verify whether our models cater for four assertions based on two requirements and if Floodlight is vulnerable to these two attacks.