Integrating model checking and UML based model-driven development for embedded systems

This paper discusses issues associated with integrating model checkers into a model-based development environment for embedded systems. The environment, DMOSES, is based on a formalization of UML Activity Diagrams and is used to generate correct and efficient code from such models; a key application area is the medical-device domain. A recent effort has focused on introducing formal reasoning into the development flow so that modelers can assess the correctness of their models before generating code from them. The verification of system requirements is shown using a case study of an infusion pump. This paper discusses issues involved in integrating model checkers into DMOSES and reports on a performance evaluation of two model checkers in particular: NuSMV and UPPAA