In previous work, we have proposed an efficient technique, using local analysis, to ensure livelock freedom of CSP systems modelled in the context of a component model, BRIC, with asynchronous compositions. Applicability of this analysis, however, imposed strong restrictions on the CSP models. In this paper, we propose a significantly more elaborate technique for establishing livelock freedom of BRIC components. We present new definitions for our local conditions to deal with asynchronous models, as well as parametrised recursive processes, and establish the soundness of this new approach. Finally, we use an implementation of our technique to demonstrate its effectiveness. We compare the performance of our approach with that of two other techniques for livelock-freedom verification, namely, FDR4 and SLAP, and demonstrate that our approach affords significant gains.

We dedicate this paper with great respect and friendship to He Jifeng on the occasion of his 80th birthday. Our research group owes much to him. The authors have over 150 publications on unifying theories of programming (UTP), a research topic Jifeng created with Tony Hoare. Our objective is to recount the history of Circus (a combination of Z, CSP, Dijkstra’s guarded command language, and Morgan’s refinement calculus) and the development of Isabelle/UTP. Our paper is in two parts. (1) We first discuss the activities needed to model systems: we need to formalise data models and their behaviours. We survey our work on these two aspects in the context of Circus. (2) Secondly, we describe our practical implementation of UTP in Isabelle/HOL. Mechanising UTP theories is the basis of novel verification tools. We also discuss ongoing and future work related to (1) and (2). Many colleagues have contributed to these works, and we acknowledge their support.

Despite the existence of new technologies, relay-based electrical circuits are still used in the majority of the Railway Interlocking Systems installations. Due to their safety-critical aspects, these systems must be safety-proved before their implementation and use. Although the railway standards strongly recommend the use of Formal Methods for the specification and proof of these systems, the literature is scarce in this regard. This article presents the results of using a process-based language, CSP, for the specification of the relay-based Railway Interlocking Systems. Differently from other approaches, our methodology allows the specification of transient states. As a result, it is possible to perform a stronger verification, including an investigation about the existence of state succession cycles, which are dangerous in such systems. An electrical circuit example with such problem is discussed and specified, demonstrating the need of our methodology for the safety proof of these systems.

This work proposes a multidimensional approach for analyzing the routing problem to determine the best routes considering data related to different domains of a city. The proposed strategy defines (i) a quality function for each considered dimension to evaluate the route quality and (ii) a utility function that simultaneously considers the different dimensions by weighting each of them at the decision maker's choice. The approach was implemented on a georeferenced smart city platform that integrates data from several city domains. As proof of concept, the platform is used to combine routing and public safety data and indicates the best routes according to these criteria.

The complexity of development and analysis is inherent to systems in general, especially in concurrent systems. When working with critical systems this becomes much more evident, as inconsistencies are usually associated with a high cost. Thus, the sooner we can identify an inconsistency in the design of a system and remove it, the lower its cost. For this reason, it is common to use strategies to reduce the difficulty and problems faced in this process. One of these strategies is the use of formal methods, which can, for instance, make use of process algebras to specify and analise concurrent systems, improving its understanding and enabling the identification of eventual concurrency problems and inconsistencies even in the initial stages of the project, ensuring the accuracy and correction of the system specification. This article presents a strategy for automatically translating the main operators of the process algebra CSP (Communicating Sequential Processes) into the VHSIC hardware description language (VHDL). The former is a language that allows us to make a formal description of a concurrent system and the latter is a hardware description language that can be compiled on a Field Programmable Gate Arrays (FPGA) board. Our automatic translator is validated by a case study of a smart elevator control system. We present its formal specification in CSP and then its translation into VHDL code, generated by our tool, which we synthesised on an FPGA board.

The CLEARSY Safety Platform (CSSP) was designed to ease the development of safety critical systems and to reduce the overall costs (development, deployment, and certification) under the pressure of the worldwide market. A smart combination of hardware features (double processor) and formal method (B method and code generators) was used to produce a SIL4-ready platform where safety principles are built-in and cannot be altered by the developer. Summarizing a 5-year return of experience in the effective application in the railways, this article explains how this approach is a game-changer and tries to anticipate the future of this platform for safety critical systems. In particular, the education of future engineers and the seamless integration in existing engineering processes with the support of Domain Specific Languages are key topics for a successful deployment in other domains. DSL like Robosim to program mobile robots and relay circuits to design railway signalling systems are connected to the platform.

We propose inheritance and refinement relations for a CSP-based component model (BRIC), which supports a constructive design based on composition rules that preserve classical concurrency properties such as deadlock freedom. The proposed relations allow extension of functionality, whilst preserving behavioural properties. A notion of extensibility is defined on top of a behavioural relation called convergence, which distinguishes inputs from outputs and the context where they are communicated, allowing extensions to reuse existing events with different purposes. We mechanise the strategy for extensibility verification using the FDR4 tool, and illustrate our results with an autonomous healthcare robot case study.

Software architecture description languages (ADLs) currently adopted by industry for software-intensive systems are largely semi-formal and essentially based on SysML and specialized profiles. Despite these ADLs allow describing both structure and behavior of the architecture, there is no guarantee regarding the satisfaction of correctness properties. Due to their nature, semi-formal ADLs do not support automated verification of the specified properties, in particular those related to safety and liveness of the specified behavior. This paper proposes a novel approach for empowering SysML-based ADLs with formal verification support founded on model checking. It presents (i) how the semantics of SysADL, a SysML-based ADL, can be formalized in terms of the CSP process calculus, (ii) how correctness properties can be formally specified in CSP, and (iii) how the FDR4 refinement checker allows verifying correctness properties through model checking. The automated model transformation from SysADL architecture descriptions to CSP composite processes has been implemented as a plug-in to the Eclipse-based SysADL Studio tool. This paper also describes an application of SysADL empowered with CSP to validate its usefulness in practice.

One of the many different purposes of software architecture descriptions is contributing to an early analysis of the architecture with respect to quality attributes. The critical nature of many software systems calls for formal approaches aiming at precisely verifying if their designed architectures can meet important properties such as consistency, completeness, and correctness. In this context, it is worthwhile investigating the role of architecture descriptions to support the formal verification of software architectures to ensure their quality, as well as how such a process happens and is supported by existing languages and verification tools. To evaluate the research landscape on this subject, we have carried out a systematic mapping study in which we collected and analyzed studies available at the literature on formal verification of architecture descriptions. This work contributes with (i) a structured overview and taxonomy of the current state of the art on this topic and (ii) the elicitation of important issues to be addressed in future research.

The success of component-based techniques for software construction relies on trust in the emergent behaviour of the compositions. Here, we propose an efficient correct-by-construction technique for building livelock-free CSP models. Its verification conditions are based on a local analysis of the shortest event sequences (traces) that represent a recursive behaviour in the CSP model. This affords significant gains in performance in model checking. We evaluate our strategy based on models of the Milner's scheduler and the dining philosophers.

The use of formal methods in software engineering considerably reduces the number of errors throughout system developments by enforcing a rigorous specification and verification before reaching a final implementation. We provide, on this paper, a full and sound Structural Operational Semantics for Circus, a formal notation that combines Z and CSP. Our work lifts the works of Freitas, Cavalcanti and Woodcock by creating rules that deal with any Circus construct. We also provide, on this paper, proof of soundness of the Structural Operational Semantics with the Unifying Theories of Programming (UTP).

In previous work we have presented a CSP based approach for developing component-based asynchronous systems, (mathcal {B}mathcal {R}mathcal {I}mathcal {C}), which guarantees deadlock freedom by construction. It uses CSP to specify the constraints and interactions between the components to allow a formal verification of the composition’s behaviour. Following this work, we also proposed an efficient approach for ensuring livelock analysis by construction. In this work we present a tool that automates the verification of component composition by automatically generating and checking the side conditions imposed by both approaches. The tool also includes a support to (mathcal {B}mathcal {R}mathcal {I}mathcal {C}mathcal {K}), an optimisation of (mathcal {B}mathcal {R}mathcal {I}mathcal {C}), that enriches the components with metadata containing additional useful information, which considerably reduces the costs of the composition verifications.

In previous work we presented a CSP-based systematic approach that fosters the rigorous design of component-based development. Our approach is strictly defined in terms of composition rules, which are the only permitted way to compose components. These rules guarantee the preservation of properties (particularly deadlock freedom) by construction in component composition. Nevertheless, their application is allowed only under certain conditions whose verification via model checking turned out impracticable even for some simple designs, and particularly those involving cyclic topologies. In this paper, we address the performance of the analysis and present a significantly more efficient alternative to the verification of the rule side conditions, which are improved by carrying out partial verification on component metadata throughout component compositions and by using behavioural patterns. The use of metadata, together with behavioural patterns, demands new composition rules, which allow previous exponential time verifications to be carried out now in linear time. Two case studies (the classical dining philosophers, also used as a running example, and an industrial version of a leadership election algorithm) are presented to illustrate and validate the overall approach.

In previous work we have proposed a correct-by-construction approach for building deadlock-free CSP models. It contains a comprehensive set of composition rules that capture safe steps in the development of concurrent systems. In this paper, we extend that work by proposing and implementing a strategy for establishing livelock freedom based on constructive rules similar to those that ensure the absence of deadlock. Our method is based solely on the local analysis of the minimum sequences that lead the CSP model back to its initial state. The effectiveness of our livelock-analysis technique is demonstrated via three case studies. We compare the performance of our approach with that of two other techniques for livelock freedom verification: FDR2 and SLAP.

Throughout the development of concurrent systems, complexity may easily grow exponentially yielding a very complex and error-prone process. By using formal languages like CSP we may simplify this task increasing the level of confidence on the resulting system. Unfortunately, such languages are not executable: the gap between the specification language and an executable program must be solved. In previous work, we presented a tool, csp2hc, that translates a considerable subset of CSP into Handel-C source code, which can itself be converted to produce files to program FPGAs. This subset restricts the use of data structures and CSP hiding. In this paper, we present an extension to csp2hc that includes sequences in the set of acceptable data structures and completely deals with the CSP hiding operator. Finally, we validate our extension by applying the translation approach to a industrial scale case study, the steam boiler.

In this paper we propose inheritance relations for a CSP-based component model (BRIC), which supports a constructive design based on composition rules that preserves desired properties such as deadlock freedom. We enhance this component model with support for extensibility via inheritance. The proposed relations allow extension of functionality, whilst preserving service conformance, which we define by means of a substitutability test. We also establish an algebraic connection between component extensibility and refinement. We illustrate our results by presenting a case study that consists of a bank system incrementally improved by inheritance.

This article presents an analysis of the selection process of students from both private and public high schools in the state of Rio Grande do Norte (Northeast of Brazil), in order to form the first group of the Information Technology technical course of the Metrópole Digital project at the Federal University of Rio Grande do Norte (UFRN).The selection instrument consists of a written exam built on the basis of a set of matrices that depict relevant competences and abilities expected from the students.Data concerning the profile of distribution of performance per exam question are presented, together with empirical evidences of the effectiveness of the proposed competence matrices in the selection process.The correlation very fied among the matrices compounding the instrument and scores in courses, and the instrument as a wholeand scores in courses is moderate to strong (rS = 0.6 and r S = 0.7; p < 0,05).The association between the criterion variables (Average of Performance in the Basic Moduleof courses) and the explicative variables (Total score in the selection instrument (QTot) and each of the five compounding matrices) is moderate (r S =0.51, p = 0.001), and the matrices and QTot are jointly responsible for 25% of the variance of the performance in the basic module.The regression coefficient for matrix 1 is 1.38 (CI of 95% = 1.07-1.68);for matrix 2 it was 0.65 (CI of 95% = 036-0.95);for matrix 3, 1.2 (CI of 95% = 0.92 -1,55); matrix 4 0,76 (CI of 95% = 0.45-1.06);matrix 5 1.08 (CI of 95% = 0.78-1.39).The effects of student-descriptive independent variables on performance in the exam are also presented and discussed, and predictive relationships between performance in the exam and performance in the disciplines of the course are verified.Data collected allow concluding that the instrument of selection proposed fits well the aim of forming a group of students to undertake a technical course in the area of information technology.

Throughout the past decades two schools have been developing formal techniques for correct software development, taking complementary approaches: the model-based approach and the behavioural approach. Combinations of languages from both approaches have also been proposed. The lack of support for refinement of state-rich reactive systems in a calculational style has motivated the creation of Circus, a combination of Z, CSP, and Djikstra’s commmand language. In this paper, we foster the reuse of theoretical results underpinned on CSP to Circus by providing a sound mapping for processes and refinement from Circus to CSP. This mapping is proved sound from an existing link between these languages, established in the Unifying Theories of Programming (UTP). Our results allow analysing Circus specifications with techniques and tools, like FDR2 and PAT, originally developed for CSP. We illustrate the overall approach with a running example.

In distributed computing, the leadership election has been used to distributively designate a node as the central controller (leader) of a network of nodes. The complexity of the algorithm arises due to the unawareness of every node of who the current leader is. After running the algorithm, however, a unique node in the network must be elected as the leader and recognized as so by the remaining nodes. In this paper, using CSP, we formalise the leadership election algorithm used by our industrial partner. Its verification is feasible only due to the use of a pattern based strategy that allows the verification to be carried out in a fully local manner. The pattern used here is novel and a further contribution of the paper. A refinement relation together with predicate abstraction is used to describe pattern conformance. The mechanisation of the behavioural conformance is carried out using FDR.

The development and the economical growth of a State in the sectors of Industry, Commerce (and eCommerce), and services are directly influenced by the investments on Information and Communication Technologies (ICTs). Emergent countries like Brazil have an extremely large deficit in qualified ICTs employees. Furthermore, despite being the 6th economy in the world, Brazil currently still presents a large number of citizens below the poverty line even after a considerable improvement in recent years. In 2006, the Federal University of Rio Grande do Norte (UFRN), developed the Digital Metropolis project, whose main objective is to provide means for the creation of a ICT Development Environment in Rio Grande do Norte, Brazil. Currently, the project’s main supporting activity is the Technical Course on Information Technology. In this paper, we describe the activities involving this course, its results and difficulties so far, and the future challenges we aim to face in a very near future.