Open AccessMODEL-DRIVEN DEVELOPMENT : FASE AWAL VERIFIKASI MODEL DESIGN REKAM MEDIS ELEKTRONIS MENGGUNAKAN PERUMUSAN GRAF LENGKAP
Author(s) -
Acep Taryana,
Bangun Wijayanto,
Naoyasu Ubayashi,
Joko Setyono
Publication year - 2014
Publication title -
jurnal ilmiah matematika dan pendidikan matematika (jmp)/jurnal ilmiah matematika dan pendidikan matematika
Language(s) - English
Resource type - Journals
eISSN - 2550-0422
pISSN - 2085-1456
DOI - 10.20884/1.jmp.2014.6.2.2904
Subject(s) - computer science , model checking , solver , graph , notation , abstract state machines , boolean satisfiability problem , unified modeling language , theoretical computer science , state (computer science) , finite state machine , programming language , algorithm , mathematics , software , arithmetic
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.