1st Delivery [PJ1]: Specification
The delivery consists of a formal definition (Machine) in B of the system. Proof obligations not automatically proven by AtelierB must be proven informally (textually).
2nd Delivery [PJ2]: Formal Model Visualisation
The delivery consists of a functional prototype created in BMotionWeb.
3rd Delivery [PJ3]: Implementation
The delivery consists of a formal definition (Implementation) in B of the system. It should be possible to generate C code from the implementation. Proof obligations not automatically proven by AtelierB must be proven informally (textually).