I started scratching on the surface of formally verified software. I whish to gain some experience on how this is done in reality. I have a project where I belive that formal methods could be applied. I year back I began work on uFSM (https://github.com/jonpe960/ufsm) which is a statechart library written in C. uFSM is From my current point of view I think the following needs to be done:
1) Translate the relevant parts of the UML Statechart spec in to something that can be analysed and proven
- What tools are available/appropriate for specifying and analysing requirements?
- What tools are available/appropriate for specifying and proving properties of the specification?
2) Derive an implementation from the specification
3) ... ?
I'm looking for advice on which methods could be appropriate, books and papers on this topic and if anyone shares this interest and wants to collaborate I would be thrilled.