Đang chuẩn bị liên kết để tải về tài liệu:
Báo cáo khoa học: "A semantically-derived subset of English for hardware verification"

To verify hardware designs by model checking, circuit specifications are commonly expressed in the temporal logic CTL. Automatic conversion of English to CTL requires the definition of an appropriately restricted subset of English. We show how the limited semantic expressibility of CTL can be exploited to derive a hierarchy of subsets. Our strategy avoids potential difficulties with approaches that take existing computational semantic analyses of English as their starting point--such as the need to ensure that all sentences in the subset possess a CTL translation. . | A semantically-derived subset of English for hardware verification Alexander Holt and Ewan Klein HCRC Language Technology Group Division of Informatics University of Edinburgh alexander.holt@ed.ac.uk ewan.klein@ed.ac.uk Abstract To verify hardware designs by model checking circuit specifications are commonly expressed in the temporal logic CTL. Automatic conversion of English to CTL requires the definition of an appropriately restricted subset of English. We show how the limited semantic expressibility of CTL can be exploited to derive a hierarchy of subsets. Our strategy avoids potential difficulties with approaches that take existing computational semantic analyses of English as their starting point such as the need to ensure that all sentences in the subset possess a CTL translation. 1 Specifications in Natural Language Mechanised formal specification and verification tools can significantly aid system design in both software and hardware Clarke and Wing 1996 . One well-established approach to verification particularly of hardware and protocols is temporal model checking which allows the designer to check that certain desired properties hold of the system Clarke and Emerson 1981 . In this approach specifications are expressed in a temporal logic and systems are represented as finite state transition systems.1 An efficient search method determines whether the desired property is true in the model provided by the transition system if not it provides a counterexample. Despite the undoubted success of temporal model checking as a technique the requirement that specifications be expressed in temporal logic has proved an obstacle to its take-up by circuit designers and therefore alternative interfaces involving graphics and natural language have been explored. In this paper we address some of the challenges raised by converting 1 In practice it turns out to be preferable to use a symbolic representation of the state model thereby avoiding the state explosion problem .