Software Requirement Specification(SRS)
Selection 1 Natural Language
Function
Description
Inputs
Source
Outputs
Destination
Action
Requirements
Pre-condition
Post-condition
Side effects
If the requirements say about the solution of errors or exceptions, detailed solution shoule be provided.
Requirements don’t care about the options that ‘shall not do’.
If there are risks occurring in functions or options we require users to confirm.
Selection 2 Graphical models
Selection 3 Formal specification
Before: sth about Formal Method
60s Program Prove
80s Model Checking - Start of industrial use (reachability, dead lock)
Z, B, VDM, SOFL
Formal verification
- Theorem Proving
- Model Checking
Formal Specification
come from requirements
Language and construction method
Data Definition
Primitive Data Elements
No further decomposition is possible or necessary
Composition
Multiple data items
Iteration
Multiple instances of one item
Selection
Limited number of discrete values
From B, Z, VDM, to SOFL
if the pre-condition can not be satisfied, any outputs are acceptable.
Once pre-condition are satisfied, post-condition must be satisfied.
Problem: Difficult to understand and use.
Solution: Formal Engineering Method.
SOFL - Structured Object-oriented Formal Language
1 | module |