Escher Technologies Escher Technologies
Home Tools Services Support News Company Contact Publications Articles
Escher Technologies
arrowEscher Verification Studio
arrowEscher C Verifier
arrowPerfect Developer
arrowEvaluating the tools
arrowWhat others say
arrowCritical embedded software
arrowYour development process
arrowPD and SPARK Ada
arrowSummary of benefits
“We were especially impressed by the automation of verification proofs, which will substantially reduce our costs, and by the level of support provided by Escher Technologies.”

Guy Mason
General Dynamics UK Ltd.

Formal Software Specification Made Easier

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.

Perfect for easy learning!

Perfect Developer - Making software bugs extinct!

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.

Perfect Developer for automatic proof!

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.

From Perfect specification to code

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.


Copyright © 1997-2015 Escher Technologies Limited. All rights reserved. Information is subject to change without notice.      Link to  Privacy/Cookie Policy (new window)