Integration of Spin tool into integrated development environment Eclipse
| Title: | Integration of Spin tool into integrateddevelopment environment Eclipse |
| University program: | Telecommunications |
| Student: | Tim Kovše |
| Mentor: | assis. prof. dr. Boštjan Vlaovič |
| Co-mentor: | dr. Aleksander Vreže |
| Abstract: During the development of telecommunication systems attention is focusing on the software development. Checking the correctness of concurrent systems is not a trivial task. Use of formal verification can help. The intention of this diploma thesis is to improve theefficiency and user experience of the developer during the use of the formal verification tool Spin (Simple Promela Interpreter). The need for a better development environment appeared during the work on the large models that were based on the specifications from the industry. We integrated Spin tool as an Eclipse plug-in. Better editing of larger models was achieved with the use of the syntax highlighting and code folding. Additionally, we help the developer with the content assistant and syntax check of the model. It is possibleto export and import parameters for the simulation and formal verification. If model is notin accordance with the correctness requirements, Spin produces exact execution path that leads to an error. The analysis of the execution trail of concurrent systems is not a trivial task. We developed an algorithm for automated generation of an MSC (Message SequenceChart) diagram from the execution trail. This produces standards-based record that canbe edited in textual editors and development environments that are used for the software development in telecommunications. | |
