OthelloPlay: a plug-in based tool for requirement formalization and validation

Requirement engineering is one of the most important phases in the development process of software and systems. In safety-critical applications, it is important to support the validation of the requirements with formal techniques to identify and remove flaws. However, requirements are often written in textual documents and their formalization and validation is not trivial for non-experts in formal methods. The goal of the OTHELLOPLAY tool is to support formalization of textual requirements and to simplify the use of formal techniques for requirements validation. The tool combines a formal verification engine and the Microsoft Word® editor in a single and consistent environment. A fundamental key in our design approach is a plug-in-based architecture, which uses the Python language in conjunction with a Microsoft Word® Add-In. The user can jump between textual requirements in the Microsoft Word® editor and the corresponding formal requirements model.