[TeeWEE]

I'm quite baffled at the fact that this standard does not include formal verification of the software models used.

Formal verification and state space analysis can prove that the software "model" will not fail. State space exploration of the actual implementation is actually often not feasible due to the enourmous amount of states.

So my question: Are you doing formal analysis of the software models/designs? I know they are using it in software used in space crafts / nuclear power plants.

Reference: - http://ti.arc.nasa.gov/m/profile/dimitra/euromicro-share.pdf - http://javapathfinder.sourceforge.net/

[sfrank]

The DO-178B/C explicitly does not specify how verification is done but describes the properties that are expected of the verification evidences that you submit to the certification authorities; so formal verification is perfectly fine as one item on your verification check list. In particular DO-333 amends DO-178C with specific topics concerning formal methods.

For example Astree [1] has been developed for decades now, with Airbus as one of the major sponsors.

[1] http://www.astree.ens.fr/

[tedunangst]

What is the largest piece of code you have formally verified?

[bglazer]

The seL4 mircrokernel is comprehensively formally verified and is marketed towards aerospace applications.

https://sel4.systems/