- The central emphasis in software development - especially in requirements and specifications - is not on proof and logical deduction,
- but rather on separate concerns and the clarity that makes truth obvious.
- The software is not on mathematical abstraction, but rather on identifying and describing the Phenomena of the Problem Context in which the machine must function.
- Software describes a machine that must fit into the world of concrete reality, nor into a world of Platonic abstractions and ideas.
Formal Methods
- It means the mathematics and modeling applicable to the specification, design, and verification of software.
- The emphasis is on the creation of theories and tools to aid these activities.
- The methods are "Forma" in the sense that they are precise enough to be implemented on a computer.
- With these techniques, the developer can develop specifications and models which describe all or part of a system's behavior at various levels of abstraction,
- and use them as input to an automated theorem prover.
- For Requirements Engineering, the input may be a collection of partial specifications, and the output may be a report on where inconsistencies lie.
- For design, the input may be a specification and a design step, and the output is either "Yes, the design step is consistent with the specification.",
- or "No, and here's why not: ... ".
- For verification, the input may be a specification and a desired property of system behavior, and the output may be either "Yes, the property is a consequence of the specification.",
- or "No, and here's why not: ... ".
Software Mythbusters Explore Formal Methods
- Myths of Formal Methods:
- Myth 1: Formal methods can guarantee that software is perfect.
- Myth 2: Formal methods are all about program proving.
- Myth 3: Formal methods are only useful for safety-critical systems.
- Myth 4: Formal methods require highly trained mathematicians.
- Myth 5: Formal methods increase the cost of development.
- Myth 6: Formal methods are unacceptable to users.
- Myth 7: Formal methods are not used on real, large-scale software.
- Myths Discussion Themes:
- Formal Methods for both Understanding and Precision.
- Formal methods are used in situations where the primary benefit is for precisely understanding and specifying requirements.
- Software developer have benefited from this type of use even without proofs or model checking.
- Formal Methods Embedded in Tools and Languages.
- Industry is adopting formal methods that are embedded in tools or languages; developers who use these tools don’t always recognize the connection to formal methods.
- Formal Methods’ Demand for Mathematical Maturity.
- Embedding formalisms in tools or languages reduces the need for certain mathematical skills, but developers still need some mathematical maturity to effectively apply many formal methods.
- Formal Methods in Agile Practices.
- The desire for agility might appear to conflict with formal methods, but by using them to enable understanding, communication, and system evolvability shows otherwise.