Validation criteria is to discover and understand all requirements and domain properties.
Verification criteria is to verify that the program satisfies the specification, and the specification, given the domain properties, satisfies the requirements.
A broad view of formal methods includes all applications of discrete mathematics to software engineering problems. This application usually involves modelling and analysis where the models and analysis procedures are derived from or derived by an underlying mathematically-precise foundation.
A formal method in software development is a method that provides formal language for describing a software artifact (eg. specifications, designs, or source code) such that formal proofs are possible in principle, about properties of the artifact so expressed.
• Reasoning about a formal description
• The requirements problem – Verification does not eliminate the need for validation; However, the discipline of producing a formal specification can result in fewer specification errors.
-
When most of the requirements are functional requirements
-
For critical components of the system
• Formal requirements specifications are specifications that have formal semantics and syntax
• Allows a specification to be precise, unambiguous, and verifiable
• Can be verified automatically
• Useful in reasoning about the relationships between domain properties, requirements and specifications
• Prove properties of requirements and specs
• Good news: very useful when applied properly
• Paris metro line 14 entirely controlled by software formally developed by Matra Transport using the B abstract machine method
• A ≡ a person comes close to the door
• B ≡ the door opens
• C ≡ motion sensor is triggered
• D ≡ OPEN signal to motor
The specification, given the domain properties, satisfies the requirements
• Requirements: { A → B }
• Domain: { A → C, D → B }
• Specification: { C → D }
• Prove that Domain ∧ Specification → Requirements
• Property-oriented languages
– System is described by a set of axiomatic properties
• Model-oriented languages
– System is described by a state, and operations
– An operation is a function which maps the value of the state and the value of input parameters to a new state
• One major benefit for formal methods is automated verification
• Two methods: Theorem proving and Model checking
• System is described with a set of formulas Γ
• Specification is described with another set of formulas ϕ
• The verification method is to discover a proof that Γ ⊢ ϕ (i.e. ϕ is provable from Γ)
Theorem Proving Example:
• x is a book
• A(x): book x exists in the library
• B(x): book x is checked out
• Property of this system may be, “If a book x exists in the library, then book x can not be checked out”, i.e. A(x) → !B(x)
• The easiest way to consider a model-oriented language is as a state machine
• When the system is in a certain state, and is given a particular input, it will turn into another state
• Properties of the system are usually given using a temporal logic
• Want to verify that the model always holds the properties true
An example of a statement that can be expressed in temporal logic may be:
“if p is true, then it is always the case that q will eventually be true”
• You can verify this behaviour by stepping through a model M and checking that the statement above holds.
• Limited scope (to functional requirements)
• Isolation from other software products and processes in organizations
• Cost (require high expertise in formal systems and mathematical logic)
• Language Z
• Communicating sequential processes (CSP)
• Vienna Development Method (VDM)
• Larch
• Formal development methodology (FDM)
• Software Cost Reduction (SCR)