Introduction Flashcards
What is a Formal Method?
Formal Methods refer to mathematically rigorous techniques and tools for the specification, design and verification of software and hardware systems…
Formal (def)
with a well-defined syntax and semantics
How do the Formal Methods help in SE?
Analysis is based on well-defined steps that follow logical reasoning and thus allow us, for example to prove that a system (a model thereof) satisfies the specification.
How is a typical SW Systems Development Process?
- Informal requierements
- informal or semi-formal specification (unambiguous? consistent?)
- design (all req. considered? design correct?)
- implementation
- unit tests (testing based on informal specification)
- integration / system tests (not what stakeholder wanted. Violates critical req. -> dire consequences)
- use and maintenance
How operates the Model Checking?
From the specification and the Model, a model checker can be used (implemented) to find out, whether the specifications are satisfied or not. In the case of a non-satisfier, the specification will be modified with the help of a counter example, that says how the specification can be violated. Also the model could be modified as mostly the error is here.
Model checking in the development process
informal specification -> will be formalized, and from here a design will be created.
* formalized spec. will be transformed to specification for MC tool
* The created design will be transformed to a Model for the MC tool
The Model and the specifications for the MC tool will be checked with the Model Checker (MC).
If specific. not satisfied -> the design / Model or the specification will be modified.
If satisfied -> write/generate code
Obstacles with applying formal methods
- high system complexity: > problem decomposed and abstracted
- writing formal specifications and designs is difficult
- existing tools are difficult to integrate: > formal analysis tools are not compatible with complex problems, not intuitive
