Escher Technologies Escher Technologies
Home Tools Services Support News Company Contact Publications Articles
Escher Technologies
More:
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.
 

The technology: Formal Methods and Automated Reasoning

It has long been realized that the behaviour of software components and even complete software and hardware systems can be described using mathematics. Similarly, the meaning of program language statements can be defined mathematically. In principle, the meanings of individual statements can be combined to calculate the meaning of a complete program, which can then be compared with a mathematical description of the required behaviour.

The use of mathematics to define and verify the behaviour of software is called formal methods. Aerospace companies and other writers of critical software traditionally use formal methods to help ensure that the most vital parts of their software are dependable.

In past years, it has not been economic to apply formal methods to the development of non-critical software. The tools available required the developer to express specifications using mathematical notations and to assist in the theorem-proving process. Further, the semantics of the specification language were often far removed from the semantics of the programming languages used to write code, making it hard to relate the two languages.

Making use of recent advances in automated reasoning technology, both Perfect Developer and Escher C Verifier include a fully-automatic theorem prover, so that it is not essential for users to possess extensive mathematical knowledge.

Taken with Perfect Developer's ability to generate code automatically from simple specifications and its high-level data types, these features make the development of dependable software possible, without sacrificing developer productivity.

 


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