In model checking environments, system requirements are usually expressed by means of temporal logic formulas. We propose a user-friendly interface (UFI) with the aim of simplifying the writing of concurrent system properties. The tool is endowed with a graphical interface that supplies a set of patterns from the natural language; the defined patterns constitute a logic (UFL) that is adequate to express the classes of properties usually checked on actual systems. Moreover, UFI is integrated with the CWB-NC tool-kit which is a verification environment based on process algebras and the mu-calculus temporal logic; UFI supports the automatic translation of UFL formulas into mu-calculus formulas and save the translation in the format required by the CWB-NC. Nevertheless, UFI is a flexible tool that can be easily integrated with other environments. (c) 2006 Elsevier Inc. All rights reserved.

A user-friendly interface to specify temporal properties of concurrent systems

DE FRANCESCO, NICOLETTA;VAGLINI, GIGLIOLA
2007

Abstract

In model checking environments, system requirements are usually expressed by means of temporal logic formulas. We propose a user-friendly interface (UFI) with the aim of simplifying the writing of concurrent system properties. The tool is endowed with a graphical interface that supplies a set of patterns from the natural language; the defined patterns constitute a logic (UFL) that is adequate to express the classes of properties usually checked on actual systems. Moreover, UFI is integrated with the CWB-NC tool-kit which is a verification environment based on process algebras and the mu-calculus temporal logic; UFI supports the automatic translation of UFL formulas into mu-calculus formulas and save the translation in the format required by the CWB-NC. Nevertheless, UFI is a flexible tool that can be easily integrated with other environments. (c) 2006 Elsevier Inc. All rights reserved.
DE FRANCESCO, Nicoletta; Santone, A; Vaglini, Gigliola
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/11568/195589
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 4
social impact