Know-how refers to the knowledge of how to achieve objectives effectively and efficiently. Mapping this knowledge helps in understanding domains, learning about problems and solutions, identifying potential gaps and places for improvements, and reasoning about the existing knowledge. Recently, we developed and formalized an approach called ME-MAP for mapping out know-how. Checking the correctness properties of such maps is essential to ensure their qualities and grantee their practical usage. Therefore, it is critical to enable automation of reasoning methods. This paper presents three reasoning methods for ME-maps: (1) checking consistency; (2) creating legal instances; and (3) extracting a “core map” for a given ME-map. The methods are based on translating ME-maps into a Constraint Satisfaction Problem (CSP) and then using an off-the-shelf CSP solver for verifying the desired properties.

Know-how deals with the knowledge of how to achieve objectives effectively and efficiently. Mapping this knowledge facilitates and encourages understanding domains, learning about problems and solutions, analyzing the trade-offs among these, identifying potential gaps and places for improvements, and reasoning about the existing knowledge. To address these goals we developed a know-how mapping approach - ME-MAP and introduced its abstract and concrete syntax. This paper further equips the modeling/mapping language of the ME-MAP approach with formal semantics and presents related analysis and reasoning tasks, elaborate on these tasks and explain their rationale. These tasks ensure keeping precise, consistent and correct models, enable the extraction of useful knowledge from the model and by this provide an inclusive support to the knowledge stakeholders.

Models lie at the heart of the emerging model-driven engineering approach. In order to guarantee precise, consistent, and correct models, there is a need for efficient powerful methods for verifying model correctness. Class diagram is the central language within UML. Its correctness problems involve issues of contradiction, namely the consistency problem, and issues of finite instantiation, namely the finite satisfiability problem. This article analyzes the problem of finite satisfiability of class diagrams with class hierarchy constraints and generalization-set constraints. The article introduces the FiniteSat algorithm for efficient detection of finite satisfiability in such class diagrams, and analyzes its limitations in terms of complex hierarchy structures. FiniteSat is strengthened in two directions. First, an algorithm for identification of the cause for a finite satisfiability problem is introduced. Second, a method for propagation of generalization-set constraints in a class diagram is introduced. The propagation method serves as a preprocessing step that improves FiniteSat performance, and helps developers in clarifying intended constraints. These algorithms are implemented in the FiniteSatUSE tool [BGU Modeling Group 2011b], as part of our ongoing effort for constructing a model-level integrated development environment [BGU Modeling Group 2010a].