Formal Systems Development

Tags

soft-eng

Is a software design model that uses a formal [see page 15, specification] of the original requirements (in a mathematical specification language such as OCL) to prove the safety and correctness of the software implementation.

This approach is generally used for safety critical systems such as microprocessor design, routers, switches, hypervisors, security applications etc. However it requires mathematical expertise, and is rarely applicable for most software projects that value time to market over correctness.

The formal development process is known as refinement. It involves creating a formal specification to clarify ideas and then deriving the program in steps from the specification.