The quality of a system depends on the degree to which it fulfills its requirements. Requirements traceability is broadly recognized as a crucial element of any rigorous system development process, especially for the design of critical complex systems. The paper proposes a model-based approach to support traceability by defining several kinds of alignment links between requirements models and high-level architecture models. We have already defined these models using a combination of graphical notations based on SysML and the formal method Event-B, hence alignment links are first graphically specified by refining the Dependency concept of SysML. Then they are translated into Event-B specifications. The main idea is to use the formal refinement concept to prove their correctness. As the semantics of this refinement is not the same as the standard Event-B refinement, we have defined new proof obligations to express it, which can be discharged using Atelier B. Finally we illustrate our approach on a case study from the railway domain.

Securing a safety-critical system is a challenging task, because safety requirements have to be considered alongside security controls. We report on our experience to develop a security architecture for railway signalling systems starting from the bare ...

In this paper, we consider the European Rail Traffic Management System (ERTMS) as a System-of-Systems (SoS) and propose modeling it using colored Petri nets. We formally control the European rail transport, while guaranteeing a set of cross-border security properties. This becomes an essential and challenging task since each of them have mainly developed safety and trackside rules regardless of its neighbors. The feature of this work lies in the approach that considers ERTMS Level 2 as an SoS and addresses the cross-border railway as a mode management problem. In addition, the aspects of mode activation/deactivation, starting state and handling of resource states common to multiple operating modes are taken into account in the proposed model.

Formalizing system specification has been highly valuable in demonstrating safety and consistence of safety critical systems. It is undoubtedly the case in railway signalling, especially the European Rail Traffic Management System/European Train Control System (ERTMS/ETCS). However, the complexity of the European standard specification, especially for its highest level, namely level 3, requires a significant overtake in early modelling approaches when it comes to clearly expressing system functionalities along with safety requirements, all towards a concrete safe design. In this regard, our research introduces a Colored Petri net (CPN) sub-class associated to an Event-B machine and annotated by mathematical sequences, which are ex-pressed in the B-language, all in the view of enriching the modelling techniques intended for system formal specification and verification. In this paper, we show through a detailed ERTMS L3 case study, how such featured CPNs fit in the progressive formalization and verification of Movement Authority (MA) computation.

International audience

ENASE 2019, 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, GRECE, 04-/05/2019 - 05/05/2019

In the context of Safety Critical Systems (SCSs), safety measures derived from the dysfunctional analysis are generally expressed in an informal way. However, in an early phase of SCSs design, there is a need to link these safety measures to Goal-Oriented Requirements Engineering (GORE) concepts. Moreover, the current practice of the safety measures development is not based on a specific goal-oriented control model. Since there are different knowledge domains, there is a lack of a common vocabulary aiming to avoid the semantic heterogeneity between them. Consequently, a common model for an unambiguous knowledge sharing and a full semantic interoperability assurance is missing. In this paper, we propose the Goal-Oriented Safety Management Ontology (GOSMO), a domain ontology, which is grounded in the Unified Foundational Ontology (UFO) and provides a conceptualization and a real-world semantic interpretation of the knowledge matching for SCSs. Furthermore, the proposed safety measures development process is performed using a reinterpretation from the safety point of view of the Organization-Based Control Access (Or-BAC), which was initially developed for the Information Systems (IS) security. The GOSMO aims to capture the alignment between the considered domains concepts through the reference models reuse and the proposed taxonomy based on standards definitions. The proposed ontology is evaluated by the formalization of two cases studies from the railway domain, since it is the target application domain. Finally, the evaluation results show that GOSMO covers and analyses several real critical situations and fulfils its intended purpose.

ICSOFT 2019, 14th International Conference on Software Technologies, Prague, TCHÈQUE, RÉPUBLIQUE, 26-/07/2019 - 28/07/2019

ICSOFT 2018, 13th International Conference on Software Technologies, Porto, PORTUGAL, 26-/07/2018 - 28/07/2018

This paper presents an original experimental protocol, which aims to study human reliability in railway systems by computing the human error probability (HEP) of human operators. The experiment is conducted on a railway traffic management system that places operators in simulated situations involving railway failures. The obtained experimental result is analyzed first by two classical human reliability analysis methods to estimate the HEP of each subject. Then, a model of human operators using valuation-based system is proposed. Finally, a methodology automatically populates the proposed model by allowing the verification of temporal properties on the simulation trace.

The aim of this work is to propose a formal model for determining the dynamic optimal path for transfer operations on an oil flow network within real conditions of exploitation such as maintenance activities and alignments in-service. The study focuses on a multi-objective problem to search a safe and short path to the oil transfer operations. It is based on, firstly, dynamic reliability, that depends on time and conditions of use, of engaged valves in the path; and secondly, pipes lengths; and it is developed in a High Level Petri Nets (HLPN) framework. Real operational constraints and goals in the seaport are modelled with data extracted from OREDA Database. The results show how the proposed solution leads to a safer use of the network by avoiding riskiest valves and conflicts between oil transfer operations and between transfer operations and maintenance tasks. This contribution is applied in the oil transport, but it is potentially applicable in many other areas.

The problem of assignment containers to AIVs in a container terminal is a complex problem, it is a combination of several problems, the dispatching problem, the vehicles routing problem and the scheduling problem. Each problem of these depends on some criteria, this makes the global problem as a multi-criteria problem. To solve this type of problem, the idea is to consider it like a mono-objective problem depending on each criterion separately. An aggregation function is calculated according to different criteria. The coefficient value of each criterion is proposed by an expert, these values can give the nearest Pareto front solution. The approach proposed in this work is a hybrid approach, genetic algorithm and Dijkstra algorithm. This approach is tested with different numbers of vehicles, for each problem separately, in order to have the best solution. The numeric results show the performance of our approach for the multi-objective problem.

The existence of maximal durations drastically modifies the performance evaluation of discrete event systems (DES). For instance, the classical formulas used for a cycle time computing can not be used. Nevertheless, there are a lot of these constraints in food and chemical industries. Therefore, using P-time PN in order to compute performance evaluation and to prove functioning margin existence is depicted in this paper. Then, the HLPN are shortly described. Based upon HLPN definition, the Hypernets are introduced. It is shown that the behaviour of a system considering time window constraints specification can be performed by the same way using P-time PN or Hypernets. Moreover, handling P-time PN as a sub-class of Hypernets allows integrating them in a global approach. It is obvious that time is not the only parameter to take into account in a plant scheduling. Hypernets allows integrating the parameter that P-time PN are not able to model. The paper ends with a proposition for an integrated approach based upon the two kinds of net. A global scheduling is made with Hypernets and a local analysis with P-time PN. This approach is illustrated on electroplating lines.

Presents the ability of a new Petri net tool to face a kind of industrial problem. These problems are characterized by operating times included between a minimum and a maximum value. The considered application is an electroplating line for which the carrying resources must be free at a time which is compatible with the treatment durations. The first step is the modeling of these specifications. The second step is devoted to the search of a sequencing of the hoist compatible with the objective and the staying time constraints of the parts in the treatment baths. The third part consists in determining a local control: the beginning and the ending instants of each treatment. This class of problems is known as the "hoist scheduling problem". We focus on the repetitive functioning mode.