| TR#: | LCL9602 |
| Class: | LCL |
| Title: | Translating Natural Language System Specifications into Temporal Logic via DRT |
| Authors: | R. Nelken and N. Francez |
| PostScript | LCL9602.ps.gz - LCL9602.ps |
| LCL9602.pdf | |
| Abstract: | In the past several years an automatic verification technique for finite-state concurrent (software and hardware)systems has been developed. By this technique, behavioral specifications of a system, expressed in a propositional temporal logic, are algorithmically checked against a model of the system. A recognized problem of this approach is making the formalism, in which specificatoins are expressed, more convenient. This paper describes a method for automatically translating natural language specifications into temporal logic, via an intermediate representation in DRT. Using this method, users may express complex specifications in relatively free natural language, while ensuring that they are correctly translated into temporal logic and subsequently verified. We describe an implementation of this method ina unification-based grammar formalism, CUF. This paper describes an application of computational linguistic methods to the domain of verification of computer systems (both software and hardware). We present a method for automatically translating natural language (NL) behavioral specifications of computer systems into temporal logic (TL), for which tools for automatic formal verification are well-developed. The method presented here has been implemented. |
| Copyright | The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information |
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/1996/LCL/LCL9602), rather than to the URL of the PDF or PS files directly. The latter URLs may change without notice.
To the list of the LCL technical reports of 1996
To the main CS technical reports page