The topic of the thesis is to check the implementation of a safety-critical protocol (the SCAN protocol) by model-based testing. The model used for testing is the model I have created during my previous studies. The goal of the tests generated on the basis of the model is to verify that the implementation conforms to the model's behavior.
The purpose of the SCAN protocol is to establish and manage connection between logical units of the object modules (belonging to railway objects like switches, signals etc.) and communication units of data transfer modules in control applications by message transfer. I modeled the protocol with the UPPAAL tool, which is a tool for modeling and verification using timed automata. With the help of the model checker, I also verified a few critical properties, proving this way the correctness of the protocol.
In the first part of the thesis, the implementation and description of the model, and then the analysis of the model-based testing options are included. These options are examined one by one to find out which ones can be used for model based testing and which are not, that is, which will not give new test cases with respect to the existing ones.
The following part describes the tools that can be used for test generation. In addition to determining the test goals, it is necessary to select the test generation tools and construct the auxiliary components (models) needed for the test generation.
Finally, the sequence of test steps generated by the selected test generation tool is included, and it is described how to process these sequence of steps in a concrete test environment.