Formalization Flashcards
Statements on requirements serve
the professional communication between project participants
* the documentation
* for analysis by
− People
− Machines
examples
The system should respond as soon as possible.
* Operating errors are largely excluded.
* The system is self-explanatory.
* The system is highly reliable.
* All processes in the system are traceable.
* The system is inexpensive.
Formalization - What is that?
Formulation and Representation of content in a form independent of individual
(subjective) interpretation and based on a given system of definitions (theory)
Formulation of Statements
Formulation of Statements on Properties:
* Subjective: No explicit model/description system
* Objective: Explicit model/description system
* Empirical: No mathematical prediction/explanatory model
– Observations/Measurements
* Formalized: Mathematical prediction/explanatory model
* Partially Combinable
The Tradeoff: Precision vs. Comprehensibility
Precision (“objective”):
How precise are Requirements
formulated
→ Ultimately requires formalization
Comprehensibility (“subjective”):
How good and simple are
requirements to understand
→ Depending on target group
Empirically Formulated Statements on Properties
Empirically Formulated Statements on Properties
→ Capturing the statements by observations of systems and their environment.
→ Verification by experiments and measurements possible.
→ Metrics!
Examples:
* A system error occurs only once in 10 hours for a given operating situation.
* With 10 entries from a certain sample 9 usable answers are generated
Formulation of Statements
Informal: Syntax and Semantics not formally defined
* Example: Natural language, sketches, informal diagrams, etc.
Semi-formal: Syntax formally defined
* Example: UML, SysML, Matlab Simulink
Formal: Syntax and Semantics formally defined
* Example: Propositional and predicate logic, temporal logic, Petri nets, 𝜆-calculus, programming
languages
Formalization versus Modeling
Formalization Requires:
* A formal description language
– A set of description/modeling concepts
– Based on a specific system view
Models Require:
Implicit model building and is therefore
– An abstraction
– Only as correct as observations of reality
correspond to those on the model (validity
of a model)
Model versus Reality
A (formal) model is always an abstraction of reality
→ Formalization and modeling create an independent view of systems
→ Formalization only allows the formulation of certain properties that can be spoken about in the
model.
Linear Time Temporal Logic (LTL)
Streams of states are sequentially ordered. Properties of streams can be described with
predicates. Linear Time Temporal Logic (LTL) is a special method for formulating
predicates over infinite state streams.
Concept: Next-Operator
Goal: Description of at the next time step valid properties
Concept: Eventually-Operator
Goal: Description of in the future valid properties
Concept: Always-Operator
Goal: Description of always valid properties
Concept: Until-Operator
Goal: Binary Operator that describes relations between
two properties followed by each other
Most of the specifications (specification templetes)correspond to the following categories:
Existence: Certain event must occur at least once
* Absence: Certain event must not occur
* Precedence: Event Y comes after event X
* Response: Event Y is the response to event X
Advantages and Disadvantages of Formalization
Pro/Strengths:
* Precise, clear description
* Automation
– Model testing
– Test case generation
– Program generation
* Clear terms for
– Consistency
– Completeness
* Rules for derivation
* Traceability
* Verifiability with formal proof
Contra/Weaknesses:
* Limited expressiveness
– Abstraction bound to a purpose
* Poor intelligibility
– Fear of contact
* If unnecessary unintended precision
* High initial outlay
– Costs for training
– Experience
* Modification may be difficult
* Poor scalability
