<![CDATA[In this paper will be shown a graph formulation as a formal approaches in research Model-Driven Development (MDD) with a case study : the development of Electronic Medical Record (RME) on the scope of the public health center. The model was designed using UML notation and be selected a State Machine diagram that represents prerequisite user needs (requirements). Before the model is derived (driven) into the skeleton code, the accuracy of the state machine must be verified. In order for the State Machine can be verified by formal approach, the State Machine should be first transformed into a propositional formula using the complete graph approach, and partial models. The initial phase of verification will check the suitability of the model with the requirements in Propositional Normal Form (PNF) using SAT Solver, respectively as and . SAT solver will provide a design decision, whether a requirement represented in the model or not. If these requirements are not hold in the model, the requirement is not certainty (uncertain) and model must be redesigned.]]>
Copyrights © 2014
