1,721,035 research outputs found
The Application of Formal Methods in the Development and Validation of Railway Control Systems
No full textVIBE: Looking for Variability In amBiguous rEquirements
No full textVariability is a characteristic of a software project and describes the fact that a system can be configured in different ways, obtaining different products (variants) from a common code base, accordingly to the software product line paradigm. This paradigm can be conveniently applied in all phases of the software process, starting from the definition and analysis of the requirements. We observe that often requirements contain ambiguities which can reveal an unintentional and implicit source of variability, that has to be detected.To this end we define VIBE, a tool supported process to identify variability aspects in requirements documents. VIBE is defined on the basis of a study of the different sources of ambiguity in natural language requirements documents that are useful to recognize potential variability, and is character-ized by the use of a NLP tool customized to detect variability indicators. The tool to be used in VIBE is selected from a number of ambiguity detection tools, after a comparison of their customization features. The validation of VIBE is conducted using real-world requirements documents.(c) 2022 Elsevier Inc. All rights reserved
Model checking fault tolerant systems
No full textThis paper proposes a modelling approach suitable for formalizing fault tolerant systems, taking into account different fault scenarios. Verification of the properties of such systems is then performed using model checking. A general framework for the formal specification and verification of fault tolerant systems is defined starting from these principles, and experience with its application to two case studies is then presented
From generic requirements to variability
No full textThis paper describes a research activity aiming at extracting variability information from ambiguities and vagueness of generic requirement documents, written in Natural Language. The proposed activity continues a research stream focusing on techniques to extract variability information from requirement documents. Here, we study the introduction of a process able to distinguish structural from functional variability, both in the extracted variability model and in the derived lower-level requirements. The problem is stated with reference to an example, a solution proposal is sketched together with related research questions, and a validation path is envisaged
Formal Description and Validation for an Integrity Policy Supporting Multiple Levels of Criticality
No full textAn Industrial Application for the JACK Environment
No full textJACK, Just Another Concurrency Kit, is a new environment integrating a set of formal verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment proposes several functionalities for the design, analysis and verification of concurrent systems specified using formal methods. In this paper we outline an experience on formal specification of a real railway interlocking system using JACK. Then we verify, by using JACK'S checking capabilities, the correctness of the specification with respect to safety requirements. Our experience shows that the JACK environment can be applied successfully in the verification of real safety critical systems
Formal Validation of Fault-tolerance Mechanisms inside GUARDS
No full textIn 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
Two standards means problems: A case study on formal protocol descriptions
No full textEstelle and LOTOS Formal Description Techniques for protocol specifications are considered as a typical example of incompatibility problems which can arise when two standard are used in the same context.
The aim of this paper is to indicate the sources of possible problems and to show the effects of having incompatible specifications of the same system. A brief discussion follows on some techniques and methods to verify the compatibility between Estelle and LOTOS specifications
A Framework to Evaluate 5G Networks for Smart and Fail-Safe Communications in ERTMS/ETCS
No full textETCS is an European system for high speed trains control and protection within ERTMS, the European standard for rail traffic management system. ERTMS/ETCS implementations use GSM-R for communications. As GSM-R is becoming obsolete, the adoption of more advanced technologies is investigated for next generation trains. New communication systems for railway infrastructures are expected to overcome the limitations of GSM-R, providing enhanced performance and reliability, as well as safety and security functionality to meet the requirements of the future signalling systems, control and users’ applications. While 4G technologies (LTE and LTE-A) are currently tested in a few field trials, railway operators should consider that fifth generation (5G) mobile communications technologies will soon be available. One of the foundational aspects of the 5G architecture is control-plane programmability, achieved through the SDN paradigm. Being aware that in a railway scenario this opportunity can be exploited to dynamically reconfigure the network behavior to better match the communication flows produced by moving trains, we aim at defining a framework, integrating formal modeling and analysis tools and techniques into a network emulator, to evaluate the impact on ERTMS/ETCS safety and security deriving from the adoption of an SDN model in the communication infrastructure. In this paper we describe a first step towards this objective, by presenting a first proof-of-concept implementation of the framework and its use to reproduce a simple railway infrastructure. In our current implementation, Finite State Machines are used to model communication protocols between ERTMS/ETCS entities and to automatically produce code and Promela models. Generated code is directly used to control the network behavior while the Promela model allows to generate and verify a network configuration by model checking
- …
