Modelling and Validating a multiple-configuration railway signalling system using SDL

This paper discusses some issues about the usage of SDL and related commercial SDL support tools for the validation of a railway signalling system: in particular, the issue of the multiple configurations presented by this system is addressed, discussing the possible strategies to validate the system regardless to the actual configuration.     

Formalizing REST APIs for web-based communication and SIP interworking

This paper proposes an instantaneous recovery route design scheme using multiple coding-aware link protection scenarios to achieve higher link cost reduction in the network. In this scheme, two protection scenarios, namely, (i) traffic splitting (TS), and (ii) two sources and a common destination (2SD) are used to integrate multiple sources and a common destination. The proposed scheme consists of two phases. In the first phase, the proposed scheme determines routes for 2SD and TS scenarios of all possible source-destination pairs to minimize the total link cost. In this phase, the network coding is applied to the common path within each scenario, individually. In the second phase, network coding is applied to the common path between two scenarios (or a scenario pair) in order to enhance the resource saving. This phase develops conditions that select the most appropriate combination of scenario pairs, such as TS–TS, 2SD–2SD, and 2SD–TS for network coding, including their proofs. Using these conditions, a heuristic algorithm is introduced in order to select the most appropriate combination of scenario pairs for further enhancing of resource saving. Simulation results show that the proposed scheme outperforms the conventional 1 + 1 protection scheme, the TS scenario, and the 2SD scenario in terms of link cost reduction in the network.     

Formal methods for railway control systems

The term intelligent transportation systems (ITS) refers to information and communication technology (applied to transport infrastructure and vehicles) that improve transport outcomes such as transport safety, transport productivity, travel reliability, informed travel choices, social equity, environmental performance and network operation resilience. The importance of ITS is increasing as novel driverless/pilotless applications are emerging. This special issue addresses the application of formal methods to model and analyze complex systems in the context of ITS and in particular in the field of railway control systems. In fact, modelling and analysis activities are very important to optimize system life-cycle in the design, development, verification and operational stages, and they are essential whenever assessment and certification is required by international standards.     

Model checking for action-based logics

A model checker is described that supports proving logical properties of concurrent systems. The logical properties can be described in different action-based logics (variants of Hennessy-Milner logic). The tools is based on the EMC model checker for the logic CTL. It therefore employs a set of translation functions from the considered logics to CTL, as well as a model translation function from labeled transition systems (models of the action-based logics) to Kripke structures (models for CTL). The obtained tool performs model checking in linear time complexity, and its correctness is guaranteed by the proof that the set of translation functions, coupled with the model translation function, preserves satisfiability of logical formulae.     

Formal validation of fault-tolerance mechanisms inside GUARDS

In this paper we report the experiments carried out during the specification and validation of the fault-tolerance mechanisms developed in the European project Generic Upgradable Architecture for Real-time Dependable Systems (GUARDS). These mechanisms are the components of an architecture developed for embedded safety-critical systems. The validation approach is based on model-checking techniques and exploits the verification methodology supported by the Just Another Concurrency Kit (JACK) environment. The properties that guarantee the desired behaviour of the mechanisms are specified as temporal logic formulae; the JACK model-checker is then used to verify that the behaviour of the mechanisms satisfy such properties also in the presence of faults.     

Distributed implementation of nested communicating sequential processes: Communication and termination

A model for the distributed implementation of CSP programs, based on cooperation between communicating virtual processors, is defined. Emphasis is placed on the relations between nested parallel commands, communication, and process termination. We then present a protocol for process termination handling that guarantees the consistency of distributed structures and aims at optimizing the rate of communications among virtual processors. Finally, the adoption of the model in the implementation of the run-time support of a CSP-based language on the MuTEAM distributed multiprocessor is described.     

A Formal Verification Environment for Railway Signaling System Design

A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems.This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.     

A state/event-based model-checking approach for the analysis of abstract system properties

We present the UMC framework for the formal analysis of concurrent systems specified by collections of UML state machines. The formal model of a system is given by a doubly labelled transition system, and the logic used to specify its properties is the state-based and event-based logic UCTL. UMC is an on-the-fly analysis framework which allows the user to interactively explore a UML model, to visualize abstract behavioural slices of it and to perform local model checking of UCTL formulae. An automotive scenario from the service-oriented computing (SOC) domain is used as case study to illustrate our approach.     

Detecting requirements defects with NLP patterns: an industrial experience in the railway domain

In the railway safety-critical domain requirements documents have to abide to strict quality criteria. Rule-based natural language processing (NLP) techniques have been developed to automatically identify quality defects in natural language requirements. However, the literature is lacking empirical studies on the application of these techniques in industrial settings. Our goal is to investigate to which extent NLP can be practically applied to detect defects in the requirements documents of a railway signalling manufacturer. To address this goal, we first identified a set of typical defects classes, and, for each class, an engineer of the company implemented a set of defect-detection patterns by means of the GATE tool for text processing. After a preliminary analysis, we applied the patterns to a large set of 1866 requirements previously annotated for defects. The output of the patterns was further inspected by two domain experts to check the false positive cases. Additional discard-patterns were defined to automatically remove these cases. Finally, SREE, a tool that searches for typically ambiguous terms, was applied to the requirements. The experiments show that SREE and our patterns may play complementary roles in the detection of requirements defects. This is one of the first works in which defect detection NLP techniques are applied on a very large set of industrial requirements annotated by domain experts. We contribute with a comparison between traditional manual techniques used in industry for requirements analysis, and analysis performed with NLP. Our experience shows that several discrepancies can be observed between the two approaches. The analysis of the discrepancies offers hints to improve the capabilities of NLP techniques with company specific solutions, and suggests that also company practices need to be modified to effectively exploit NLP tools.