Remnants of an attempt made in 2022 to get familiar with the concept of runtime verification.
- RV emanated from model checking.
- One could say that RV started out as a special case of MC.
From [2]:
Runtime verification avoids the complexity of traditional formal verification techniques (like model checking and theorem proving) by analyzing only one or a few execution traces and working directly with the actual system. Thus, runtime verification scales up relatively well and gives more confidence in the results of the analysis because it avoids the tedious and error-prone step of formally modeling the system (at the expense of reduced coverage).
—
From abstract of this:
Runtime verification is the topic of analyzing execution traces using formal techniques.
Safety property
- A property that will always true.
- Essentially the
◇in modal logic.- Or
Gin LTL.
- Or
- Once a violation is found, there is no hope the property will hold.
- Eg: Mutual exclusion, deadlock freedom ʳ¹
Liveness property
Every finite prefix can be extended to have a run that satisfies the property. ie, we can never be sure.
- A property that 'something good' will eventually happen.
- 'Stipulates that a "good thing" happens during execution' ʳ¹
- Essentially the
◇in modal logic.- Or
Fin LTL.
- Or
- There's always some hope that it will hold.
- Eg: Starvation freedom, termination ʳ¹
From abstract of [1]:
liveliness properties stipulate that "something good" events really happens during execution
Morbidity
Every finite prefix can be extended to have a run that violates the property. ie, we can never be sure.
Non-monitorable property
Not all properties are monitorable
- No matter how much of the stream is obtained, no definite verdict can be pronounced with respect to the property.
- Verdict cannot be given based on any finite prefix.
Eg: □(◇ p): ie, that a property holds infinitely often.
DBT: ie, all liveness and morbidity properties are non-monitorable??
Prefix
- Bad prefix: Every possible continuation would lead to a bad state
- Good prefix: Every possible continuation would lead to a good state
- Ugly prefix: There are continuations which can lead to good and bad states
- Eg: □(request → ◇ack)
Classification of properties
As per [2]:
| Class | Prefix | Verdict on | Pnueli |
|---|---|---|---|
| Safety | Bad | Failure | □ |
| Guarantee / co-safety | Good | Success | ◇ |
| Liveness | Ugly | Never | |
| Morbidity | Ugly | Never |
- AFS: Always Finitely Satisfiable
- AFR: Always Finitely Refutable
- NFS: Never Finitely Satisfiable
- NFR: Never Finitely Refutable
- SFS: Sometimes Finitely Satisfiable
- SFR: Sometimes Finitely Refutable
| Class | Description | Monitorable |
|---|---|---|
| AFR | If false, bad prefix exists | Yes |
| AFS | If true, good prefix exists | Yes |
| NFR | No | |
| NFS | No | |
| SFR | ||
| SFS |
Only property that's both a safety and guarantee property is true:
- safety: never fails, but we could've given ⊥ verdict if it did.
- guarantee: satisfied for empty prefix. Once satisfied, always satisfied (ie, ⊤).
Only property that's both a liveness and morbidity property is false:
- liveness:
- morbidity:
Model checking vs runtime verification
| Model checking | Runtime verification |
|---|---|
| Checks if all possible runs | Checks if a particular run |
| satisfies the property | satisfies the property |
| A language inclusion problem | A word inclusion problem |
Formal methods
Based on mathematical theories like
- Logic
- Set theory
- Automata
From a 2008 issue of AMS ³:
A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. All the intermediate logical steps are supplied, without exception. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors.
In the same AMS issue, from 'Formal Proof-Theory and Practice' by John Harrison:
A formal proof is a proof written in a precise artificial language that admits only a fixed repertoire of stylized steps. This formal language is usually designed so that there is a purely mechanical process by which the correctness of a proof in the language can be verified.
Spec
An abstract description of the system.
A system is correct if it meets its requirements.
'Program correctness' has meaning only with respect to a spec.
The spec usually says something to this effect:
something bad cannot happen and something good will happen
Testing vs verification
- Testing: Might be able to prove presence of bugs, but not their absence
- Formal verification: Can prove absence of bugs.
- Because the proof witnesses that it does what the spec say it does.
- Prove correctness of an abstract mode of the code.
Although formal verification doesn't mean 100% guarantee, it can come quite close. It definitely increases the trustworthiness of the system.
Errors in spec
Wrong spec means result of verification cannot be relied upon either.
Types of errors in the spec level include:
- Incomplete spec
- Incorrect spec
LTL
Linear Temporal Logic
Syntax:
φ := true
| p
| φ ∧ φ
| ¬ φ
| φ U φ
| X φ
Derived:
- F φ ≡ true U φ
- G φ ≡ φ U false
≡ φ U (¬ true)
≡ ¬ [◇ (¬ φ)]
- φ ∨ ψ ≡ ¬ [(¬ φ) ∧ (¬ ψ)]
- φ → ψ ≡ (¬ φ) ∨ ψ
Originally LTL specs were made for sequences of states, but for RV we usually indicate occurrence of events.
Monitor
A monitor checks whether an execution (ie, a finite prefix of a run) satisfies a property.
If ⟦φ⟧ is the set of executions that satisfies a spec φ, and the current execution is w, runtime verification boils down to checking if w ∈ ⟦φ⟧. [1]
So, runtime verification corresponds to a word problem. ie, checking whether a given word (w) is part of a given language (⟦φ⟧).
References
- Alpern, B. and Schneider, F.B., 1985. Defining liveness. Information processing letters, 21(4), pp.181-185.
- Peled, D. and Havelund, K., 2019. Refining the safety–liveness classification of temporal properties according to monitorability. In Models, Mindsets, Meta: The What, the How, and the Why Not? (pp. 218-234). Springer, Cham.
- Lamport, L., 1977. Proving the correctness of multiprocess programs. IEEE transactions on software engineering, (2), pp.125-143.
- Leucker, M. and Schallhart, C., 2009. A brief account of runtime verification. The journal of logic and algebraic programming, 78(5), pp.293-303.
- Daian, P., Guth, D., Hathhorn, C., Li, Y., Pek, E., Saxena, M., Şerbănuţă, T.F. and Roşu, G., 2016, September. Runtime verification at work: A tutorial. In International Conference on Runtime Verification (pp. 46-67). Springer, Cham.