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.

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

Cavada, Roberto;Cimatti, Alessandro;Micheli, Andrea;Roveri, Marco;Susi, Angelo;Tonetta, Stefano
2011-01-01

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/104411
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact