What is verification?

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 are providing a definition below, to which which are going to adhere in this course, it is important to be aware that the term is 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:

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 a process of checking if a system satisfies 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.

Example 1 (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.

G init init waiting {} waiting init->waiting swiped {pending} swiped waiting->swiped swipe card swiped->waiting reject payment paid {paid} paid swiped->paid accept payment coke_dispensed {paid, delivered} coke dispensed paid->coke_dispensed choose coke fanta_dispensed {paid, delivered} fanta dispensed paid->fanta_dispensed choose fanta coke_dispensed->waiting take coke fanta_dispensed->waiting take fanta
Figure 1: LTS for a beverage vending machine

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.

Back to top