Ming ChaiRuntime Verification of Railway Applications with Extended Live Sequence Charts | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
ISBN: | 978-3-8440-4333-4 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Reihe: | Informatik | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Schlagwörter: | runtime verification; monitoring; railway system; live sequence charts; linear temporal logic; hybrid logic; multi-valued logic; RBC/RBC Handover | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Publikationsart: | Dissertation | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Sprache: | Englisch | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Seiten: | 166 Seiten | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Abbildungen: | 60 Abbildungen | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Gewicht: | 434 g | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Format: | 24,0 x 17,0 cm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Bindung: | Gebundene Ausgabe | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Preis: | 48,80 € | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Erscheinungsdatum: | März 2016 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Kaufen: | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Download: | Verfügbare Online-Dokumente zu diesem Titel: Sie benötigen den Adobe Reader, um diese Dateien ansehen zu können. Hier erhalten Sie eine kleine Hilfe und Informationen, zum Download der PDF-Dateien. Bitte beachten Sie, dass die Online-Dokumente nicht ausdruckbar und nicht editierbar sind.
Benutzereinstellungen für registrierte Online-Kunden Sie können hier Ihre Adressdaten ändern sowie bereits georderte Dokumente erneut aufrufen.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Weiterempfehlung: | Sie möchten diesen Titel weiterempfehlen? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Rezensionsexemplar: | Hier können Sie ein Rezensionsexemplar bestellen. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Verlinken: | Sie möchten diese Seite verlinken? Hier klicken. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Export Zitat: |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Zusammenfassung: | 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 sufficient 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 sufficient 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 efficient 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. |