CPN-B editor aims at designing, editing and transforming Colored Petri Nets (CPNs) to B abstract machines and Event-B language, which offers a number of powerful edition features and a new grammar for describing Colored Petri Nets. The goal of the CPN/B transformation is to enhance the use of integrated formal methods in safety critical software/systems development, verification and validation.
-
Coloured Petri nets (CPN) are a backward compatible extension of the concept of Petri nets. CPN preserve useful properties of Petri nets and at the same time extend initial formalism to allow the distinction between tokens. Coloured Petri Nets allow tokens to have a data value attached to them. This attached data value is called token color. Although the color can be of arbitrarily complex type, places in CPNs usually contain tokens of one type. This type is called color set of the place.
-
The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the Paris Métro Line 14). It has robust, commercially available tool support for specification, design, proof and code generation.
Compared to Z, B is slightly more low-level and more focused on refinement to code rather than just formal specification — hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this.
Recently, another formal method called Event-B has been developed. Event-B is considered an evolution of B (also known as classical B). It is a simpler notation, which is easier to learn and use. It comes with tool support in the form of the Rodin tool.