CSCI P415/515 Fri Jan 6 15:18:04 EST 2012 [SDJ]

Homework Assignment

Introduction to SMV


  1. Run vw on or.smv [SMV] and verify the SPEC formulas using the verify-all command in the Prop menu, or its keyboard shortcut, "a"
  2. For those SPEC statements that are false, examine the counter-scenerios to determine the cause of the failure.
  3. Add SPEC formulas saying:
    1. "It is (im)possible for the first event to be missed."
    2. "It is (im)possible for the first event to counted twice."
    3. "It is (im)possible to count one event three times."
    Construct these formulas to make SMV show you how the eventualities are (im)possible.
  4. Submit a report, report.pdf explaining your findings.

Notes and Hints

The Observer-Reporter Problem

An observer process is monitoring asynchronous events. When it senses an event it increments a counter variable. In pseudocode:

    Observer: while true do
                await EVENT;
                COUNT := COUNT + 1;
A reporter process periodically prints the event tally and clears the counter.
    Reporter: while true do
                wait INTERVAL seconds;
                print(TIME, COUNT);
                COUNT := 0;
These higher level instructions must be compiled into a "machine-level" model whose atomic instructions can only:
The machine model, then, is a traditional one in which "memory" can only hold data, and in order to manipulate date, it must first be brought into the registers of the processor. At this level of atomicity, the processes are:
OBSERVER: {wait for EVENT to occur}
          MOV count, r1   -- retrieve the value of COUNT
          ADD 1, r1, r1   -- increment it
          MOV r1, count   -- store the result
          JMP OBSERVER

REPORTER: {wait for an INTERVAL of time}
          MOV count, r1   -- retrieve the value of COUNT
          MOV 0, count    -- clear the global value
          {Print r1}      -- log the value
          JMP REPORTER