文章基本信息

标题：Checking Unsatisfiability for OCL Constraints
本地全文：下载
作者：Clavel, Manuel ; Egea, Marina ; García de Dios, Miguel Angel 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2009
卷号：24
期号：0
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：In this paper we propose a mapping from a subset of OCL into first-order logic (FOL) and use this mapping for checking the unsatisfiability of sets of OCL constraints. Although still preliminary work, we argue in this paper that our mapping is both simple, since the resulting FOL sentences closely mirror the original OCL constraints, and practical, since we can use automated reasoning tools, such as automated theorem provers and SMT solvers to automatically check the unsatisfiability of non-trivial sets of OCL constraints.