Title: Combining formal methods for the development of reactive systems

Authors: Olfa Mosbahi; Mohamed Khalgui

Addresses: LORIA, INRIA Lorraine, Nancy University, France; Martin Luther University, Germany. ' Martin-Luther-Universität Halle Wittenberg, Institut für Informatik, Raum 324, Von-Seckendorff-Platz 1, 06120 Halle (Saale), Germany

Abstract: This paper deals with the use of two verification approaches: theorem proving and model checking. We focus on the Event-B method by using its associated theorem proving tool (Click_n_Prove), and on the language TLA⁺ by using its model checker TLC. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA⁺ to verify liveness properties on a software behaviour. We extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, we give transformation rules from a temporal B model into a TLA⁺ module. We present in particular, our prototype system called B2TLA⁺, that we have developed to support this transformation; then we can verify these properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of the predicate diagrams. We illustrate our approach on a case study of a parcel sorting system.

Keywords: reactive systems; event-B method; refinement; language TLA+; liveness properties; verification; predicate diagrams; theorem proving; model checking; parcel sorting.

DOI: 10.1504/IJCAT.2011.045402

International Journal of Computer Applications in Technology, 2011 Vol.42 No.2/3, pp.127 - 149

Published online: 11 Feb 2012 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article