Verification of a microcomputer program specification embedded in a reactive system
This paper proposes a model checking method for microcomputer programs. To deal with the state explosion problem. we adopt a compositional verification approach. Based on the proposed method, a microcomputer program for a real-life air-conditioner is verified. The program is large enough tu cause state explosion. Among fourteen typical properties of the program, five properties are successfully verified by our method.
reactive system model checking compositional verification reachability graph