Petri nets to B-language transformation in software development

Abstract

Petri nets and B-Method represent a pair of formal methods, for computer systems engineering, with interesting complementary features. Petri nets have nice graphical representation, valuable analytical properties and can express concurrency. B-Method supports verified software development. To gain from these complements, a mapping from Petri nets to the language of B-Method has been defined and its correctness proved. This paper presents, by means of a case study, the usefulness of incorporation of Petri net designs in a software application developed by B-Method. Modifications of this mapping intended for the Event-B method and treatment of concurrency are also discussed.