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.
◇ in modal logic.
G in LTL.Every finite prefix can be extended to have a run that satisfies the property. ie, we can never be sure.
◇ in modal logic.
F in LTL.From abstract of [1]:
liveliness properties stipulate that "something good" events really happens during execution
Every finite prefix can be extended to have a run that violates the property. ie, we can never be sure.
Not all properties are monitorable
Eg: □(◇ p): ie, that a property holds infinitely often.
DBT: ie, all liveness and morbidity properties are non-monitorable??
As per [2]:
| Class | Prefix | Verdict on | Pnueli |
|---|---|---|---|
| Safety | Bad | Failure | □ |
| Guarantee / co-safety | Good | Success | ◇ |
| Liveness | Ugly | Never | |
| Morbidity | Ugly | Never |
| 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:
Only property that's both a liveness and morbidity property is false:
| 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 |
Based on mathematical theories like
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.
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
Although formal verification doesn't mean 100% guarantee, it can come quite close. It definitely increases the trustworthiness of the system.
Wrong spec means result of verification cannot be relied upon either.
Types of errors in th spec level include:
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.
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 (⟦φ⟧).