Petri Nets to B-Language Transformation in Software Development
Acta Polytechnica Hungarica · 2014
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.