Functional verification for UML-based model driven design of embedded systems

Abstract

Modeling and formal specification in combination with formal verification can substantially contribute to the correctness and quality of design of embedded systems and consequently help reduce the development costs. This paper tackles the problem of providing a fully automated formal verification for UML-based design of embedded systems. For verification it employs the model checking technique. Unlike other approaches, the paper focuses on supporting a consistent subset of UML diagrams that cover all main aspects of an embedded system, i.e. the structure, communication and behavior. The whole approach is evaluated on a case study of a Manufacturing Flow System with distributed control.