Integration of Automatic Theorem Provers in Event-B Patterns

Free registration required

Executive Summary

Event-B is a formal method for the system level modeling and analysis of dependable applications. It is supported by an open and extendable Eclipse-based tool set called Rodin. In this paper, the authors proposed using automatic theorem provers known as SMT-solvers with event-B pattern. The benefits of that are to reduce the proving effort, to reuse a model and to increase the degree of automation. The proposed approach has been applied successfully on two different case studies.

  • Format: PDF
  • Size: 1261.3 KB