Table-based Software Designs : Bounded Model Checking and Counterexample Tracking

Model description languages used by most software model checkers are typically program-like languages such as the Promela language for the well-known model checker Spin. To promote practical use of model checking techniques in on-site software development, we realized, however, that graphicalized modeling languages (e.g., representatively, UML) are more easily acceptable compared to model-checker-specific program-like formal description languages. In this paper, we propose a model checking technique for software designs developed in a table-based description language – State Transition Matrix (STM), which is commonly considered to be effective for embedded software development. In addition, we also describe our proposed approach for graphically tracking counterexamples (i.e., design errors w.r.t. specified properties) reported by model checking. Supporting both graphicalized model description and graphically counterexample tracking is believed by us to be important for enhancing usability of model checking techniques and tools for on-site software engineers.