François Huet

Kieu Ngo
email: kieu.ngo@sorbonne-universite.fr

Electrochemical Noise-Guidance for Improving Measurements and Data Analysis

Keywords: electrochemical noise, guideline, dummy cell, pitting corrosion

  L'archive ouverte pluridisciplinaire

INTRODUCTION

In order to evaluate the reliability of electrochemical noise (EN) measurements performed by commercial general-purpose potentiostats, Round-Robin (RR) tests have been performed by different groups. 1,2 Recently, three new RR tests on EN measurements with dummy cells have been performed by the European Cooperative Group on Corrosion Monitoring of Nuclear Materials (ECG-COMON). 3 Using dummy cells, composed of three resistors of equal value connected in a 'star' arrangement, with a potentiostat working in a zero-resistance ammeter (ZRA) mode, gives the possibility of measuring voltage and current noise signals of reproducible amplitude, in contrast to corrosion processes that often evolve with time.

As shown in Figure 1(a), the power spectral densities (PSDs) of the potential fluctuations due to the thermal noise of 1 M dummy cells measured by all participants are extremely different, some of them being 8 decades higher than the theoretical value of 6kTR, where k is Boltzmann's constant, T is the temperature in Kelvin and R is the resistance in Ohm. 4 An important cause of the large discrepancy in the results comes from aliasing of high to low frequencies during the analog-to-digital conversion in potentiostats that are not equipped with analog low-pass anti-aliasing filters that eliminate frequencies above half the sampling frequency to respect the Shannon theorem. 5 Consequently, for such measuring devices, signals measured at different sampling frequencies have PSDs that do not overlap in common frequency ranges, as shown for example by the non-overlapping PSDs in turquoise and peach colors (amplitude between 10 -6 and 10 -7 V 2 /Hz) on the top of Figure 1(a) (see also Figure 5 in Reference 3). From this work, it was concluded that only very few commercial potentiostats are actually able to perform valid EN measurements. Working with a potentiostat equipped with an anti-aliasing filter gives better results, as illustrated in Figure 1(b) in which all curves are in a range of only 5 decades above 6kTR. Nevertheless, this figure exhibits some errors in the measurements and different levels in the PSDs at low frequencies, which was unexpected since only the gain of the voltage amplifier had to be fixed adequately. The results are even worse for the current fluctuations according to the much larger scatter observed in the PSDs observed during the RR tests. 3 It is then important to train people to learn how to perform valid EN measurements, which is the aim of this paper that presents two practical works, one using dummy cells and the other a corrosion system. It is not intended in these works to perform complete EN studies on new systems: pitting corrosion of aluminum in 1M potassium chloride solution was chosen for its rapidity to generate pits and, as a consequence, an EN signal of high level easy to measure. However, it is not possible for a beginner in the EN technique to start working directly with a corrosion system since the EN results vary from one user to another according to the experimental conditions, while the level of the thermal noise generated by dummy cells is well known. It is then necessary to start EN measurements with dummy cells to try measuring the expected level of noise and, for that, to learn how to use the software controlling the potentiostat. The thermal noise of dummy cells is a signal of low level, so the measurement is difficult, but it should be noticed that the EN generated by a passive electrode is as low. It is then important to succeed in achieving such measures. In a second step, pitting corrosion was investigated first using identical electrodes to show how to valid the EN measurements using the noise impedance, and then asymmetric electrodes to raise awareness of the difficulty of analyzing the noise measured in such conditions.

EXPERIMENTAL PROCEDURES

Dummy cells

Figure 2 shows two dummy cells composed of three identical resistors of 1 and 10 M in a 'star' arrangement, the latter being installed on a printed circuit board. The resistors were connected to the counter electrode (CE), working electrode (WE), and reference electrode (RE) inputs of the potentiostat that imposed a zero potential difference between the CE and the WE (ZRA mode). [2][3][4] Therefore, no current was flowing through the resistors that were at thermodynamic equilibrium. A simple Faraday cage made of aluminum paper surrounding the dummy cell and connected to the floating ground cable of the potentiostat, or to the ground of the mains supply, was used to eliminate as much as possible 50/60 Hz electrical interference. The dummy cell must first be wrapped in insulation paper to avoid any contact with the aluminum foil. In practice, it is advised to use a Faraday cage for investigating systems with high impedance at high frequency, as for the dummy cell, since this drastically reduces the amplitude of the signal components at 50/60 Hz and harmonics that hinder the measurement of the EN at low frequencies.

Electrochemical system

As mentioned above, pitting corrosion of aluminum (Al) electrodes in 1 M potassium chloride was chosen as a real electrochemical system to start EN measurements. Two identical Al electrodes consisting of disks of 25 mm in diameter (surface area of about 4.9 cm 2 ) polished on 1200 emery paper were used as WE and CE. The electrodes faced each other at a distance of about 1 cm in a vertical position by a retaining ring. A saturated calomel electrode (SCE) was used as RE. As for the dummy cells, a zero potential difference was imposed between the Al electrodes by the potentiostat in ZRA mode so that both electrodes were at corrosion potential (symmetric system). In another experiment, an asymmetric system was obtained by imposing a bias potential of 800 mV between the WE and the CE so that one electrode could be considered as an anode, the other one as a cathode. No Faraday cage was used since the external noise sources in the laboratory environment were insignificant. When the EN signals are corrupted by 50/60 Hz electrical interference, it is necessary to use a Faraday cage, for example as that described above.

Procedure for EN measurement and validation

A Gamry Reference 600 † potentiostat with software ESA410 † was used in this work for measuring the fluctuations of the potential difference between the WE and the RE, and the fluctuations of current flowing between the WE and the CE. The measurement procedure in ZRA mode for this particular measuring device is given in Appendix A. For potential measurements, only the range of the potential channel (Vch range) has to be set by the user, which fixes the amplification gain of the potential difference between the WE and the RE (see Table 1) in the potentiostat. In contrast, measuring the current fluctuations is more complex since the user must set the values of two parameters, the I-E range, which fixes the value of the current-measuring resistance (Rm), and the Ich range, which fixes the gain of the amplifier (see Table 1) installed at the output of the I-E converter.

Table 2 gives the values of Rm and the effective gain in V/A of the I-E converter as a function of the I-E range. It also indicates the upper value of the frequency bandwidth of the measurement channels as a function of the I-E Stability parameter. Depending on the corrosion system, the I-E range and the Ich parameter must be fixed according to the amplitude of the current fluctuations at the sampling frequency fs employed (see the procedure in Appendix A) with a special attention to the fact that the upper limit of the frequency bandwidth might not be half of the sampling frequency when low I-E ranges are selected (see Table 2). Extremely low frequencies can be analyzed, the lowest being fs/N where N is the number of data points recorded as long as desired but, in practice, the EN is not stationary enough to investigate frequencies well below 1 mHz.

Validation of EN measurements is not possible in the time domain since the amplitude of the noise depends on the sampling frequency, as shown below (Figure 3(a)). Validation can only be performed in the frequency domain by calculating the PSDs of signals sampled at least at two different frequencies. 4 The two main calculation methods usually employed are the maximum entropy method and the periodogram method based on the fast Fourier transform. After comparison, the latter was preferred to obtain a good overlap of the PSDs of wide-band random signals requiring to be sampled at various frequencies. 6 In this work, the PSD of each time record was calculated using the program psd-detrend_ECG-COMON.exe that can be downloaded for free from the ECG-COMON website (www.ecg-comon.org) with its configuration file config_psd-detrend_ECG-COMON.txt, after having exported the raw time data (extension .esa) to an ASCII file consisting of three columns (time in s, potential noise in V, and current noise in A), separated by tabs. Following the instructions given by the user in the configuration file, the program calculates the potential PSD, the current PSD, and the noise impedance (Zn), which is defined as the square root of the ratio PSD V/PSD I, by dividing the ASCII file in several (at least 10 is recommended) sections of N data points to get averaged PSDs in the frequency bandwidth [fs/N, fs/2] that are accurate enough to control the overlap of the PSDs. 3 To limit the measurement time in a practical training work, it is possible to successively sample the signals at frequencies fs = 1 kHz during 30 s, 100 Hz during 4 min, 10 Hz during 4 min 30 s, and 2 Hz during 5 min 30 s. In that case, the PSDs are calculated with 14, 11, 10, and 10 sections of N = 2048, 2048, 256, and 64 data points, respectively. Obviously, the analyzed frequency bandwidth is limited at low frequency (fs/N = 0.5 Hz, 0.05 Hz, 0.04 Hz, and 0.03 Hz, respectively) in this exercise. In practice, for a complete study of a given electrochemical process, it is necessary to analyze lower frequencies by selecting a lower sampling rate and/or a higher number N of data points per section. In the literature, in most studies using the EN technique, the analyzed frequency bandwidth is roughly [1 mHz -1 Hz] when the measurements are performed in ZRA mode since the corrosion processes at the open circuit potential (OCP) are slow. Higher sampling rates have to be used when the measurements are carried out in potentiostatic mode in the passivation domain to investigate pitting corrosion since the passive layer breakdown and pit repassivation are fast processes.

RESULTS AND DISCUSSION

Measurement of the thermal noise of resistors

The aim of this practical work is to learn how to perform and validate EN measurements on a stationary system giving reproducible results on the one hand, and to determine the noise level of the potentiostat on the other hand. According to the Fluctuation-Dissipation theorem (Nyquist law), 7 the PSD of the thermal noise voltage generated by a resistor at thermodynamic equilibrium is equal to 4kTR. For the dummy cell considered in this work, it has been shown that the PSDs of the potential and current noise is equal to 6kTR and 2kT/R, respectively. 4 The thermal noise level is low, as low as that generated by a passive electrode, and it is important to carry out the EN measurements at different I-E ranges to identify in the measured EN the contribution due to electrochemical processes and that due to the potentiostat. Validating EN measurements is not possible in the time domain since the peak-to-peak amplitude of the time records varies according to the sampling frequency selected, as shown in Figure 3(a) for the dummy cell but this could be shown for any electrochemical system. This is due to the presence of the anti-aliasing low-pass filter required in the measurement channel before the analogto-digital conversion: the lower fs, the lower the cut-off frequency of the filter, the higher the number of filtered frequencies, and therefore, the lower the amplitude of the signal. In contrast, validation of the EN measurements is possible in the frequency domain by checking the overlap of the PSDs. As an example, Figure 3(b) shows the good overlap of the PSDs of the time records presented in Figure 3(a). Moreover, the PSD level is equal to 6kTR at frequencies above 5 Hz, indicating that the voltage thermal noise of the dummy cell was actually measured. A pure 1/f behavior, typical of noise generated by semiconductors and originating from the instrumentation, can be observed at lower frequencies. In this range, an electrochemical potential noise of lower amplitude cannot be measured in the operating conditions employed.

As explained above, measuring the thermal noise in current (current noise) is more difficult since two parameters, the I-E range and the Ich range, have to be set by the user. For the 10 M dummy cell, various PSD levels can be viewed in Figure 4 for the current noise measured at different I-E ranges with the I-E Stability parameter "Fast". This parameter is usually selected because it allows the highest upper limit of the frequency bandwidth to be measured for a given I-E range (see Table 2) without playing any role on the lowest frequency that can be analyzed. To explain the magnitude of each PSD and select the proper I-E range, it is necessary to model the different noise sources influencing the measurement of the electrochemical current noise. 8 Writing the generalized Ohm's law at point A and across the resistor Rm gives in the frequency domain (j is the square root of -1), respectively:

  ) i (i Z ) i (i Z e G e 1 1 2 2 n2 n1      (1)
and:

) i i (i R i Cj 1 nm C m C     (2)
where C is the capacitance in parallel with Rm, which depends on the I-E Stability parameter selected. Equations 3 and 5 are then straightly derived:

  2 2 1 1 n 2 1 i Z i Z e Z Z 1 i     (3) with: n2 n1 n e G e e   (4)
and:

) i ) Z (Z i Z i Z e ( Z Z 1 Cj R 1 Cj R i nm 2 1 1 1 2 2 n 2 1 m m C          (5)
which gives the expressions of the potential and current measured by the potentiostat:

            out 1 2 1 meas n,v 3 3 1 1 1 2 3 3 n,v n V 1 2 1 2 V Z Z Z V e Z i Z( i i) ( i i) Z i e e G Z Z Z Z (6)
and:

                n,i n,i out C 2 2 1 1 n meas nm I m m m m 1 2 1 2 m e e I i Z i Z i e 1 1 I -i G R R Cjω R 1 R Cjω Z Z Z Z R (7)
Under the hypothesis of independent noise sources, the expressions of the PSDs of the measured potential and current can be derived:

           2 2 2 1 2 1 V i i 3 i e e meas 1 2 3 n,v n 1 2 1 2 Z Z Z ( ) Z Z Z Z Z (8)                      2 2 1 i 2 i e 1 2 n I i e meas nm n,i 2 2 2 2 2 2 m m 1 2 Z Z 1 1 1 R C 4 f R Z Z (9)
For the dummy cell, Z 1 = Z 2 = Z 3 = R. The PSD of the current thermal noise of a resistor R being equal to 4kT/R, Equations 8 and 9 become:

     V e e meas n,v n 1 6 kTR 4 (10)
and:

               I e e meas n n,i 2 2 2 2 2 2 m m m 1 2kT 1 4kT 1 R R 1 R C 4 f 4R R (11)
The last two terms in Equation 10 correspond to the voltage noise of the instrument, which is preponderant at frequencies lower than 5 Hz in Figure 3 In conclusion, according to Figure 4, for R = 10 M the best value of Rm to obtain a PSD plateau close to the expected amplitude of 2kT/R was 20 M, which is a value of the same order of magnitude as R. In practice, for stationary systems showing a low EN level, as for dummy cells or for passive electrodes, it is important to select the highest value of Rm that does not overload the current amplifier. For electrochemical systems, when the noise level is expected to increase with time, it is advised to select a lower value of Rm (see Appendix A).

Measurement of the EN generated by pitting corrosion of aluminum electrodes

Symmetric system

Figure 6 shows time records of the potential and current fluctuations generated by pitting of Al electrodes in potassium chloride, and their corresponding PSDs, together with the noise impedance Zn and the modulus of the impedance of the electrodes that was measured from 100 kHz to 0.1 Hz in potentiostatic mode at OCP using an excitation signal of 10 mVrms amplitude. As for the dummy cells, validation of the noise measurements is given by the satisfying overlap of the PSDs measured at different sampling frequencies, as shown in Figure 6(b). Furthermore, the noise impedance derived from the potential and current PSDs fits well with the modulus of the impedance in Figure 6(c), which is another argument for noise validation. Indeed, this result has been demonstrated theoretically 9 and experimentally 10 when the RE is a true reference electrode (such as calomel, sulfate, silver/silver chloride reference electrodes). It must be noticed that such result is obtained as long as the noise of the instrumentation can be neglected 8 , as in the present experiment in which the high pitting activity was due to many individual pitting transients that overlapped so that they cannot be observed separately in Figure 6(a). The amplitude of the resulting noise is large, a few mV for the potential and a few µA for the current. Of course, such result could not be obtained with the dummy cell since the noise of the RE had the same amplitude as the noises of the CE and WE. It cannot be obtained either in the field when a third identical electrode is used as a pseudo RE since the noise generated by corrosion processes on this electrode has a great influence on the noise impedance. 9,10 Asymmetric system Asymmetry in the electrodes has sometimes been purposely employed, so as to limit corrosion on one electrode, the anode, the other electrode acting as a cathode. 11 In other cases, identical electrodes cannot be used, as in stress corrosion cracking investigations where only one electrode is under stress, or in crevice corrosion studies where crevice attack occurs on one electrode only. As an easy exercise to appreciate the difficulty of the EN analysis for asymmetric systems, a bias potential of 800 mV was applied between the two identical aluminum electrodes and the potential and current noises were measured in ZRA mode. Then, the impedance of each electrode was measured. It must be noted that the anode potential varied significantly with time so that it was difficult to perform the impedance measurement in potentiostatic mode at the electrode potentials measured when the bias potential was applied. Therefore, the impedance measurements were carried out in galvanostatic mode by imposing a DC current of +4.3 mA for the anode, which gave a potential of -0.74 V/SCE, and -4.3 mA for the cathode, which gave a potential of -1.54 V/SCE (see Figure 7(a)). The amplitude of the current excitation was 0.7 mArms. fluctuations have an amplitude much higher than that at OCP in Figure 6 and do reflect pitting corrosion, the noise impedance derived from the PSDs is equal to the impedance modulus of the cathode, according to Figure 7(d), which is an a priori surprising result. This can be explained using Equations 8 and 9, in which all noise sources due to the instrumentation have been neglected in front of the EN caused by pitting corrosion. The PSDs of the measured current and potential fluctuations can be written:

     2 a c V i i meas a c a c Z Z ( ) Z Z and       2 2 a i c i a c I meas 2 a c Z Z Z Z (12)
where Za and  I a (resp. Zc and  I c ) are the impedance and the current noise source of the anode (resp. cathode). For the present system, the impedance of the cathode was much lower than that of the anode and the current noise due to oxygen reduction on the cathode was not significant compared to that on the anode, so that the expressions of  V meas and  I meas can be reduced to:

   2 V c i meas a Z and    I i meas a (13)
which shows that the noise impedance is equal to the impedance modulus of the cathode. Finally, owing to the high noise generated by pitting occurring on the anode, the impedance (modulus) of the cathode was determined, which is not a straightforward result. In other situations, the noise impedance may be close to the impedance modulus of the anode or simply be comprised between the impedance moduli of the electrodes. 11 It should be noted that, despite a higher current noise ia on the anode, the amplitude of the potential fluctuations was lower in presence of the bias potential. This can be explained using Equation 13 in which  V meas reduces to |Zc| 2  i a , which remains low because of the much lower impedance modulus of the cathode.

In conclusion, while the EN analysis is simple for symmetric systems, asymmetric systems require the measurement of both the potential and current noise and the impedance of each electrode for a thorough analysis of the stochastic behavior of the corrosion process.

CONCLUSIONS

In view of the unreliable EN results obtained in the Round-Robin tests performed on dummy cells by the ECG-COMON with most commercial potentiostats, 2,3 often coming from the absence of anti-aliasing filters in the measuring devices, it is important to train people to learn how to perform valid EN measurements with a commercial potentiostat equipped with such filters. This paper presents several practical experiments, consisting first in measuring the thermal noise of dummy cells, a noise of amplitude as low as that of passive electrodes, to learn how to set the parameters of the controlling software correctly and identify the noise level of the instrumentation. Then, the EN generated by pitting corrosion of aluminum in potassium chloride was investigated by using symmetric and asymmetric electrodes. Validation of the EN measurements is obtained from the quality of the overlap of the PSDs of time records sampled at different sampling frequencies. It is important to emphasize that it cannot be obtained from the analysis of data in the time domain only and that working in the frequency domain is absolutely mandatory. In addition, when the corrosion system generates an EN of relatively large amplitude, which is often the case for pitting corrosion, validation is also obtained by comparing the noise impedance, calculated from the potential and current PSDs, to the impedance modulus of the electrodes for a symmetric system, or to the impedance modulus of the less noisy electrode for an asymmetric system. All these recommendations concerning the validation of the EN measurements have been issued using a particular commercial potentiostat. However, they are general and can be applied to any other equally reliable EN measuring 8) For the voltage fluctuations, evaluate the peak-to-peak amplitude on the screen during the measurements, and check if this value is lower that the Vch range. 9) For the current fluctuations, evaluate the peak-to-peak amplitude on the screen during the measurements, multiply it with the gain in V/A of the I-E converter given in Table 2 and check if this value is lower that the Ich range.

10) If the EN is expected to increase during the experiment, it may be necessary to use higher I/E, voltage, and current ranges.

11) Start to record EN data.

12) Observe the overload indicators. Once the overload warning occurs, the data may be unreliable.

13) When the test is finished, toggle cell off.

LIST OF CAPTIONS

  Figure 5 presents the schematic circuit of the potentiostat used in ZRA mode (Z1, Z2, and Z3 are the electrochemical impedances of the WE, CE, and RE, respectively) with the main noise sources due to the electrochemical processes and to the instrumentation: thermal noise of the resistors, -inm is the current thermal noise source of the current-measuring resistor Rm, -en1 is the voltage noise source of the operational amplifier controlling the potential in the potentiostat, -en2 is the voltage noise source of the amplifier (gain G equal to 1) measuring the potential difference between the CE and WE, -en,v is the voltage noise source of the potential amplifier of gain GV, -en,i is the voltage noise source of the current amplifier of gain GI.

  , as mentioned above. The expression of the PSD of the measured current noise is more involved but Equation 11 allows the results of Figure 4 to be explained. For the lowest values of Rm (2 k to 2 M), the PSD varies in 11, the main source of noise below 5 Hz is then the differential amplifier of gain GI. At high frequency,  I meas is inversely proportional to Rm so the measured noise may be attributed to the thermal noise of Rm. For Rm = 20 M and 200 M, the spectra  I meas are identical at low frequency, indicating that the current noise below 5 Hz can be attributed to the noise of the amplifiers in the potentiostat,  e n /R 2 . At high frequency, it must be noted that the presence of the capacitance C (close to 150 pF for "Fast" I-E Stability) in parallel with the resistor Rm introduces a low-pass filtering with a cut-off frequency of 1/(2RmC), which plays a significant role when high values of Rm are selected. For example, for Rm = 20 M (I-E range = 6 nA), the PSD starts decreasing at a frequency close to 50 Hz, as expected from Table 2 for the I-E Stability parameter "Fast". The PSD decrease would have appeared at a lower frequency if another value of the I-E Stability parameter had been used. Around 10 Hz, the PSD value is equal to the sum of the PSD values of the current thermal noise of the dummy cell and resistor Rm, 2kT/R + 4kT/Rm. If a higher value of Rm is selected (Rm = 200 M, i.e. I-E range = 600 pA) to eliminate the influence of 4kT/Rm and measure the thermal noise of the dummy cell, the cut-off frequency decreases, which explains the shift on the left of the high frequency part of the PSD of the current noise.

Figures 7 (

 7 Figures 7(b) and 7(c) show the time records and PSDs of the potential and current fluctuations,

6 ) 7 )

 67 devices. In addition, the development of Equations 10 and 11 allowing the interpretation of the EN results for the dummy cells and the determination of the instrumental noise, may serve for other equipment because the measuring circuits in most commercial potentiostats are very similar. The current noise is measured by amplifying the voltage across a resistor and the potential noise by amplifying the potential difference between the WE and the RE. Set all I-E range, Current channel, Voltage channel to manual mode. Try to decrease I-E range down to get a minimum setting without overload. Once the overload indicator is triggered for more than 20 s, meaning a too-low current range for the measured value, the user should set the range one order up. Decrease voltage channel and current channel manually down to get a minimum range without overload.

FIGURE 2 .FIGURE 3 .

 23 FIGURE 2. (a) 10 M and (b) 1 M dummy cells in a 'star' arrangement.

FIGURE 4 .

 4 FIGURE 4. PSDs of the current fluctuations measured on a 10 M dummy cell at various sampling frequencies and I-E ranges (I-E Stability "Fast", Ich = 30 mV).

FIGURE 5 .FIGURE 6 .FIGURE 7 .

 567 FIGURE 5. Schematic circuit of the potentiostat working in ZRA mode with predominant noise sources.

FIGURE 1 . 3 VoltageFIGURE 2 .FIGURE 3 .FIGURE 4 .

 13234 FIGURE 1. PSDs of potential fluctuations measured on 1 M dummy cells by the ECG-COMON

FIGURE 5 .FIGURE 6 .

 56 FIGURE 5. Schematic circuit of the potentiostat working in ZRA mode with predominant noise

FIGURE 7 .

 7 FIGURE 7. (a) Current-voltage curve showing the potentials Va, Vc of two identical corroding electrodes of the same material connected through a ZRA when a bias voltage Vbias is superimposed; (b) time records (fs = 100 Hz, arbitrary zero of time scale) and (c) PSDs of the potential and current fluctuations due to pitting corrosion of identical aluminum disk electrodes (diameter 2.5 cm) in 1 M KCl (fs = 10 Hz and 100 Hz); (d) Zn and |Z| of each electrode.

TABLE 1 .

 1 Gain of the Vch and Ich amplifiers as a function of the Vch and Ich range

TABLE 2 .

 2 Current

	-measuring resistance, Rm, gain of the I-E converter, and upper value of the
	frequency bandwidth of the current channel as a function of the I-E range and I-E stability
	FIGURE 1. PSDs of potential fluctuations measured on 1 M dummy cells by the ECG-COMON
	in 2017 (a) with potentiostats of various origins (77 curves), (b) with the potentiostat used in this
	paper (36 curves). 3

† Trade name

ACKNOWLEDGMENTS

The authors thank Max Yaffe and Dominik J. Moosbauer from Gamry Instruments † for participating in the Round-Robin tests as well as for helpful discussions on EN measurements.


Keywords: Railway signalling systems, Formal methods, Safety verification

Due to the increasing complexity of railway signalling systems, the design of those systems is more difficult and the demonstration of their safety can be extremely tedious. In this article, the verification and validation of railway signalling systems is investigated. We explain how railway signalling functions are designed, we show how they can be mathematically modelled using formal methods and we discuss some ways to use formal methods mechanisms to design, verify signalling systems and to prove the validity of their safety properties.

Introduction

About two centuries ago, the railway revolutionized our lives, allowed an acceleration of exchanges and redesigned our territories. Since then, it has constantly evolved and improved, complying with two contradictory requirements: speed and safety. The railway transport typifies one of the oldest safety cultures, in which, there is the willingness to create systems and installations that are not susceptible to the risk of human error.

The aim being to reduce the frequency and the consequences of accidents which can be dramatic in terms of human and financial losses, due to the speed of the trains, the number of passengers and the cost of infrastructures. Nowadays, railway accidents are very rare and their consequences are far less disastrous than they have been at the beginning of the railway era. However, the safety of railway transport is not granted. In France for example, the number of people seriously injured in a railway accident has increased by 22%, in 2016 [START_REF] Epsf | [END_REF]. Thus, designers must constantly adapt to technological developments to maintain a high level of safety. The railway signalling is a crucial element of this safety. Its task is to give to the driver, via well-defined codes and signals, all the needed information to safely circulate, and, via the interlocking functions, it guarantees a secured track status and inhibits the movement of track devices, such as points, while a train is traveling along a route. In addition to their safety function, signalling systems must improve operations by ensuring traffic optimization. The mission of railway signalling design offices is to offer safe and optimum solutions while meeting the economic feasibility constraints. In order to do so, they rely on experts' knowledge and experience. Nowadays design offices are facing new challenges: the increasing number of passengers that requires more efficient operations, the extension of the rail networks that leads to a congestion of the installations. Moreover, due to technological evolutions such as computerization and automation, the design of signalling systems requires the ability to combine old and new technologies.

In this context, new design and verification methodologies must be provided and those methodologies must be adapted to safety systems by offering rigor and automation, and must be adapted to the specificities of the railway field. Formal methods are suitable. Indeed, thanks to its rigorous and exhaustive nature, a formal methodology could guarantee, via proof of properties, that the designed system is consistent with the specifications.

In this paper, we want to show how formal methods could be introduced in signalling design offices to assist verification, to encourage innovation and to lighten safety demonstration processes. Section 2 describes the main issues of designing signalling principles. In Section 3 we give an overview of formal methods. In Section 4 we explain how to model an electromechanical system of signalling with formal methods through, a concrete example. In Section 5, we discuss the modelling approach and its limits.

Evolution, Constraints, Standards

Railway is one of the safest means of transport. In railway transport, the concept of safety is essential and it is based on four factors: regulation, staff alertness, braking devices and railway signalling. Railway regulation, expressed as standards and directives, describes all the organizational, technical and legal arrangements that govern the operations and the design processes of railway systems. The standards are regularly revised to adapt to technological changes. For instance, the standard EN50128 [START_REF]Standard NF EN 50128 Railway applications. Communication, signalling and processing systems[END_REF] applicable for information systems of signalling has recently been revised, in 2011. The safety integrity level (SIL) is a quantization index of risk reduction, based on a scale of one to four, and a risk analysis defines, for each function of a system, its SIL requirement. For example, the route setting commands are SIL0 because there is no need of risk reduction, while the signal opening is SIL4 because it is a safety function. The standards IEC 61508 [START_REF]Standard IEC 61508 Functional Safety of Electrical/Electronic/Programmable Electronic Safety-related Systems[END_REF] describe the development activities and the techniques to be used to comply with the SIL level. The higher the level, the more constraining are the development activities imposed by the standards. When a system is designed, it is assigned a SIL level, which expresses a safety objective, and then, the system is evaluated by certifying bodies; compliance with applicable standards means obtaining a SIL certificate. Railway signalling, was at first rudimentary; for example, on the first railroad lines, track surveillance was carried out by humans, using signal flags, marker lights and whistles to transmit signals. Now, it is a highly precise technical field, based on modern technologies, combining electromechanical devices and computer science. Since the early days of railway, the science of accident investigation started to transform railway systems to improve their reliability and engineers introduced automation to avoid human fault. For instance, one of the first major innovations was the continuous automatic compressed-air-brake, invented in the nineteenth century and still used to date in current trains. The latter system is based on the safety principle that allows to release the brake only if it is pressurized and not damaged.

Modern systems are still designed with a view to reducing the risk of human fault. In fact, since the seventies, information technology has been introduced in operations support systems, then in interlocking systems, such as the System of solid-state interlocking (PAI). More recently, this technology takes also action to automate metro lines (e.g. System METEOR) or for predictive maintenance using Internet of Things (IoT). The emergence of all these new technologies leads to more complexity and need to be supported by modern, adapted methods.

Railway Signalling in France

The railway signalling is an information system, the function of which is to control, monitor and interlock points, s²ignals and other appliances, in order to ensure a safe train-running over track sections. The main purposes of this system are to: ─ maintain a safe separating distance between trains going in the same direction, ─ avoid derailment due to speed excess, ─ avoid traffic in both directions on the same track (face to face), ─ ensure a safe traffic at level crossings, ─ prevent trains from taking conflicting routes (converging traffic lanes, traffic cut…).

Another function of railway signalling systems is to ensure optimum operations while guaranteeing safety; and the growth of the number of passengers in urban transportation networks makes it a real challenge, promoting the emergence of systems as the SACEM (Système d'Aide à la Conduite à l'Exploitation et à la Maintenance) which provides optimum speed instructions to the driver.

In France, hard-wired logic systems have been favored due to their reliability, maintainability and to the intrinsic safety of their equipment. In fact, electromechanical interlocking devices are a safe bet for the railway signalling and a good knowledge of the equipment is essential for the maintenance of a system. For this reason, computerized signalling technology has not witnessed the same success. Moreover, the implementation of computer-based systems is mostly constrained by the cost of their development because that implies to be able to prove their Safety Integrity level (SIL). In fact, meeting the requirements of standards such as EN50128 [START_REF] Coudert | Formal Methods for Safe Design of Autonomous Systems dedicated to risk management[END_REF] in terms of resources, organization and development cycles can be difficult and expensive because it imposes, at each stage, a quantity of documents (specifications, plans…), verifications and tests, carried out by independent teams. Furthermore, the software maintainability can hardly reach the safety relay's which is ensured by the endurance of the equipment. Nevertheless, there are some good examples of the use of digital systems such as the Computer-Controlled All-relay Interlocking (PRCI) which allows the computerized command of routes, while the interlocking and the monitoring of the routes are ensured by the safety relays NS1 [START_REF] Rétiveau | La signalisation fériovaire[END_REF].

Besides, the French regulation requires, for all new systems or any alteration of an existing system, to demonstrate a safety level at least equal to the safety level of the existing systems [START_REF]Standard NF EN 50126 Railway Applications Specification and Demonstration of Reliability, Availability, Maintainability and Safety (RAMS)[END_REF]. Hence, it is easier to achieve an equivalent level by using the technologies of existing systems rather than trying new technologies. Therefore, we can say that the tediousness of safety demonstration can be a slowing point to innovation which is regrettable considering that signalling systems need more innovation than they ever did before Indeed, the installations are increasingly complex, congested, making them more difficult to maintain. Maybe by optimizing logic circuits or by interfacing them with digital systems, it would be possible to reduce the quantity of equipment and, as a result, reduce wire and congestion in installations Innovation on principles of hardwired logic can also improve the operations. A perfect example [START_REF] Rétiveau | La signalisation fériovaire[END_REF] is the passage of rigid transit (which allowed the setting of a route only after all the occupied transit zones of the conflicting route were released) to flexible transit (which allowed the setting of a route as soon as the convergence zone with the conflicting route was released).

The design of signalling principles is a creative task based on experts' reasoning and this reasoning is usually checked manually. In fact, the verification of these principles is a real issue for design offices because it requires specific skills and good experience and knowledge of systems and equipment. Besides, it has to be carried out by two experts with a sufficient level of independence in terms of the standard EN50126 [START_REF]Standard NF EN 50126 Railway Applications Specification and Demonstration of Reliability, Availability, Maintainability and Safety (RAMS)[END_REF], who have not been involved in the design part of the system. This whole independent organization represents a significant cost for companies. In addition, an installation cannot be tested until it is totally wired, which makes the correction of errors much more expensive as it generates much more reworking. Providing designers with modeling and verification tools that afford a theoretical support to the design choices would be a good way to reduce verification costs. As pointed by [START_REF] Elisabeth Haxthausen | Comparing Formal Verification Approaches of Interlocking[END_REF], the automated verification of signalling systems design, especially for the interlocking part, is an open research subject for which the challenge is to handle the growing complexity of the systems.

Formal methods are useful mathematical techniques for modelling complex system designed on a logical reasoning because they provide a verification of the consistency and the validity of this reasoning [START_REF] Coudert | Formal Methods for Safe Design of Autonomous Systems dedicated to risk management[END_REF], through proof of properties which requires a precise statement of system's properties. This constraint is the opportunity for the designers to unambiguously specify the essential requirements of the system. These methods offer many advantages, in addition to enhancing confidence in the safety and the efficient functioning of systems; they provide a better automation of design and verification tools. The automated proof can be done in different ways, such as model checking.

As mentioned above, digital systems have not been able to replace electromechanical interlocking. But, before considering a whole transition from so-called "classical" signalling systems to computer-based systems, we can start by modernizing the methods of verification on old technologies. Formal methods could be a way of modernization. The modeling of railway signalling systems would allow doing the verification at the same time as they are designed. Formal methods, such as B method, require this verification through the proof of properties at each refinement. Finally, there is an obvious analogy between the logic of the electromechanical signalling circuits and the Boolean logic, which makes the modeling in formal language quite feasible. This analogy will be explained in section 3.

Formal Methods overview

Formal methods originate in logics which is, to some extent, the science of reasoning.

In ancient time, Aristote characterized well reasoning as succession of sentences respecting precise patterns. It traced the path for the reduction of reasoning to a question of shape that can be verified by machines ignoring semantics. With mathematical logic [START_REF] Krivine | Elements of mathematical logic (model theory)[END_REF], languages are mathematically defined by way of formal syntax. They are provided with mathematical models, i.e. precise non-ambiguous semantics. Then proving patterns are defined on a purely syntactic base. Thus, they can be handled by computer to monitor proving activity. Mathematician proves that these patterns are sound: they only allow proving true things in semantics. It guarantees that proofs using them are sure.

Computer monitoring exclude human error. Of course, provided guarantees are only valid if mathematical models are relevant with respect to real world, which can only be checked by human. Formal methods rely on such kind of foundations. They provide a lot of logical languages and associated computerized tools. They were initially developed to support software engineering [START_REF] Sommerville | Chapter 27. formal methods[END_REF] and enhance software reliability. Nowadays their scope extends to many domains, kind of problems or applications. Their aim is to guarantee the behavior of systems following rigorous approaches. The choice of one method depends, of course, on how the method fits into the development process as a whole. In this paper, we do not describe or classify all the methods. We provide an overview of two approaches used in the railway domain the B method [START_REF] Pearson | Modeling in Event-B: System and Software Engineering[END_REF][START_REF]Modeling in Event-B: System and Software Engineering[END_REF] and model checking method [START_REF] Clarke | Model checking[END_REF].

Both approaches consider state machines as models for mathematical semantics. States are simplified views of snapshots of real world states and state changes in models are "transitions" which can be events, actions, time... depending of approaches. When the number of state is finite, state machines (also called automata) are often graphically represented by graphs with labeled states linked by labeled arrows as transitions. For example, transition labels may express conditions constraining states changes. These models are discrete: state evolves step by step and not continuously and thus modeling of continuous systems requires discretization. Lot of applications can be modeled this way, and complementary approaches [START_REF] Liu | A formal framework for hybrid event b[END_REF][START_REF] Platzer | A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems[END_REF] are available for a more precise handling of continuity.

The B method enables describing machines with a language that allows comprehensive characterizations of transitions and description of properties expected from the system. And then, a support is provided to ensure and exhaustive proof of these properties. Proofs are similar to usual mathematical proof. Tools provide monitoring and assistance to human work. This proof approach can't be fully automated but its power takes benefit of human mining. The second advantage of B method is to offer a fully guaranteed refining process: a way to move from high level models (abstract simple view of application) to low level ones (detailed view of implementation) in a rigorous way. This allows expressing and proving properties on simple and user-level models, and by refinement, to ensure that these properties hold in the final technical implementation of the system. Two variants of this approach exist. The B method is dedicated to software development and in this case, state transitions are calls of software procedures.

It has been widely used for developing certified railway software [START_REF]sil4 railway software[END_REF]. The "Event B" version considers events as transitions and its scope is more generally system modeling, and not only computer or IT domain [START_REF] Fürst | Formal Development of a train control system using event-B. Theses[END_REF].

"Model checking" denotes a family of algorithms offering automated verification for finite-state automata. The principle consists in exploring the model entirely, going through all states, to verify, through logical questions, the validity (or not) of provided expected properties. Thus, it is more proof by exhaustive inventory of cases (states) than a mathematical comprehensive proof (as proofs with B method are). The approach is mathematically sound: proved properties are sure. The advantage is automation, whereas, the limit is the size of the set of states to explore, which must be finite. Model checking is often combined with abstraction techniques (the converse of refinement), which allow to forget details in models which are not significant with respect to properties of interest. Abstraction leads to simpler models, with less state and easier to check. Moreover, computing capacity increased a lot and despite the intrinsic character of complexity, model checking approaches are nowadays relevant for many applications. In the railway domain, a lot of works [START_REF] Elisabeth Haxthausen | Comparing Formal Verification Approaches of Interlocking[END_REF][START_REF] Busard | Verification of railway interlocking systems[END_REF][START_REF] Vu | Formal modelling and verification of interlocking systems featuring sequential release[END_REF][START_REF] Haxthausen | On the Use of Static Checking in the Verification of Interlocking Systems[END_REF][START_REF] Benerecetti | Dynamic state machines for modelling railway control systems[END_REF]) studies how to apply them to the interlocking problems, which is hard to solve by a general comprehensive reasoning.

Model checking and comprehensive proof are not exclusive. For example, the second can take benefit of the first to prove some intermediate results (lemmas), and conversely. Expertise leads to choose the most efficient approaches depending on the properties to prove. A domain specific methodology may provide support to help such choices and combine results. Such a methodology may also give access to the numerous theoretical and concrete primitive and tools allowing to decompose problems and specifications in order to make proof and verification simpler following the "divide and conquer" idea. Refinement and abstraction are part of this structuring toolkit. Even though no complete methodology exists for railway, as pointed by Author's name [START_REF] Sommerville | Chapter 27. formal methods[END_REF], formal methods have been applied for years in railway domain; a proof of this is the fact that European Standards CENELEC [START_REF]Standard NF EN 50128 Railway applications. Communication, signalling and processing systems[END_REF] applicable for development of software in railway control system requires the use of formal methods for specification, design and V&V activities for software of the highest safety and integrity level 4

Railway infrastructure modelling example

A railway signalling network is composed of different electrical equipment mainly: points, shunting signals and train detection devices. Basically, a track layout consists of, at least, two tracks and it can include many routes. A route delimits the space between two signals, it is a succession of sections to be traversed, and these sections could be points. A point is a convergence spot between two tracks; it is locked in a position allowing either to traverse a route in one track, or to traverse a junction route between two tracks. A signal can be open or closed, authorizing or banning downstream the traversing of the transit zones (route). In railway signalling, an interlocking [START_REF] Rétiveau | La signalisation fériovaire[END_REF] physically bans the handling of signals and equipment under any condition incompatible with the traffic safety.

The main purpose of a signalling system is to open a signal if all the conditions that allows the driver to cross it are satisfied and to close it, if, at least, one condition is missing. In order to do so, information has to be exchanged. This information is classified into two types: Supervisor's commands and local information. A supervisor is in charge of the control of the signalling system, he gives commands, for example route setting, via a user interface. On the other hand, local information gives the state of the track, for example, the position of the points, the presence of a train, etc.

In hard-wired logic systems, the signalling functions for a given network layout, are described in two complementary documents: functional diagrams and scheme plans. Both must be modeled for using a rigorous approach employing formal methods. The relationship between logic and functional diagrams is simple and direct, so we will explain it in this section. The relationship is less trivial with scheme plans and it brings some methodological questions, thus, we will only give explanations about the methodologies of the domain, in this section, and the formalization will be detailed in the following section.

Functional diagrams

Functional diagrams are relay logic circuits, i.e. electrical networks that control outputs. A function (or an output) is materialized by an electromagnetic coil and controlled by a combination of conditions represented by relays connected in series or in parallel. The set of all the functional diagrams represents the global behavior of the signalling. The coil SIG belongs to two circuits, it is energized when one of them is closed. The relays that close the circuits are the images of the state of equipment on the field. The first circuit represents one route downstream the signal A, it closes if the relays "Section 1", "Section 2", "Section 3" are closed, which means that, on the field, every section of the route downstream the signal are free (the track is clear), and if the relay "Point" is on a position that corresponds to the Left position of the point traversed by the route. The second circuit represents another route downstream the signal, it closes if the relays "Section 4", "Section 5", "Section 6" are closed and the relay "Point" is on a position that corresponds to the Right position of the point traversed by the route.

The functional diagram Fig. 1 can easily be transcribed in a logical diagram, as shown in the Fig. 2 below. Using the logical diagram on Fig. 2, we can describe the function "Coil SIG" through Boolean logic, as showed by the following table (table 1).

With Boolean logic, le function "Coil SIG" is described by the equation below:

S = (A and B and C) or ((Not A) and E and F and G) (1)

This example shows how the analogy between functional diagrams and logical diagram is perfectly viable. Because they have been conceived for computer science, formal methods are suitable for signalling principles.

Scheme plans of the example

Scheme plans comprises a track plan and various tables, among them control tables [START_REF] Elisabeth Haxthausen | Comparing Formal Verification Approaches of Interlocking[END_REF].

A track plan is a graphical representation of all the railway tracks in a station and control tables specify, for each route in the network layout, all the conditions for setting this route. The figure 3 is an example of a track layout plan. It contains one point PT1 that links the track 1 and the track 2. In the case of this example, the train detection devices are axle counters. An axle counting section is marked out by at least two counting heads (CH). When a train traverses one of the counting heads which marks out a section, the number of axles of the train is recorded. This section is considered occupied until the same number of axles passes the counting head at the exit of the section. For example, the ACS1 section is marked out by the counting heads CH1 and CH3, depending on the direction of the train, each of these could be an entrance or exit point of the section. The ACS3 section is marked out by the counting heads CH3, CH5 and CH0. When the train runs the route from A to B, the counting head CH3 will be the entrance point and the CH5 will be the exit point. Whereas, for the route from D to A, the CH0 will be the entrance point and CH3 will be the exit point. The two vertical and parallel lines connecting the two switch blades of the PT1 point represent the "fouling point limit", that is to say, the limit zone where a train can stop without approaching the convergent track gauge. Furthermore, in this example, the PT1 point is a trailable and reversible point. In opposition to motorized points which receive a point's electrical command (CPT) sent by the signalling system; in a position depending on the route's direction, a trailable and a reversible point turns in a position depending on the occupied heel section. When a route traverses it in a facing mode (which is case of the routes DC and DA), the point is positioned through a manual command, by an authorized operator, at a building site respecting the safety conditions. In the case of the PT1 point:

-If the ACS2 section is occupied through the traversing of the CH2 counting head: the point turns Left. -If the ACS3 section is occupied through the traversing of the CH3 counting head: the point turns Right. -The default position of the point is to the Left (represented by the small line under the point).

A signalling system, for the track layout Fig. 3, must ensure the following safety features: -Avoid collisions between trains going the same direction by prohibiting the opening of a signal if a section of the route is occupied, -Avoid collisions between trains going in two opposite directions on the same track (face to face), by prohibiting the simultaneous opening of incompatible signals, -Avoid collisions between trains taking conflicting routes, by prohibiting the simultaneous opening of conflicting signals.

The track table below (Table 2) inventories, for each route of the track layout, all the conditions required to open the signal upstream the route. The events that can change the state of the system are:

1. The supervisor sets a route: which can open the signal upstream the route if all the sections of the route are free and all the conflicting routes are destroyed 2. The supervisor destroys a route: which closes the signal upstream the route 3. A train traverses a counting head: which can occupy or release a section. if it occupies a section and if this section is a heel section of the point PT1, the point will turn to the corresponding position

In design offices, the verification of the two documents (functional diagrams and scheme plans) consists in checking manually and thoroughly that all the conditions described in track tables are met by the system's behavior described in functional diagrams and also, checking that the track tables are complete according to the track layout plan. This verification could be automated using model checking, this is the topic of the following section.

Formalisation

In the scientific literature, there is many examples that confirms the suitability of model checking for the modeling of interlocking systems. Nevertheless, this method is not that easy to implement. In fact, its application can be tedious if the system is complex and it is based on the quality of the modeling which depends on human expertise. This is what we want to illustrate, in this section, by giving an overview of what can be done with model checking, and then, by justifying the importance of rigorous methodological complements.

Model checking for interlocking

To create a formal model of the system, we need to define abstract states. We use a current way to do this: we provide a finite state of state variables. A state is fully characterized by the values of these variables. Choosing relevant variables is an important aspect of modeling: they define an abstraction and they must allow to describe the system and to express the expected property with respect to this abstraction. In our pedagogical example, they must allow to represent concepts and ideas expressed in table 2, figure 3 and event description in the previous section. We choose to represent the signals, the axle count sections, a generic OUTSIDE section, the point and the routes: -Signal_A, Signal_B, Signal_C, Signal_D accept OPEN or CLOSED as value -Section_1, Section_2, Section_3, Section_4, Section_6, OUTSIDE accept BUSY or FREE as values -Point accepts LEFT or RIGHT as values -Route_AB, Route_AC, Route_BA, Route_DA, Route_CD, Route_DC accept SET or UNSET as values.

Then the temporal behavior of the system must be rigorously described in a methodical way. Various languages are usable depending on tools and formalisms. Here we use events described by two aspects: the way they modify the state and the conditions under which they can happen. Description must not only reflet reality but also provide all information required to prove the expected property, although we omit or abstract some (train direction for example), here, to simplify presentation. The three events of section X become are methodically described and something must be added to make train appear: a new event "New".

- Tools are able to build automaton from such descriptions. The single additional information they need is an initial state. They compute the set of all reachable states by successions of events, and these events are the transitions. Figure 4 A model checking algorithm can then automatically explore the entire automaton to verify formally expressed properties. In our case, we don't want two trains to be on the same section at the same time, thus we could require that each time a train enters a section (except OUTSIDE), the section is free. More formally: if two states in automaton are linked by a "Trav(S,S')" transition, then S' is FREE in the source one, which can be obviously checked by an exhaustive exploration. If checking fails, a counterexample is generally provided to help the designer to find the error. In our example, signals remain open after a train passed them which compromise the expected property.

The suit "set(AB);trav(Out,1);trav(Out,1)" is a counterexample as shown on figure 4.

Errors can be errors in the real system. They can be also errors in the model, when for example the specifier forget some implicit information and allows then behaviors that do not exist in real world. This shows how the demand of proof helps to correct errors and construct safe solutions ( [START_REF] Fehnker | Refining abstractions of hybrid systems using counterexample fragments[END_REF]). The model checking avoids the risk of human error or oblivion in complex verifying. However, even if a formal verification is not susceptible to errors of reasoning, it is susceptible to errors of modeling. This is what we will explain in what follows.

Human impact

Formal approaches appeal to human expertise for various reasons. First, to avoid unnecessary complexity and to obtain optimized models, easier to implement. In fact, choosing the right variables and the right abstractions limits the number of states, in the model checking, and reduces the number of proofs. Else, the properties checked must, above all, be relevant vis-a-vis the real problems. The model must reflect the system, and the properties expressed in mathematical language must correspond to the properties that the system should ensure. For the example above, the model must reflect the signalling system's behavior described in functional diagrams and the properties checked must be conform to the track tables. In some other areas, such as software engineering, there are design environments with graphical interfaces and various tools that help the test and visual verification of specifications. For the field of railway transport, whose experts are less accustomed to formal ratings than in computer science, such assistance is even more necessary. However, even if the methodologies used in design offices are informal, they are based on standards that provide a framework, with well-defined processes and nomenclatures, which could facilitate the formal modeling. The specification of the signalling system, in the example above, is based on a strong hypothesis: "two trains cannot clash if they are in two different sections". This hypothesis is true with a fixed length of trains. But, if the length grows up, the hypothesis become invalidated. Indeed, when the DA route is set (the PT1 point is previously positioned to the Right), a train (Train 1) will traverse the ACS6 section and then the ACS4 section and when the counting head CH21 counts out the last axle, the ACS4 section will be released and the ACS3 section will then be occupied. If the train stops right before passing the counting head CH21, we will be facing a problem. If the supervisor destroys the DA route and sets the CD route, another train (Train 2) could enter the point section ACS4 (left heel). Since the distance between the two tracks (track 1 and 2) is small, it is possible that the second train strikes the rear of the first train (See figure 5). This error would never have been detected by a model checker with the model defined in the previous section.

Formal methods must be used carefully and cannot replace human judgment; it shows the importance of the specification phase. In fact, to obtain a viable and exhaustive model, the system's features should be expressed precisely and for this case of study, the property that is missing from the requirements is that we should not have the sections ACS3 and ACS4 busy at the same time, if the point PT1 is on the right position.

Fig. 5. Example of track plan (accident case)

The presented reasoning is based on a hypothesis: two train on different sections can't collide together. It is the base of block signal systems which has been used in railway development for a long time (long before formalization) to facilitate the design of safe interlocking. Historically, blocks exactly corresponded to physical sections. The modeling for model checking proposed above depends on this. But, as explained in section 2, railway evolves. It is more and more demanding and static block systems limits optimizations and performances. Thus, practices in the domain have also evolved from static to dynamic block systems. Now blocks do not always correspond to physical sections. They are virtual: they can comprise several sections and they can change over time. In our example, ACS3 and ACS4 should be a single block, precisely when PT1 is on the right direction. A simpler solution would have been to forbid the opening of the signal SC when the ACS3 section is occupied. This makes the routes CD and BA incompatible and we have then virtual static blocks. But this compromise is restrictive and would significantly decrease operations.

Experts of railway signaling are able to propose technical solutions to implement the dynamic model of block systems, using new equipment and technologies. As block system principles remains, the new reasoning model is quite similar to the previous one but more complex. Formal modeling may be adapted by adding state variables to characterize dynamic blocks and new events to describe the behavior of new equipment. Then their complexity increases too. Adding custom modifying to existing solutions can progressively lead to useless complexity. Thus, when reasoning paradigms evolves too much, it is required to reconsider in more depth the model, choosing new abstractions and variables in order to recover simplicity. Experience resulting from previous modelling generally makes the developing of new ones much faster, as a lot of ideas remains relevant although they are not always applied in the same way.

This example shows how it is possible to improve operations by creating new signaling principles. To verify and validate new principles, designers need reliable tools and methodologies to prove the safety of their innovative solutions. Formal methods could provide those tools and methodologies. For this, new expertise in formal methods is required. This difficulty can be overcome by simple consensus, for example the verification of the correspondence between the track tables and track layout plans can still be the task of signaling experts and the formal modeling be assigned to staff trained on the formal methods. In addition, providing intuitive graphical modeling tools could be a way for signaling experts to participate concretely to formal methods implementation.

Conclusion

In this paper, the application of formal methods for the design and the verification of railway signalling systems has been discussed. Considering the evolution of railway technologies and the need for increasingly efficient systems and operations, the usual means of verification are no longer appropriate. Formal methods provide solutions to deal with this context. These solutions have been detailed, as well as the reasons why a modeling a mathematical modeling of a railway system is perfectly feasible. First, an overview of formal methods has been given, focusing on two of the most widely used formal methods: B Method and Model Checking method. Next, the analogy between Boolean functions and functional diagrams has been described. Then, through an example of a track layout, the modeling process using model checking has been detailed. This example showed a way to define abstract variables to build an abstract model, in order to automate verification using algorithms of model checking. Those algorithms are not totally resistant to human errors; they are susceptible to errors of modelling. This has been illustrated by a case of accident due to equipment evolution that has not been taken into account in the model. This case allows to make a fundamental point: using formal methods does not free from the human factor. Human expertise, in the field of signaling as well as in the use of formal methods, is essential. Finally, a discussion about the way to organize a verification work by combining railway signalling expertise and formal methods knowledge, has highlighted the need for providing adapted tools dedicated to railway professions.

Fig. 1 .

 1 Fig. 1. Functional Diagram of Railway infrastructure example.

Fig. 2 .

 2 Fig. 2. Logical Diagram issue of Functional Diagram of Railway infrastructure example.

Fig. 3 .

 3 Fig. 3. Track plan corresponding to the infrastructure example.

  Set(R): set the route R. Conditions: associates sections are FREE and conflicting routes are UNSET. Modifying: Signal opening the route becomes OPEN -Unset(R) : unset the route R. Conditions: none. Modifying: Signal opening the route becomes CLOSED -Trav(S,S'): traverse counting head between sections S and S'. Conditions: S is BUSY and if S is OUTSIDE, then the signal associated to S' is OPEN. Modifying: S becomes FREE and S' becomes BUSY. If S' is Section_3 or Section_4, Point becomes LEFT OR RIGHT, following indications provided in previous informal description. -New: a train appears. Conditions: none. Modifying: OUTSIDE becomes BUSY.

Fig. 4 .

 4 Fig. 4. Partial graph of studied system

Table 1 .

 1 "Coil SIG" description.

	Function	Symbol	Boolean values
	Coil SIG	S	Energized (1), Not Energized (0)
	Position of the point	A	Left (1), Right (0)
	Section 1	B	Free (1), Buzy (0)
	Section 2	C	Free (1), Buzy (0)
	Section 3	D	Free (1), Buzy (0)
	Section 4	E	Free (1), Buzy (0)
	Section 5	F	Free (1), Buzy (0)
	Section 6	G	Free (1), Buzy (0)

Table 2 .

 2 Track table.

		Route's characteristics		Conditions
	Signal Setted	Departure Arrival	Points'	Released	Destroyed	Destroyed
		Route			position	sections	incompatible	conflicting
							routes	routes
	SA	AD	CH1	CH26	PT1 :	ACS1,	DA	BA, CD
					Right	ACS3,
						ACS4, ACS6
		AB	CH1	CH15	PT1 :	ACS1, ACS3 BA	DA
					Left
	SB	BA	CH5	CH11	PT1 :	ACS3, ACS1 AB	DA
					Left
	SD	DC	CH6	CH22	PT1 :	ACS6,	CD	AD, DA
					Left	ACS4, ACS2
		DA	CH6	CH11	PT1 :	ACS6,	AD	CD, BA
					Right	ACS4,
						ACS3, ACS1
	SC	CD	CH2	CH28	PT1 :	ACS2,	DC	AD
					Left	ACS4, ACS6

Formal Methods for Railway Disasters Prevention

Lilia Belabed 1,2 , Tullio Joseph Tanzi 1 and Sophie Coudert


Ronny Chevalier

David Plaquin

Guillaume Hiet

Intrusion Survivability for Commodity Operating Systems and Services: A Work in Progress

Keywords: Intrusion Tolerance, Intrusion Recovery, Survivability, Resiliency, Intrusion Response, Availability

This paper presents a work-in-progress of our approach for intrusion survivability in commodity operating systems. Our approach relies on an orchestration of recovery and mitigation actions. We rollback infected services (i.e., their processes) and infected files to a previous known safe state, and we apply per-service mitigations (i.e., privileges removal) before unfreezing the restored processes. Such approach effectively puts the previously compromised service into a degraded mode, allowing the system to withstand ongoing intrusions and ensures the availability of core functions to the users. A prototype for Linux-based systems is currently in development.

I. INTRODUCTION

Organizations rely on the security of their computing platforms, such as laptops, servers, or phones, to operate properly and to provide services to their users in an uninterrupted manner. Despite progress in computer security (e.g., cryptography, coding practices, hardware protections, or access controls) to reduce the likelihood of an intrusion impacting those platforms, given time, an intrusion will eventually occur. Such case may happen due to technical reasons (e.g., a misconfiguration, a system not updated, or an unknown vulnerability) and economic reasons [START_REF] Kshetri | The simple economics of cybercrimes[END_REF].

To limit the damage done by intrusions, intrusion recovery systems help administrators to restore a compromised system in a sane state. One common limitation, however, affecting prior work [START_REF] Xiong | Shelf: Preserving business continuity and availability in an intrusion recovery system[END_REF][START_REF] Goel | The taser intrusion recovery system[END_REF][START_REF] Kim | Intrusion recovery using selective re-execution[END_REF][START_REF] Hsu | Back to the future: A framework for automatic malware removal and system repair[END_REF], is that they stop neither the intrusion from reoccurring nor the attackers from achieving their goals (e.g., data integrity violation). If the recovery system manages to restore the system in a sane state, the system continues to run with the same vulnerabilities and nothing stops attackers to reinfect it and to accomplish their goals. Thus, the system could enter in a loop of infections and recoveries.

Our work aims at designing a system able to withstand ongoing intrusions and to allow business continuity despite the presence of an active adversary. We focus on the implementation of an architecture to provide intrusion survivability in commodity Operating Systems (OS) and their services. In particular, our approach relies on two components: service recovery and threat mitigation.

One key point of our approach is that after an intrusion is detected, it puts the system into a degraded mode following a predefined policy. Some non-essential functions of a service are no longer available due to some mitigations applied, while core functions are still operating (e.g., a core function of web server would be to always provide read access to a website). The goal here is to recover infected services and to put them in a degraded mode with fewer privileges to ensure the integrity of the OS despite the presence of an adversary, while providing availability of core functions of the service. Such degraded mode allows the system to mitigate the threat and to provide business continuity, since users of the system still have access to the essential functions. Thus, it gives time for administrators to plan an update of the system to fix the vulnerability, and potentially to wait for a patch to be released if necessary.

Our work relies on existing work in Intrusion Detection Systems (IDS) and malware characterization, but our contributions concentrate on the ability to recover from and withstand ongoing intrusions, while providing availability to core functions of a system. This work is part of a broader approach to achieve survivability for a whole platform (i.e., its hardware, firmware, and OS). Previously, we worked on intrusion detection, and more specifically, on improving the security of firmware [START_REF] Chevalier | Co-processor-based behavior monitoring: Application to the detection of attacks against the system management mode[END_REF].

The rest of this document is structured as follows. First, in section II, we mention related concepts about our work, and we review state-of-the-art work on intrusion recovery systems. Then, in section III, we provide a more detailed description of our approach. In section IV, we describe the current state of our proof-of-concept. Finally, we give the next steps regarding our work-in-progress in section V.

II. RELATED WORK

In this section, we first discuss related concepts close to our work such as dependability, resiliency, or survivability. Then, we review existing work on intrusion recovery systems.

A. Concepts

Laprie [START_REF] Laprie | From dependability to resilience[END_REF] defined the concept of resilience as "the persistence of dependability when facing changes", where dependability is "the ability of a system to avoid service failures that are more frequent or more severe than is acceptable" [START_REF] Avizienis | Basic concepts and taxonomy of dependable and secure computing[END_REF].

Avizienis et al. [START_REF] Avizienis | Basic concepts and taxonomy of dependable and secure computing[END_REF] suggested that dependability and survivability (based on an earlier definition [START_REF] Ellison | Survivable network systems: An emerging discipline[END_REF]) were similar concepts. Knight et al. [START_REF] Knight | Towards a rigorous definition of information system survivability[END_REF] weighed that survivability distance itself from dependability, since it should encompass the notion of degraded service, and a trade-off between the availability of some functions and the cost to maintain and provide them.

Thus, from these concepts, we consider our work closer to survivability. More specifically intrusion survivability, since our approach focuses on withstanding ongoing intrusions and does so by service degradation. In our trade-off, the cost to provide some core functions without applying some mitigations represents a security risk on the system.

To achieve dependability, resiliency, survivability, or other close concepts, four categories of techniques exist: fault prevention, fault tolerance, fault removal, or fault forecasting [START_REF] Avizienis | Basic concepts and taxonomy of dependable and secure computing[END_REF]. In our case, we focus on fault tolerance, since we use recovery techniques to roll back the state of objects in the system, and we isolate recovered services by applying mitigations.

B. Intrusion Recovery Systems

Intrusion recovery systems [START_REF] Xiong | Shelf: Preserving business continuity and availability in an intrusion recovery system[END_REF][START_REF] Goel | The taser intrusion recovery system[END_REF][START_REF] Kim | Intrusion recovery using selective re-execution[END_REF][START_REF] Hsu | Back to the future: A framework for automatic malware removal and system repair[END_REF] focus on system integrity by recovering legitimate persistent data. Except for SHELF [START_REF] Xiong | Shelf: Preserving business continuity and availability in an intrusion recovery system[END_REF], they do not preserve availability since their restore procedure either forces a system shutdown or it does not record the state of the processes. These systems log all system events to later replay legitimate operations [START_REF] Xiong | Shelf: Preserving business continuity and availability in an intrusion recovery system[END_REF][START_REF] Goel | The taser intrusion recovery system[END_REF][START_REF] Kim | Intrusion recovery using selective re-execution[END_REF] or rollback illegitimate ones [START_REF] Hsu | Back to the future: A framework for automatic malware removal and system repair[END_REF], thus providing a fine-grained recovery. However, they generate gigabytes of logs per day inducing a high storage cost.

Most related to our work is SHELF [START_REF] Xiong | Shelf: Preserving business continuity and availability in an intrusion recovery system[END_REF]. SHELF is an intrusion recovery system focusing on business continuity able to recover the state of processes while performing damage assessment. It performs periodic asynchronous snapshots of files and process states on the system. It keeps a log of system call events and it uses dependency tracking to perform damage assessment when the IDS notifies it of an intrusion. During recovery, SHELF quarantined infected objects by freezing processes or forbidding access to files. However, such quarantined state is removed as soon as the system is restored.

One common limitation affecting prior work is that they prevent neither the attacker from reinfecting the system nor the attackers from achieving their goals (e.g., data theft, integrity violation, or propagation) when successfully reinfecting the system. They rely on the implicit assumption that after the recovery the attacker will stop attacking the system, that the vulnerability is fixed, or that the cost of the recovery is negligible. Unfortunately, these assumptions do not necessarily hold even if an intrusion is detected and recovered from. A worst-case scenario could be a loop of infections and recoveries impacting the availability of the services.

III. APPROACH DESCRIPTION

In this section, we describe the assumptions made and the different components of our approach, illustrated in Figure 1.

A. Intrusion Detection

Since our work focuses on intrusion survivability, we assume an IDS able to detect intrusions on the system and able to associate such intrusion to a specific service in the OS (e.g., a web server or an SMB server). After the IDS detected an intrusion, it notifies the recovery and mitigation system about which service is infected in the OS and what are the potential characteristics and attributes of the intrusion.

For the attributes of the intrusion, we rely on the Malware Attribute Enumeration and Characterization (MAEC) [START_REF] Kirillov | Malware Attribute Enumeration and Characterization[END_REF] and Structured Threat Information eXpression (STIX) [START_REF] Barnum | Standardizing cyber threat intelligence information with the Structured Threat Information eXpression (STIX)[END_REF] standard languages. These languages are used to encode threat information, such as malware attributes, behaviors, artifacts, or attack patterns.

B. Recovery and Mitigation

After the recovery and mitigation system received the notification from the IDS, it recovers as soon as possible the core functions of the system to maintain business continuity. The procedure must meet the following goals: maintain core functions, mitigate the threat, and restore infected objects (e.g., files and processes).

These goals are achieved using an orchestration of recovery and mitigations actions. A recovery action restores the state of a service (i.e., the state of its processes and metadata describing the service), a file, or a filesystem to a previous known safe state. A mitigation action removes privileges or isolate components of the system from the service according to the MAEC and STIX information provided by the IDS. Such mitigation either stops the service from being reinfected or stops attackers from achieving their goals (e.g., data theft or data integrity violation). After a mitigation is applied, however, not only the attackers but the service is restricted in its capacity. It effectively puts the system in a degraded mode, because some functions are not available anymore.

In order to perform recovery actions, we create periodic snapshots of the filesystem and the services, during the normal operation of the OS. In addition, we log all the files modified by the monitored services. Hence, when restoring infected services, we only restore the files they modified.

For example, let us consider a web server infected by some ransomware. After being notified, our mechanism restores the infected processes to a previous known safe state (preinfection), and it restores all the files modified by the service since the last snapshot. In addition, before unfreezing the service, it degrades the state and applies a mitigation removing the write access privilege of the service to the filesystem. Here we achieve multiple goals: we restore the data, we continue to provide access to the web server, and we stop a reinfection from having any impact.

C. Policy

Our approach relies on policies describing a set of constraints of what can be and cannot be done for each service. Such policies help to maintain the availability of core functions of the services and provide flexibility to fit the different needs depending on the context of the system. A server, a desktop, or an embedded system have different constraints due to the different functions they provide. Hence, some mitigations or recovery actions should not be attempted due to their availability cost. The goal is to provide a trade-off between the availability of a function in a service and the security risk due to an intrusion that could benefit from the absence of some mitigations.

In our previous example with a web server, one constraint was that the server always has read access on the filesystem. Another constraint could have been that the service has always write access to a specific directory in the filesystem. Thus, the writer of the policy accepts the risk that in case of an infection such directory might be compromised.

IV. PROOF OF CONCEPT

In this section, we describe the work we started on the development of a proof-of-concept for Linux-based systems. Since this is still a work-in-progress, not all the aspects described in section III are implemented. In addition, we give a brief overview of some limitations of our current work.

A. Current state

We use CRIU [START_REF]CRIU[END_REF], a checkpoint and restore project implemented in userspace for Linux, mainly developed to perform the checkpointing and restoring containers. In addition, we use snapper [START_REF]Snapper, the ultimate snapshot tool for linux[END_REF] to perform snapshots of the filesystem and to fetch previous versions of files when restoring.

We modified systemd [START_REF]systemd system and service manager[END_REF], a system and service manager for Linux-based systems, to checkpoint and restore services with the help of CRIU and snapper. We perform periodic atomic snapshots of the monitored services (i.e., their processes and service metadata) and the filesystem, by freezing their processes (i.e., they are removed from the scheduling queue) during the checkpointing procedure, thus avoiding any inconsistencies.

Finally, we modified systemd and CRIU to apply mitigations when restoring an infected service, before unfreezing the processes. We use seccomp [START_REF] Corbet | Seccomp and sandboxing[END_REF] to filter system calls and we apply Linux namespaces [START_REF] Kerrisk | Namespaces in operation, part 1: namespaces overview[END_REF] to isolate or remove access of parts of the system (e.g., files or devices) from the service.

B. Limitations

The periodic snapshot of the services we monitor requires freezing their processes to avoid any inconsistency during the procedure. Hence, services will be longer to respond to any request made by a user during the snapshotting procedure.

If a process has opened a device to have direct access to some hardware, checkpointing its state may not be possible (except for virtual or pseudo devices not corresponding to any physical devices). This technical limitation is because we cannot be sure that when the process is restored, the physical device (e.g., a printer) has the same state as when the process was checkpointed. One would need a standard interface to control the state of such devices in a generic way. Finally, even if there was such interface, restoring its state may create inconsistencies with other users of the device.

V. FUTURE WORK

We are currently developing a proof-of-concept implementation of our approach for Linux-based systems. When finished, we plan to evaluate the performance impact during normal system workload and when an intrusion is detected, to evaluate its efficacy against different attacks, and to evaluate its efficacy to maintain the availability of core functions. After, we would like to investigate how, based on our current work, we could adapt the system to gradually remove the mitigations and achieve an optimal number of recovered functions.