Even with most advanced quality assurance techniques, the correctness of complex railway software is hard to be guaranteed. To solve this problem, this thesis uses runtime verification to provide on-going protection during the operational phase. Runtime verification is performed by checking whether an execution of a running computational system satisfies a given monitoring property. A problem with most runtime verification systems is that the formalisms are often complicated. This thesis proposes extensions of live sequence charts (LSCs) which avoid this problem. It extends the standard LSCs as proposed by Damm and Harel by introducing the notion of "necessary pre-charts", and by adding concatenation and iteration of charts. With the language of extended LSCs (eLSCs), necessary and sucient conditions of certain statements can be intuitively specified. Moreover, similar as for message sequence charts, sequencing and iteration allow to express multiple scenarios. To express data-relevant properties, the language of parametrized eLSCs (PeLSCs) is defined by introducing condition and assignment structures. Monitors are generated through translating eLSCs and PeLSCs into linear temporal logic formulae and hybrid logic formulae, respectively. This thesis determines that the complexities of the word problem for the languages are both linear with respect to the lengths of input traces. In practice, an observed execution of a system may contain uncertainties. According to the impact on a monitoring result, this thesis divides various sources of uncertainties into incompleteness and inaccuracy. This thesis proves that a five-valued logic is sucient to express both of the two dimensions of uncertainties in a monitoring result. The semantics for eLSCs and PeLSCs are extended on basis of the five-valued logic. An ecient formula rewriting algorithm is developed, which allows to record only the last part of the observations necessary to perform the checking. The proposed monitoring approach is used to test a concrete example of the RBC/RBC handover process from the European Train Control System (ETCS) standard. With the language of eLSCs and PeLSCs, it expresses the properties of three functionalities of the process, including the management of communication, the safe functional module of the euroradio and the RBC/RBC handing over. The feasibility of the approach is shown by evaluating it on several benchmarks.

Hersteller:
Shaker Verlag GmbH
info@shaker.de
Am Langen Graben 15a
DE 52353 Düren