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.
|