- Formal methods can guarantee that software is perfect.
- They work by proving that programs are correct.
- Only highly critical systems benefit from their use.
- They involve complex mathematics.
- They increase the cost of development.
- They are incomprehensible to clients.
- Nobody uses them for real projects.
Activities of Formal Methods
- Writing a formal specification
- Proving properties about the specification
- Constructing a program by mathematically manipulating the specification
- Verifying a program by mathematical argument
Key points
- Formal system specification complements informal specification techniques.
- Formal specifications are precise and unambiguous. They remove areas of doubt in a specification.
- Formal specifications force an analysis of the system requirements at an early stage. That helps us in correcting errors at this stage is cheaper than modifying a delivered system.
- Formal specification techniques are most applicable in the development of critical systems and standards.
- Algebraic techniques are suited to interface specification where the interface is defined as a set of object classes.
- Model-based techniques model the system using sets and functions. This simplifies some types of behavioural specification.
Limitations to Formal Methods
- Use formal methods as supplements to quality assurance methods not a replacement for them
- Useful for consistency checks, but formal methods cannot guarantee the completeness of a specifications
- Formal methods must be fully integrated with domain knowledge to achieve positive results
Acceptance of formal methods
- Formal methods have not become mainstream software development techniques as was once predicted
- Other software engineering techniques with better quality results.
- Time-to-market versus high quality
- Hard to scale up to large systems
- Not well-suited for specifying and analysing user interfaces and user interaction
No comments:
Post a Comment