Revising specifications with CTL properties using bounded model checking

Abstract

During the process of software development, it is very common that inconsistencies arise between the formal specification and some desired property. Belief Revision deals with the problem of accommodating new information that may be inconsistent with an existing knowledge base. In this paper, we propose the use of belief revision techniques in order to deal with inconsistencies in formal specifications. The main problem to be solved is that the most well known results for belief revision only hold for logics which are monotonic and compact, while most discrete-time temporal logics used to express system properties - and in particular, CTL - are not compact. We suggest the use of bounded model-checking, transforming the problem from CTL into classical propositional logic and then transforming back the results to suggest revisions to the user. © 2008 Springer Berlin Heidelberg.