Safety-Critical Software Development

Perfect Developer reduces the cost of developing safety-critical software. The fast prototyping facilities allow for rapid system integration in a test environment, so that requirements errors are detected early. By supporting object-oriented design, Perfect Developer allows you to construct highly resuable application frameworks. Manual coding is eliminated, saving time and eliminating a source of errors. The C++ code generated by Perfect Developer uses a language subset carefully chosen to avoid unsafe constructs and conforms in most respects to the MISRA guidelines. Alternatively, Ada code generation may be possible if your application will not use object-oriented features.

Aerospace software development to DO-178B

The FAA and NASA created the Object Oriented Technology in Aviation (OOTiA) program to examine and document issues arising when DO-178B certification is required for software developed using object-oriented techniques. The program has produced a Handbook for Object Oriented Technology in Aviation, highlighting these issues and providing guidance.

Perfect Developer provides solutions to almost all issues documented in the Handbook. For example, by using the verified design-by-contract paradigm, it guarantees that formal subtyping is achieved (section 3.3.7 of the handbook). Type conversions (section 3.7.4) are formally proved safe and are never performed implicitly. Overloading (section 3.8) is rendered safe by the absence of implicit conversions and the formal verification of behaviour. Please contact us for further details.

Defence software development to UK DefStan 00-55, DefStan 00-56 or MIL-882

Defence Standard 00-55 mandates the use of formal proof for software that is highly critical to system safety, while the newly-issued version 3 of 00-56 cites formal proof as one of the highest forms of safety evidence and deprecates reliance on process-based evidence alone. Not only does Perfect Developer reduce the cost of developing critical software, by providing formal proofs it provides much of the safety evidence needed to achieve certification.

Development to IEC-61508

Perfect Developer is well-suited to the development of software to IEC 61508 safety standards. Formal methods are recommended for Safety Integrity Levels 2 and 3 (see Table A-1 of IEC 61508-3) and highly recommended for SIL 4. By generating proofs automatically, Perfect Developer makes the production of formally-verified software quick and economical, while at the same time allowing the use of agile development methods such as Extreme Specification if appropriate.