Abstraction Aided Model-Checking for Validation of Event-B Descriptions (preliminary)

Abstract. Event-B covers the system modeling at the early stages of the development, and thus puts emphasis on concurrent or non-deterministic behavior. Since the control aspects are complicated, automatic behav-ioral analysis techniques such as model-checking would be desirable to complement the proof-based verification method. The model-checking, however, is basically an exhaustive search technique, and the state space should be finite. For the case of Event-B, the state spaces are often in-finite since Event-B has a quite expressive Mathematical Language and evaluating formulas is undecidable in general. We are interested in apply-ing the abstraction aided model-checking techniques, found effective in checking C or Java programs, to Event-B, a modeling or design specifica-tion language. This paper presents an abstraction aided model-checking method and its application to Event-B. It further includes discussions on future research directions.