I'm trying to use the B-Method as an mechanism to formally specify structured data.
As in a function that parses a block of bytes representing some data. All the examples I can find are of some form of sequential state machine (train system, control system, etc), as specified as machines (which I get the B-Method is used for in the main).
As example, I trying to formally specify the parsing of a DNS packet. Such that one could prove or partially that parsing function met certain conditions, so the packet could be said to be malformed or not.
I tried the Atelier tool based on QT, as an approach to implement something of this nature, but it all seems geared for ordered event machines.
The B method has been used industrially for such applications. There is not much publicly available material. For inspiration, you may want to have a look at Systerel's S2OPC OPC UA Toolkit (https://gitlab.com/systerel/S2OPC).
There are some B developments are in the
bsrcfolder.