Building a Body of Knowledge on Model Checking for Software Development

Formal Methods has been recognized as a rigorous development methodology for hardware and software systems. In particular, model checking is well accepted as an effective verification method for hardware systems, safety/missioncritical systems and embedded systems. To foster this technology in industry, we recognize a need to develop educational materials to enhance learning the technology by students and practitioners. However, there are neither standard guidelines nor instructions how to teach this technology. In this paper, we will present the first draft of a body of knowledge on model checking called MCBOK to address this issue, and present lessons learned from its development experience.