A400M Airbus Flier crashed because of software issues

Re:A400M Airbus Flier crashed because of software issues by TeeWEE on Tuesday May 19, 2015 @09:36AM (#9569901)

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/

[ Parent | on HN ]

Re:A400M Airbus Flier crashed because of software issues by sfrank on Tuesday May 19, 2015 @11:21AM (#9570747)

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/

[ Parent | on HN ]

Re:A400M Airbus Flier crashed because of software issues by tedunangst on Tuesday May 19, 2015 @09:42AM (#9569937)

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

[ Parent | on HN ]

Re:A400M Airbus Flier crashed because of software issues by bglazer on Tuesday May 19, 2015 @10:18AM (#9570191)

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

https://sel4.systems/

[ Parent | on HN ]