-
Notifications
You must be signed in to change notification settings - Fork 0
/
Introduction.tex
146 lines (86 loc) · 20.2 KB
/
Introduction.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
\thesischapter{Introduction}{Introduction}
This thesis is concerned with the application of formal methods within the Railway Domain and to the tools used when applying formal methods themselves. Firstly we present a new approach to develop verified SAT solving algorithms, which have been applied to the verification of a real world train control system: the solid state interlocking. Secondly we present an approach to formalise and model the European Rail Traffic Management System (ERTMS), in such a way as to capture the performance of the system and also apply a model checker to verify the system's safety. We hope that by capturing these performance properties, such as the speed of trains, we will be able to measure the capacity of different implementations of the system in the future.
\section{Motivation}
A major problem facing those who design and develop computer systems today is that of designing and implementing such systems correctly. The answer to this problem is more elusive than it may seem initially due to the underlying complexity of modern systems. The process of checking that a system meets its specification is called \emph{verification}. In industry the most widely used means to verify both hardware and software systems is testing. This checks that for a given input the output of the system is correct with regards to the specification. The biggest downfall of testing is that it is typically used in a \emph{non-exhaustive} manner, due to the fact that most modern systems have a large number of inputs which makes testing each possible combination is not feasible. This problem is further compounded when several systems are operating in parallel and communicating with each other.
One of the most famous and costly errors to occur was that of the Ariane 5 flight 501\cite{GL97}. A 64-bit floating point number representing horizontal velocity was converted into an 16-bit signed integer resulting in an overflow and a hardware exception being raised. The control system interpreted the hardware exception as position and velocity data which lead it to fly on a self destructive trajectory. Another example of a flawed computer system is "Chip and PIN" smart cards secured by the EMV protocol \cite{JM10}. It is supposed to be the case that only someone with the 4 digit personal identification number (PIN) can make payments with the cards, however it is possible for a fraudster to perform a man-in-the-middle attack and to trick the terminal into believing the PIN was correctly entered when no PIN was entered at all. With over 730 million smart cards in circulation this poses a significant threat to the security of many peoples finances. Both of these problems were avoidable. In the case of the Ariane rocket all that would have been required was an extra line of code or two to prevent the variable over-flowing. Many other variables in the code had been protected against over-flow in this way; it was simply over looked in the case of this particular variable.
Formal methods are a group of approaches that capture certain aspects of the development process with a logical and mathematical basis. This thesis is mostly concerned with \emph{formal verification}, which uses logic and formal reasoning to prove that a program meets its specification, and \emph{formal specification}, which attempts to capture the behaviour of the program in a logic or language with a logical underpinning. The advantage of using formal verification in combination with formal specification is that one can prove that a system satisfies its specification for all inputs in an \emph{exhaustive} manner. These formal methods however do not make testing redundant, for example, e.g. would you rather fly a plane that has been formally verified and never tested or a plane that has been heavily tested but not verified? Formal verification will only check that a system is correct with respect to its specification. There is the question of whether the specification itself is also correct. Testing can validate the system i.e. show that the plane we have made really functions as a plane. Another problem is that manual formal verification requires a large amount of technical ability to perform and in addition is time consuming. There are a number of automatic verification techniques, however these are typically not complete in the sense that they are not guaranteed to produce an output for every possible input. One area that automatic techniques do perform well in is verifying large but logically un-complex systems, which do occur in industry. It is also beneficial if these systems are part of a product line. If that is the case then a customised verification approach may be developed that exploits similarities between individual implementations of the system.
One such automatic verification technique is \emph{model checking} which attempts to exhaustively search the state space of the system and check that a safety property holds in each individual state. This can be done by formulating the model checking problem as a Boolean satisfaction problem and then applying a SAT solver to do the search. These SAT solvers have the advantage that they are highly optimised and are typically faster at solving any Boolean satisfaction problem, without any problem specific customisation, than any proprietary software. However, low level and complex nature of many SAT solver optimisations makes it harder to reason about the solver's correctness. This causes a problem when such solvers are used in a safety critical environment where their results must be trustworthy. Besides the correctness also
totality (or universality) of SAT solvers is an issue. For example, in the 2012 SAT competition (www.smtcomp.org) many systems were not total in the sense that they returned
"Unknown" for certain inputs signifying that they could not deal with the given problem. There are also numerous specialised model checking algorithms, each of which, is geared towards solving a specific type of problem and comes with their own unique optimisations.
Another approach to formal verification is that of interactive theorem proving \cite{HG09,SSD06} where a tool aids with the human driven construction of a formal proof of correctness for a system. These tools have the advantage that the machine can check the human produced proof and they typically include a number of built in tactics that aid in the construction of a proof. Some interactive theorem provers realise the Curry-Howard correspondence \cite{HC34, HC58, WH80} which states that constructive proofs performed using the natural deduction calculus can be viewed as programs in the lambda calculus. The process of exploiting this correspondence to produce a program from a proof is called \emph{program extraction}. This technique allows for the development of programs that are correct by construction as the program comes with a proof that certifies its correctness. The Minlog theorem prover comes with a number specialisations for the purpose of extracting programs from formal proofs.
The Railway Verification Group at the Computer Science Department of Swansea University (\url{http://www.cs.swan.ac.uk/Rail/}) has been researching the development of formal methods for use in real world situations in particular for the development of train control systems. The majority of this work has been in the form of an industrial collaboration with our partner Siemens Rail Automation (UK). Siemens are continuously modernising and improving their development processes and as a part of this are looking to use formal methods for the development of their systems. The Westrace interlocking is one such system that is being considered for treatment by formal methods. These interlockings have the benefits of being large but relatively un-complex and each one has to comply to the same range of safety requirements. Another product currently under development by Siemens Rail Automation is the European Rail Traffic Management System (ERTMS). This system is developed to a European standard with each country or individual company producing their own implementation. Since the specification is loose and allows for a wide range for implementations this makes modelling of the system desirable to understand possible behaviours and to ensure safe integration with existing infrastructure. Furthermore, it is an open field when it comes to substantiating the claim that the ERTMS approach offers a higher performance of the railway compared to the traditional control systems.
\section{Results of the Thesis}
The first result of this thesis (Chapter 4/5) is the use of program extraction to obtain a verified DPLL SAT solving algorithm that can solve industrial sized problems in the form of verifying solid state interlockings following the approach set out in \cite{AL14a}. We have named the resulting SAT solver XSAT and show that its performance is comparable with other verified SAT algorithms. This case study opens up a new area of application for program extraction to obtain verified SAT and resolution algorithms and has been published in \cite{AL12,AL14b}. This is one of the largest case studies so far in the area of program extraction and demonstrates that the technique can be used for practical purposes. One argument against the use of program extraction is that one loses control over the efficiency of the program. We have demonstrated that it is possible to carry out efficiency considerations at the proof level and therefore obtain a more efficient extracted program.
As a next result, we show that it is possible to modify the SAT proof system and extract a more advanced SAT algorithm that implements an optimisation called clause learning. Finally, we demonstrate that it is possible to extract a resolution algorithm based on our original DPLL SAT solver (See end of Chapter 4).
The final set of results of this thesis is the modelling of the European Rail Traffic Management System and verification of its safety and performance using Real Time Maude. First, we formalised the ERTMS system, controlling an example railway in the form of a pentagon, as several hybrid automata in order to capture its behaviour. This pentagon case study along with a small junction case study were then modelled as Real Time Maude specifications. In our model, speed, acceleration, braking behaviour and track length are integral parts, as even safety cannot be decided without these properties. The inclusion of these properties in the model enables the performance of this system to be analysed by executing the Real Time Maude specifications. This is also the first formalisation of ERTMS to capture the interlocking, radio block processor, train and the communications between them. The interface between the interlocking and the radio block processor, in particular, has yet to be examined in detail even though it plays a crucial role in the safety of the overall system.
\section{Publications}
The results in this thesis have been published in the following articles:
\textbf{\ul{1. Extracting a DPLL Algorithm} (with Berger and Seisenberger), MFPS 2012, \cite{AL12}}
The formalisation of the DPLL proof system and its completeness are described along with the use of non-computational quantifiers to optimise the extracted program. The extracted program is run as a term inside the Minlog system on pigeon hole formulae.
\textbf{\ul{2. Extracting Verified Decision Procedures: DPLL and Resolution} (with Berger, Nordval Forsberg and Seisenberger), LMCS \cite{AL14b}}
This paper is an extension of \cite{AL12}. We extract a resolution solver based on the DPLL solver by showing that DPLL derivability implies derivability in the resolution proof calculus. The extracted program was translated into the function programming language Haskell and a comparison was performed with another verified SAT solver Versat and the industrial tool SCADE. The extracted solver was additionally applied to the verification of solid state interlocking programs following the methodology set out in \cite{AL14a}.
\textbf{\ul{3. Safety and Performance of the European Rail Traffic Management System: A Modelling and Verification Exercise in Real Time Maude} (extended abstract with Berger, Roggenbach and Seisenberger), WADT 2014 \cite{AL14c}} We present an approach to model ERTMS in such a way as to capture performance aspects of the system in an executable specification to which we can apply model checking to verify safety properties. Two case studies are presented: the first consists of two trains that travel round a closed track in the shape of a pentagon, the second case study takes the shape of the small junction from which trains can enter and leave. In the pentagon case study we verify the safety property that the movement authorities of the two trains do not overlap which implies that they do not crash. In the second case study we verify the safety property that the point does not move whilst it is in a movement authority i.e. the train does not derail.
\textbf{\ul{4. Modelling and Analysing the European Rail Traffic Management System in Real Time Maude} (extended abstract with Berger, James, Roggenbach, and Seisenberger), FTSCS 2014 \cite{AL14d}} An extended version of \cite{AL14c} has been submitted.
Material from the following publications formed part of my MRes thesis and influenced work in this thesis:
\textbf{\ul{5. Verification of Railway Interlockings in SCADE} (extended abstract with Seisenberger), AVOCS 2010 \cite{AL10}}
Two approaches are described to model and verify train control systems using the industrial modelling and verification tool SCADE~\cite{Scade}. The first involves the translation of ladder logic into the SCADE language and then applying SCADE's built in model checker to verify safety properties. The second approach involves segment of railway in a modular fashion allowing for the individual components to be verified before being combined together.
\textbf{\ul{6. Verification of Solid State Interlocking Programs} (with Chadwick, James, Kanso, Moller, Roggenbach, Seisenberger and Setzer), DTU Technical Report, \cite{AL13}}
This paper aims to provide a complete body of knowledge on the subject of verifying ladder logic programs for solid state interlockings. It contains the combined work of three MRes theses and associated research papers condensed to form a single methodology.
\textbf{\ul{7. Verification of Solid State Interlocking Programs} (with Chadwick, James, Kanso, Moller, Roggenbach, Seisenberger and Setzer), Lecture Notes in Computer Science, \cite{AL14a}}
This is an extended version of \cite{AL13}.
\section{Thesis Outline}
%%\textbf{Chapter 1}: This introduction.
%%\medskip \\
\textbf{\ul{Chapter 2}}: Overview of the formal foundations of the Minlog interactive theorem prover and program extraction. This is background information.
\medskip \\
\textbf{\ul{Chapter 3}}: Overview of SAT solving, including the DPLL algorithm and proof system, clause learning and resolution. This is background information.
\medskip \\
\textbf{\ul{Chapter 4}}: Proof of soundness and completeness for the DPLL and resolution proof systems. The completeness proofs are new.
\medskip \\
\textbf{\ul{Chapter 5}}: Formalisation of the DPLL and Resolution proof systems along with their soundness and completeness (as described in Chapter 4) in the Minlog System. The proof of completeness for the DPLL proof system forms the basis of our extracted SAT solver XSAT. The final part of this section describes the behaviour of the extracted program XSAT which is compared with another verified solver. The formalisation and extraction presented in this section are new results.
\medskip \\
\textbf{\ul{Chapter 6}}: Describes an approach to extract a prototype conflict driven clause learning SAT algorithm by modifying the DPLL proof system. This is a new formalisation.
\medskip \\
\textbf{\ul{Chapter 7}}: A general introduction to the traditional railway domain. This is background information.
\medskip \\
\textbf{\ul{Chapter 8}}: Overview of the model checking techniques used in this thesis for verification. This is background information. \medskip \\
\textbf{\ul{Chapter 9}}: A description of the European Rail Traffic Management System. This is background information.
\medskip \\
\textbf{\ul{Chapter 10}}: Formalisation of the European Rail Traffic Management System as 3 hybrid automata. This is a new formalisation.
\medskip \\
\textbf{\ul{Chapter 11}}: The European Rail Traffic Management System is modelled as a Real Time Maude specification (Based on the formalisation in Chapter 10). This is a new modelling approach.
\medskip \\
\textbf{\ul{Chapter 12}}: Validates the Real Time Maude specification of ERTMS (from Chapter 11) using simulation via execution of the specification and describes the verification of the specification using the Maude LTL model checker. This is a new simulation and verification approach.
\medskip
\begin{comment}
\begin{itemize}
\item Formalise the DPLL proof system and a proof of its completeness.
\item Extract a standard DPLL SAT algorithm from the formalisation into a functional programming language and test its performance
\item Modify the formalisation and completeness proof of the DPLL proof system so that it captures the behaviour conflict driven clause learning SAT algorithms.
\item Extract a clause learning SAT algorithm from the formalisation of the modified DPLL proof system and show that clause learning increases the efficiency of the solver.
\item Apply verified SAT algorithms to the verification of solid state railway interlocking programs.
\end{itemize}
Our second set of results is in regard to the formal specification and verification of the European Rail Traffic Management System (ERTMS) using Real Time Maude.
\begin{itemize}
\item Formalise ERTMS as a hybrid automata.
\item Formalise and Model ERTMS as a Real Time Maude specification.
\item Verify ERTMS using Real Time Maude's linear temporal logic model checker.
\end{itemize}
\end{comment}
\section{Hardware}
The following computer was used for all benchmarks and tests run as part of this thesis:
\begin{center}
\begin{tabular}{| l | c |} \hline
Operating system: & Ubuntu 14.04 LTS \\ \hline
Processor: & Intel(R) Core(TM) i7 870 64 bit quad core CPU at 2.93GHz \\ \hline
Memory: & 8 GBs 1333 MHz DDR2 RAM \\ \hline
Hard disk: & 750GB 7200 RPM SATA\\ \hline
\end{tabular}
\end{center}
\section{Implementations}
The Minlog implementations described in Chapters \ref{chapter:dpllminlog} and \ref{chapter:cdclproof} and Real Time Maude implementations described in \ref{chap:modelertms} and \ref{chap:verifyertms} are available at \url{http://cs.swan.ac.uk/~csal/phd/index.html}.
\section{Acknowledgements}
There are a great many who have supported me or contributed in some way throughout the writing of this thesis. I would first and foremost like to thank my supervisor Dr Monika Seisenberger for her eternal patience and guidance. She has mentored me since my undergraduate degree and moulded me into the research I am today.
Siemens Rail Automation/ Invensys Rail deserve many thanks for their support and valuable technical input throughout the whole of my research career. In particular I would like to thank Simon Chadwick for organising the collaboration from the Siemens' end and for dealing with my queries and questions via email.
My mother Sharon Lawrence provided me with many cooked meals and washed my clothes during my stay at her house in the summer of 2014; this enabled me to spend even more of my time on the writing of this thesis.
Dr Fredrik Nordvall Forsberg has made several contributions to this thesis. Firstly, he wrote the automatic translation which enabled Minlog terms to be translated into Haskell during a stay at LMU Munich with Prof. Helmut Schwichtenberg. I would have been unable to perform such an in-depth analysis of the extracted program without it. He was also a co-author on a paper and acted with a large amount professionalism throughout the writing period. Dr Ulrich Berger has provide his expert guidance numerous times both as an co-author and as a second supervisor during Monika's maternity leave. Dr Markus Roggenbach also acted as a second supervisor. Amongst other things Markus introduced me to Hybrid Automata as well as provided valuable knowledge on the Railway Domain. Finally, I would like to thank Alison Jones for sharing her in-depth understanding of the English language and for proof reading my thesis.