Verification of State Machines

Problem 1: Traffic Lights

The beauty of finite state machines is that they can be used to model a wide variety of phenomena. For example, a finite state machine can be used to describe the behavior of a system of traffic lights. A single traffic light can be either green (go), yellow (caution), and red (stop).

A four-way intersection typically has one light for each incoming road. However, on many intersections, the behavior of the lights across from each other are symmetric. That is, consider the following intersection:

    A
    |
D ===== B
    |
    C

Because A and C are opposite each other, it is fine if both their lights are green, so they will typically be in sync, likewise with D and B. However, it would be problematic if A and B's lights were synced because then cars driving from A and B might collide into each other.

Because of this, we will model an intersection as a pair of color values, one for each light with the idea that each light represents parallel intersections, i.e., A and C or B and D. On top of this, when both lights become red, we need to know which of the two sets of lights should become green. Therefore, we need to also include a third value in our pair that tells us which light—the first or second element of the pair—should become green once both lights become red.

This leads to the following formal definition of the state of traffic lights at an intersection $S$:

1.a: Code-to-Automata

We can translate these definitions into code pretty easily. Python allows us to write tuples directly, and we can use a string to represent color and a boolean to represent which light will toggle next. For example, the Python expression ('g', 'r', True) captures the state $S$ above. With this, we can give a Python function that simulates a traffic intersection:

def advance_intersection(state):
    match state:
        case ('g', 'r', b):      return ('y', 'r', b)
        case ('y', 'r', b):      return ('r', 'r', b)
        case ('r', 'r', True):   return ('r', 'g', False)
        case ('r', 'g', b):      return ('r', 'y', b)
        case ('r', 'y', b):      return ('r', 'r', b)
        case ('r', 'r', False):  return ('g', 'r', True)

Feel free to try this Python function out and give it some sample inputs, e.g., advance_intersection(('g', 'r', True)), and see how it operates.

Once you are comfortable with the function, draw a finite automata that represents this simulation. You should think carefully about how the different aspects of this problem map to the different components of a finite automata. You do not need to give a formal, symbolic description of the automata.

1.b: Correctness

A properly working intersection does not give right-of-way to perpendicular lights. We'll call such an intersection consistent. An inconsistent intersection is, therefore, one that gives right-of-way to perpendicular lights. Write a Python function, intersection_consistent, that takes a state as input and returns True iff the intersection is consistent.

1.c: A Slight Hiccup

We would like to eventually prove that advance_intersection only produces consistent results. However, it is not always the case that this is true. Show this by proving the following claim:

(Hint: use your finite automata diagram to identify any particular states that don't have reasonable transitions!)

1.d: Fix-ups

What pre-condition do you need on advance_intersection to guarantee that advance_intersection always produces a consistent result? Write the condition formally $P(s)$ as a function of an arbitrary intersection state.

1.e: Proof of Correctness

With the precondition $P(s)$ that you identified in the previous part, finally prove the correctness of advance_intersection:

Problem 2: Servers

Another example of a finite state machine is a server-style program that hosts data, public and private. The server allows users to optionally authenticate after connecting to enable them to read private data in addition to public data. While we would need to appeal to networking and database libraries to properly implement such a server, we can emulate the authentication portion of the system with simple Python code.

First, let's define the series of commands we can issue to the server as a collection of strings:

• "Connect": connects to the server
• "ReadPublic": reads public data from the server
• "Authenticate": authenticates with the server
• "ReadPrivate": reads private data
• "Disconnect": disconnects from the server

A session is a sequence of these commands.

Next we'll formalize the rules of the server, i.e., what constitutes a valid session:

1. A user must connect before reading or authenticating to the server.
2. A user must authenticate before reading private data.
3. A user must be disconnected at the end the session.

The state of a session, then, consists of two parts: whether a client is connected to the server and whether the client is authenticated. We'll represent this with a pair of booleans.

Problem 2a: Translation

Below is a candidate implementation of this protocol, a function that takes the current server state and a command and returns the updated state:

def process_command (state, cmd):
    (connected, authenticated) = state
    match cmd:
        case 'Connect':
            if not connected:
                print("Connected")
                return (True, authenticated)
            else:
                raise RuntimeError("Tried to connect but already connected")
        case 'ReadPublic':
            if connected:
                print("Reading public data")
                return (connected, authenticated)
            else:
                raise RuntimeError("Tried to read before connecting")
        case 'Authenticate':
            if connected and not authenticated:
                print("Authenticated")
                return (connected, true)
            elif not connected:
                raise RuntimeError("Tried to authenticate before connecting")
            else:
                raise RuntimeError("Tried to authenticate but already authenticated")
        case 'ReadPrivate':
            if connected and authenticated:
                print("Read private data")
                return (connected, authenticated)
            elif not connected:
                raise RuntimeError("Tried to read before connecting")
            else:
                raise RuntimeError("Tried to read private data before authenticating")
        case 'Disconnect':
            if connected:
                print("Disconnected")
                return (false, authenticated)
            else:
                raise RuntimeError("Tried to disconnect but not connected")

From the code, write down a finite state machine that captures this protocol.

Problem 2b: Problems

If you didn't see already, it turns out there is a serious flaw in our implementation of the server protocol! Prove the following claim:

Problem 2c: Fix-ups

Correct your finite automata from problem 2a so the problem from the previous part is resolved. Use this new finite automata to rewrite the code so that it is correct!