MODEL-DRIVEN DEVELOPMENT : FASE AWAL VERIFIKASI MODEL DESIGN REKAM MEDIS ELEKTRONIS MENGGUNAKAN PERUMUSAN GRAF LENGKAP

Abstract

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.