The benefits of formal specification have long been recognized by the writers of ultra-reliable software. In the past, software specifications have often been written in Z, a language with a steep learning curve and limited tool support.
Now there is an alternative: the Perfect specification language, supported by the Perfect Developer tool.
The Perfect specification language builds on standard concepts from procedural, object-oriented, and functional programming languages, with mathematical notation kept to a minimum, using the principles of Verified Design by Contract.
This specification language is much easier than Z for most software developers to learn. Like Z, Perfect supports refinement of high-level to low-level specifications.
The Perfect specification language is supported by the Perfect Developer tool, which includes a powerful automatic theorem prover for producing verification proofs without user intervention. This means you can easily and economically verify your specifications as you develop and refine them.
If you code in MISRA-C, then by transferring your design and low-level requirements to Escher C Verifier, you can develop code that is formally verified to meet the low-level requirements.
Alternatively, Perfect Developer can be paired with SPARK Ada, allowing the design and low-level specifications to be carried through to SPARK-annotated Ada code. Perfect Developer provides partial SPARK Ada code generation, as well as full prototype code generation in a choice of other languages.
If you would like some more information, please contact us.
