Correct-by-Construction

Tools for RHO-Lang smart contracts formal verification (with Namespace/Spatial/Hennessy-Milner Logics)

Labeled Transition System (LTS)
Calculus of Communication Systems (CCS)
Strong / Weak Bisimulation
Hennessy-Milner Logic (HML)

Labeled Transition System (LTS)

LST syntax

Core classes:

net.golovach.verification.LTSLib.{LTS, LTSState, LTSAction, LTSEdge}

Base imports:

import net.golovach.verification.LTSLib._

Nota bene:

scala.Symbol - for LTSState (implicit conversion for syntax sugar)
scala.String - for Action (implicit conversion for syntax sugar)

Type aliases

type ⌾ = LTSState
type ⒜ = LTSAction
type ➝ = Edge

State syntax

val s0 = LTSState("s", 0) // or
val s1: LTSState = 's1    // or
val s2: ⌾ = 's2          // or

Action syntax

// Input actions
val a_in = ↑("a") // or
val b_in = "b".↑  // or

// Output actions
val a_out  = ↓("a") // or
val b_out = "b".↓   // or

// Silent action
val tau = τ

// Checking are there annihilated actions
val x: Boolean = a_in ⇅ a_out // true

Edge syntax

val e0 = Edge('s0, τ, 's1) // standard syntax
val e1 = 's0 × τ ➝ 's1    // syntax sugar

LTS operations

Simple cyclic Coffee Machine definition

val lts = LTS(
  ports = ("$", "☕"),
  actions = ("$".↑, "☕".↓),
  states = ('s0, 's1),
  init = 's0,
  edges = Set(
    's0 × "$".↑ ➝ 's1,
    's1 × "☕".↓ ➝ 's0
  ))

Print to console

println(dump(lts))

CONSOLE

>> ports:   {$, ☕}
>> actions: {↑$, ↓☕}
>> states:  {'s0, 's1}
>> init:    's0
>> edges:   
>>     's0 × ↑$ → 's1
>>     's1 × ↓☕ → 's0

Calculus of Communication Systems (CCS)

Base classes

net.golovach.verification.ccs.CCSLib.Process
net.golovach.verification.ccs.CCSLib.{∅, ⟲, Prefix, Sum, Par, Restriction, Renaming}

Process = ∅ | ⟲ | Prefix | Sum | Par | Restriction | Renaming

Base imports:

import net.golovach.verification.LTSLib._
import net.golovach.verification.ccs.CCSLib._

CM ≡ Coffee Machine

1) Prefix and ∅ syntaxes with transformation to LTS

Simple disposable (acyclic) Coffee Machine

val CM = ↑("$") :: ↓("☕") :: ∅
println(dump(toLTS(CM)))

CONSOLE

>> ports:   {☕, $}
>> actions: {↓☕, ↑$}
>> states:  {'s0, 's1, 's2}
>> init:    's2
>> edges:   
>>     's1 × ↓☕ → 's0
>>     's2 × ↑$ → 's1

Or states can be named explicitly

val CM = ↑("$") :: ↓("☕") :: ∅("CM")

CONSOLE

>> ports:   {☕, $}
>> actions: {↓☕, ↑$}
>> states:  {'CM0, 'CM1, 'CM2}
>> init:    'CM2
>> edges:   
>>     'CM1 × ↓☕ → 'CM0
>>     'CM2 × ↑$ → 'CM1

2) Loop/Recursion (⟲) syntax

Simple cyclic Coffee Machine

val CM = ↑("$") :: ↓("☕") :: ⟲
println(dump(toLTS(CM)))

CONSOLE

>> ports:   {☕, $}
>> actions: {↓☕, ↑$}
>> states:  {'s0, 's1}
>> init:    's1
>> edges:   
>>     's0 × ↓☕ → 's1
>>     's1 × ↑$ → 's0

Or states can be named explicitly

val CM = "$".↑ :: "☕".↓ :: ⟲("CM")

Or sequence with loop at the end

val LOOP = "$".↑ :: "☕".↓ :: ⟲
val CM = "init".↑ |: LOOP

println(dump(toLTS(CM)))

CONSOLE

>> ports:   {☕, $, init}
>> actions: {↓☕, ↑$, ↑init}
>> states:  {'s0, 's1, 's2}
>> init:    's2
>> edges:   
>>     's2 × ↑init → 's1
>>     's1 × ↑$ → 's0
>>     's0 × ↓☕ → 's1

Or one-liner

val CM = "init".↑ |: ("$".↑ :: "☕".↓ :: ⟲)

Another sequence with loop at the end

val LOOP = "$".↑ :: "☕".↓ :: ⟲
val CM = "initA".↑ :: ("initB".↑ |: LOOP)

println(dump(toLTS(CM)))

CONSOLE

>> ports:   {☕, $, initB, initA}
>> actions: {↓☕, ↑$, ↑initB, ↑initA}
>> states:  {'s0, 's1, 's2, 's3}
>> init:    's3
>> edges:   
>>     's3 × ↑initA → 's2
>>     's2 × ↑initB → 's1
>>     's1 × ↑$ → 's0
>>     's0 × ↓☕ → 's1

Or one-liner

val CM = "initA".↑ :: ("initB".↑ |: ("$".↑ :: "☕".↓ :: ⟲))

3) Alternative/Choise/Sum (+) syntax

val CS = ("$".↓ :: "☕".↑ :: "✉".↓ :: ⟲) + ("☕".↑ :: "✉".↓ :: ⟲)
println(dump(toLTS(CS)))

CONSOLE

>> ports:   {✉, ☕, $}
>> actions: {↓✉, ↑☕, ↓$}
>> states:  {'s0, 's1, 's2, 's3}
>> init:    's2
>> edges:   
>>     's1 × ↑☕ → 's0
>>     's2 × ↓$ → 's1
>>     's0 × ↓✉ → 's2
>>     's3 × ↓✉ → 's2
>>     's2 × ↑☕ → 's3

4) Parallel Composition (|) syntax

With silent τ-action generation

val A_IN  = "A".↑ :: ⟲
val A_OUT = "A".↓ :: ⟲

println(dump(toLTS(A_IN | A_OUT)))

CONSOLE

>> ports:   {A}
>> actions: {↑A, ↓A, τ}
>> states:  {'s0}
>> init:    's0
>> edges:   
>>     's0 × ↑A → 's0
>>     's0 × ↓A → 's0
>>     's0 × τ → 's0

More complex example

val CM = "$".↑ :: "☕".↓ :: ⟲
val CS = "$".↓ :: "☕".↑ :: "✉".↓ :: ⟲

println(dump(toLTS(CM | CS)))

CONSOLE

>> ports:   {☕, $, ✉}
>> actions: {↓☕, ↑☕, ↓✉, τ, ↑$, ↓$}
>> states:  {'s0, 's1, 's2, 's3, 's4, 's5}
>> init:    's5
>> edges:   
>>     's1 × τ → 's3
>>     's3 × ↓✉ → 's5
>>     's3 × ↑$ → 's0
>>     's1 × ↑☕ → 's0
>>     's4 × ↑☕ → 's3
>>     's2 × ↓$ → 's1
>>     's2 × ↓☕ → 's5
>>     's5 × ↑$ → 's2
>>     's4 × ↑$ → 's1
>>     's0 × ↓☕ → 's3
>>     's5 × τ → 's1
>>     's5 × ↓$ → 's4
>>     's0 × ↓✉ → 's2
>>     's1 × ↓☕ → 's4

5) Restriction (|) syntax

val CM = ("$".↑ :: "☕".↓ :: ⟲) \ "$"
println(dump(toLTS(CM)))

CONSOLE

>> ports:   {☕}
>> actions: {↓☕}
>> states:  {'s0, 's1}
>> init:    's1
>> edges:   
>>     's0 × ↓☕ → 's1

val CM = ("$".↑ :: "☕".↓ :: ⟲) \ "$" \ "✉"

val CM = ("$".↑ :: "☕".↓ :: ⟲) \ ("$", "✉")

6) Rename (∘) syntax

val CM = ("$".↑ :: "☕".↓ :: ⟲) ∘ ("$" -> "A")
println(dump(toLTS(CM)))

CONSOLE

>> ports:   {☕, A}
>> actions: {↓☕, ↑A}
>> states:  {'s0, 's1}
>> init:    's1
>> edges:   
>>     's0 × ↓☕ → 's1
>>     's1 × ↑A → 's0

val CM = ("$".↑ :: "☕".↓ :: ⟲) ∘ ("$" -> "A", "☕" -> "B")

Strong / Weak Bisimulation

CCS Bisimulation syntax

import net.golovach.verification.LTSLib._
import net.golovach.verification.ccs.BisimulationLib._
import net.golovach.verification.ccs.CCSLib._

val A = "a".↓

val x = A :: ∅
val y = (A :: ∅) + (A :: ∅)

val isStrongBisimilar:    Boolean = x ~ y
val isNotStrongBisimilar: Boolean = x ≁ y
val isWeakBisimilar:      Boolean = x ≈ y
val isNotWeakBisimilar:   Boolean = x ≉ y

LTS Bisimulation syntax

import net.golovach.verification.LTSLib._
import net.golovach.verification.ccs.BisimulationLib._
import net.golovach.verification.ccs.CCSLib._

val A = "a".↓

val x = (A :: ∅).asLTS
val y = ((A :: ∅) + (A :: ∅)).asLTS

val isStrongBisimilar:    Boolean = x ~ y
val isNotStrongBisimilar: Boolean = x ≁ y
val isWeakBisimilar:      Boolean = x ≈ y
val isNotWeakBisimilar:   Boolean = x ≉ y

Example: University

Source code:

// CM ≡ Cofee Machine
// CSh ≡ Computer Scientist (honest)
// CSr ≡ Computer Scientist (real)
// Univ ≡ University (implementation)
// Spec ≡ Specification

// === impl
val CM = ↑($) :: ↓(☕) :: ⟲
val CSh = ↓($) :: ↑(☕) :: ↓(✉) :: ⟲
val CSr = (↓($) :: ↑(☕) :: ↓(✉) :: ⟲) + (↑(☕) :: ↓(✉) :: ⟲)
val Univ = (CSh | CM | CSr) \ ($, ☕)

// === spec
val Spec = ↓(✉) :: ⟲

println(Univ ~ Spec)
println(Univ ≈ Spec)

CONSOLE

>> false
>> true

Strong Bisimulation algorithm

The algorithms for computing bisimilarity due to Kanellakis and Smolka, (without Paige and Tarjan optimizations), compute successive refinements of an initial partition π-init and converge to the largest strong bisimulation over the input finite labelled transition system. Algorithms that compute strong bisimilarity in this fashion are often called partition-refinement algorithms and reduce the problem of computing bisimilarity to that of solving the so-called relational coarsest partitioning problem.

The basic idea underlying the algorithm by Kanellakis and Smolka is to iterate the splitting of some block Bi by some block Bj with respect to some action a until no further refinement of the current partition is possible. The resulting partition is often called the coarsest stable partition and coincides with strong bisimilarity over the input labelled transition system when the initial partition π-init is chosen to be Proc.

Weak Bisimulation algorithm

The problem of checking weak bisimilarity (observational equivalence) over finite labelled transition systems can be reduced to that of checking strong bisimilarity using a technique called saturation.

golovach-ivan / correct-by-construction Goto Github PK