One of the initial steps of software development is the specification of requirements. In the case of critical systems this important work phase becomes even more significant. However, the usage of natural language for the specification of requirements becomes easily misunderstandable and tiresome to use, because the correctness of these expressions are difficult to verify. This is why we use formal methods to create the requirements instead. Applying these formal methods, we can use finite-state verification tools if we have formal models and formal requirements for our system.
The creation of formal requirements for the model-checker tools could become quickly tiresome by many obstacles during the process, because in this case we should use some kind of formal language to define the requirements, for example temporal logic. The developers who want to understand, concatenate, nest, edit or maintain these expressions need not negligible amount of expertise in this topic.
The topic of my thesis is designing and implementing a tool which could facilitate the work of developers during the creation of formal specification of requirements. To achieve this goal I am going to use property specification patterns.
With features of property specification patterns, the user of the tool that I developed is able to avoid the direct editing of property specifications. This way he meets only the natural language representation of the requirements, and the temporal logic is automatically generated in the background. The software contains the most useful set of patterns but it also gives the user the opportunity to freely extend this set.
For the creation of the tool I got to know the property specification patterns, the temporal logics and through these things the formalization of functional requirements. I had to do some research to be able to choose the proper technology which can be applied for the implementation. This is how I’ve chosen JavaFX. Last but not least, during the development a dozen of programming problems and questions popped up for which I have found the answers and solutions in the existing software design patterns. Because of this, my knowledge of software technologies has also broadened during the project.