Systerel used the B formal method and Atelier B for the development of their Safe and Secure Open Platform Communications (S2OPC), an open-source solution for OPC UA communications.
The OPC UA is a standard overseeing interoperability and data exchange for industrial communications. It provides safe and secure means to connect supervision systems (SCADA), programmable logic controller (PLC), with actuators and field systems. It is particularly dedicated to the Industrial Internet of Things (IOT).
This development integrates the B modelling of dynamic memory management, including memory allocation, deallocation and pointers validity.
This OPC UA implementation confirms that developing software with the B method with EAL4 and SIL2 certification capabilities is feasible and well founded.