summary of benefits
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.
Our tools have been designed from the outset to overcome these constraints, using
automated reasoning and
an easy-to-learn language. The initial learning curve is not as steep as with tradional formal methods.
Rapid prototyping for simulation purposes is easy, and - should the initial requirements change -
adapting to many requirements changes is fast due to the high level of the specifications.
By comparison with earlier mathematically-based development methods, our tools
- easy to use
- take up minimal developer time
- enable both high productivity
- AND high reliability
All these factors combine to give you