摘要 : 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... 展开 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. 收起