Perfect Developer reduces the cost of developing critical software. By using Perfect Developer to prove the system correct before it is built, you avoid the need for debug/re-work/re-test cycles. When it is used within a mature software development process, Perfect Developer reduces the need for unit testing, by facilitating Correct by Construction software development.

Use Perfect Developer as a specification and modelling tool, to prove that the specification and design satisfy the stated functional requirements, and that the requirements have been correctly captured.

Optionally, you can go on to use Perfect Developer to generate code, either for rapid prototyping or for the finished system, 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, SPARK-annotated Ada code generation may be possible.

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 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, but also 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.

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, Perfect Developer 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.