University of Twente Student Theses
Verification of a SysML railway specification with a translation to UPPAAL
Rekker, W. (2022) Verification of a SysML railway specification with a translation to UPPAAL.
|
PDF
3MB |
| Abstract: | In this research we successfully created a translation from EULYNX state machines modelling the behaviour of railway signalling equipment interfaces to the modelling language of UPPAAL. It provides additional aid in model checking these systems because UPPAAL uses different model checking techniques and is more accessible than mCRL2. The main research question that guided this research is: How can we create a jEULYNX to UPPAAL translation which can be used on models of railway signalling equipment interfaces? Our success in answering this question is supported by the following conclusions that are drawn from this research. In order to create a translation from EULYNX to UPPAAL the following things are required. Because the target model of the translation is in a formally defined domain, a clear interpretation of the source model needs to be chosen in order to translate from an informal domain. For this research the best choice was to synchronise the state machines with an execution loop and have them communicate with direct memory sharing. Changes in the memory are handled via an event queue per state machine. This interpretation worked well with model synchronisation and memory sharing features of UPPAAL. Next, the translation needs translation patterns that create a framework in the target model in order to facilitate certain features that are not directly available in the target modelling language. In our translation to UPPAAL this included for example the orchestrator process and the event manager processes. This provided the right features and it kept the state machine processes simple and close to the original structure of the EULYNX state machines, which satisfies our goal that the target model should be easy to read. To ensure the quality of the translation, it is necessary to validate it both in terms of correctness and usability. In this research the translation was tested by translating example 94 models and verifying their behaviour with properties in UPPAAL. This systematic approach gave us strong confidence in saying that the translation is correct, even though it is not able to completely proof the absence of errors. The technique that fit our research the best to validate the usability of the translation was evaluating the checkability of a set of requirements on models part of the EULYNX standard. The set of requirements was created with the needs of railway engineers in mind. This provided enough evidence that the translation can be used successfully by railway engineers. However, there are some intricate but realistic requirements that could not be translated. As part of the usability of the translation, performance is also an important factor as it determines the scale of the models that can be verified using the translation. We found that the performance of the translation can be improved by decreasing the number of intermediate locations and synchronising the processes more strictly. This is discussed in further detail in Chapter 10. While the translation is not yet suitable for large scale models, we are confident that it can be improved for larger input models by implementing the proposed alterations. To conclude we can say we succeeded in creating a useful translation that helps with the verification of railway signalling equipment interfaces in the EULYNX standard. As part of the research we tested it for correctness and usability, which gave a positive result. We did find some problems in the usability as a result of state space explosion. To help increase the usability we proposed some improvements on the translation in its current state. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/89467 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page