Validating formal specifications with HOL
Guohui Feng · 1994
This research develops an approach to validating formal specifications. The method uses and extends the techniques of higher-order logic (HOL) and automated reasoning to detect potential inconsistencies. A potential inconsistency in a specification is not in itself an inconsistency, but only becomes one when facts are added, i.e., when we populate the database. From a software engineering perspective, the method helps ensure a consistent formal specification from which code is generated. This is important for domain modeling in software development. From a knowledge engineering perspective, the method provides automation of the complex process of conflict detection between sets of rules. This enables a knowledge-based system to give its users consistent solutions to their problems. From an automated reasoning perspective, the method provides an effective way to handle second-order problems as encountered in circumscription and second-order theorem proving. This dissertation describes this approach and shows how to automatically detect conflicts between sets of first-order clauses. This dissertation shows that detecting potential inconsistencies is a second-order problem. It presents a method that extends SCAN and transforms the second-order problem into an equivalent first-order problem if possible. This dissertation also presents a second-order method that enhances the Set-Var method. This dissertation presents an algorithm for detecting potential inconsistencies in a formal specification. This algorithm discovers potential inconsistencies by generating new clauses. A search strategy is developed for controlling the generation of useless clauses, and an indexing scheme is used to maintain the generated clauses. Finally, this dissertation describes the VAL system (VALidation system). VAL is applied to a real-world specification and successfully detects potential inconsistencies. The application of VAL supports the central tenet of this dissertation: Validating first-order specifications can be automated through HOL and automated reasoning techniques.