Nondeterministic Inputs and Transitions

Description of the Case Study

To evaluate how nondeterministic choices impact model checking performance, we extend a standard example in two ways.

We first change the high and low as integers ranging \(0 \ldots k\). Next, the model of #14.1 set the initial condition nondeterministically as a number from \(0 \ldots k\). Another model in #14.2, instead, have high initially as \(0\), but on the next transition, have high set to a number \(\le k\).

The HyperLTL formula used is the classic \(\forall\exists\) non-interference, but with arithmetic comparison instead of simply Boolean matching.

Benchmarks

The Model(s)

-- (hand-craft)
MODULE main
-- A simple program that violates non-interference
-- 1: LOW=0, HIGH={0....10}
-- 2: if(HIGH>5):
-- 3:   LOW=HIGH
--
VAR
  HIGH: 0..12;
  LOW: 0..12;
  PC: 1..3;
ASSIGN
  -- Initial Conditions
  init(HIGH):= {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 12};
  init(LOW):= {0};
  init(PC):= 1; -- program counter starts at 1.

  -- Transition Relations
  next(HIGH) := HIGH;
  next(LOW) :=
    case
      ((PC=2) & (HIGH>6)): HIGH;
      TRUE: LOW;
    esac;
  next(PC) :=
    case
      (PC=3): 3;
      TRUE: PC+1;
    esac;
DEFINE

Formula

forall A. exists B.
F~(*HIGH[A] = HIGH[B]*)
/\
G(*LOW[A] = LOW[B]*)