An approach to model real-time systems in B

Abstract

B-method is a formal method that covers the entire process from specification to implementation. The purpose of this paper is to develop a formal method for modeling real-time system in B. Our approach relies on timed automata; where the timed automa a is one of the successful approaches for modeling real time systems. In this paper we present methods to automate the derivation of B-model from network of timed automata system. In order to do so, the entire system needs to be represented using B language. We created an automatic mapper that converts the network of timed automata system into Bmodel.