-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathverification_intro.qmd
110 lines (80 loc) · 6.04 KB
/
verification_intro.qmd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
---
title: "What is verification?"
bibliography:
- ref_hybrid.bib
- ref_verification.bib
csl: ieee-control-systems.csl
format:
html:
html-math-method: katex
code-fold: true
code-summary: "Show the code"
crossref:
fig-prefix: Fig.
eq-prefix: Eq.
engine: julia
---
It has become nearly a tradition in our course that the terminology we use is often heavily overloaded. The term *verification* is no exception. Although we provide a definition below, to which which are going to adhere in this course, it is important to be aware that the term is also used in many different contexts and with different meanings.
## Verification vs validation
One particular opportunity for confusion is the related term *validation*. According to [PMBOK Guide](https://www.pmi.org/pmbok-guide-standards/foundational/pmbok):
Validation
: The assurance that a product, service, or system meets the needs of the customer and other identified stakeholders. It often involves acceptance and suitability with external customers.
Verification
: The evaluation of whether or not a product, service, or system complies with a regulation, requirement, specification, or imposed condition. It is often an internal process.
Undoubtedly, other definitions can be found, but we are going to stick to viewing verification as the process of checking if a system satisfies the given specifications or requirements. Whether these correctly capture the needs of the customer is a different question.
## Approches to verification
- Testing – just run the system and see if it behaves as expected. Disadvantages are obvious: cost, time, coverage.
- Simulation – reduces these disadvantages, but not completely – the coverage issue remains.
- Analytical techniques, also known as *formal verification* – the aim is to *prove* satisfaction of specifications *for all* possible conditions/evolutions of the system. The specifications (or requirements) are given in a formal (mathematical) language. Formal (mathematical) methods are then used.
## Model checking as one of formal verification approaches
There are several classes of formal verification techniques. One of them is *model checking*. It is based on a model of the system. For discrete-event and hybrid system the model is in the form of *Labelled Transition System (LTS)*. The outcome of the model checking is a *proof* or a *counterexample*.
## Labelled Transition system (LTS)
*Labelled transition system (LTS)* is essentially a variant of a (hybrid) automaton. Labels are attached to the states rather than the transitions. The labels come from the set $\mathcal{P}$ of atomic propositions $\mathcal{P} = \{p_1, p_2, \ldots, p_n\}$.
*Labelling function* $l: \mathcal X \to 2^\mathcal{P}$ assigns a set of atomic propositions to each state.
::: {#exm-lts-beverage}
## LTS for a beverage vending machine
We consider our good old friend – the beverage vending machine. We draw (again) its automaton, but also consider the set of atomic propositions $\mathcal{P} = \{\text{pending},\text{paid},\text{delivered}\}$ and we label the states with these.
``` {dot}
//| fig-cap: LTS for a beverage vending machine
//| label: fig-lts-beverage
digraph G {
bgcolor = "transparent";
rankdir = "LR";
node [shape = plaintext]; init
node [shape = circle width=1.4 margin=0 fixedsize=true];
waiting [label = "{}\n\n\n\nwaiting\n\n\n\n\n"];
swiped [label = "{pending}\n\n\n\nswiped\n\n\n\n\n"];
paid [label = "{paid}\n\n\n\npaid\n\n\n\n\n"];
coke_dispensed [label = "{paid, delivered}\n\n\ncoke\ndispensed\n\n\n\n"];
fanta_dispensed [label = "{paid, delivered}\n\n\nfanta\ndispensed\n\n\n\n"];
init -> waiting;
waiting -> swiped [label = "swipe card"];
swiped -> waiting [label = "reject payment"];
swiped -> paid [label = "accept payment"];
paid -> coke_dispensed [label = "choose coke"];
paid -> fanta_dispensed [label = "choose fanta"];
coke_dispensed -> waiting [label = "take coke"];
fanta_dispensed -> waiting [label = "take fanta"];
}
```
Having the states labelled with atomic propositions, we can now formulate specifications in terms of these propositions. For example, we can express the following two specifications:
- Specification #1: The machine never dispenses a beverage without being paid, that is,
$$
\text{delivered} \Rightarrow \text{paid}.
$$
- Specification #2: If the user pays, the machine will *eventually* dispenses a beverage.
The trouble with the latter specification is: how do we formally express the "eventually" part? It turns out that the classical propositional logic is not enough. We will need to introduce temporal logic(s). This we will do in one of the next sections.
:::
Before we move on, we can highlight two common types of specifications that can do without temporal logics.
## Two special types of specifications
- Safety (also invariance)
- Liveness (also progress)
### Safety (also invariance)
*Safety* (yikes, another rather overloaded term) means that "something bad never happens". Within state models (state automata and hybrid automata), this can be formulated as the system never entering the bad (unsafe) region of the state space.
Equivalently, it can be phrased as "something good always holds". With the state perspective, the system always stays in a good (safe) region of the state space.
How do we check safety? There are several techniques. In our course we are going to introduce two that are very popular in the control systems community:
- Reachability analysis,
- Barrier certificates.
### Liveness (also progress)
It can be phrased as "something good will eventually happen". Liveness (or progress) specifications be formulated in the state spacee too. The system is required to eventually reach a certain state or a subset in the state space. Depending on the flavour of the liveness specification, the initial set may be specified or not.
Control systems community must immediately recognize here one fundamental property that does clasify as a liveness property: stability. A stable system will eventually reach a certain state – the equlibrium.