Traffic-Light System

Introduction

This chapter is part of the supplementary material for the practical part of a lecture on formal software verification. The students are given the task to design, implement and verify (the control logic of) a small smart home automation system in C. Here we give a guided example of how this could be done for a traffic light system. This way we can hopefully help the students overcome difficulties with parts of the task that are unclear or unfamiliar. Some of the questions we hope to answer are:

  • How to write such a program in C when I only speak Java?
  • Which level of detail is expected for the project?
  • How do we model the actual system?
  • How do we model safety and liveness properties?
  • How can we model user input?
  • How can we use automatic software verification tools?
  • How can we generate test cases automatically?

The program we will develop can be found in its completeness here: main.c. We will explain parts of it as we go along rather than showing incremental versions of the file, so do not get frightened if you look at it right now, just keep in mind that we always refer to line numbers in this file.

Requirements

The task is to design a traffic light system for a road crossing. So there are four traffic lights where pairs of opposing lights shall always display the same color. The lights have four states: red, green, yellow and off. There is also a switch that has two positions and allows to switch the traffic lights on and off. When switched on, the traffic lights shall begin at either red or green, but not yellow, as this would confuse drivers that are about to enter the crossing. Red shall never be followed directely by green, and green shall never be directely followed by red.

System Design

Before we start and implement the system, we can model one of the lights as transition system as shown in the following figure.

simple implementation automaton
Figure: simple implementation automaton

We start in the state Off, indicating that the light is off. As long as the switch s is off (expressed by the formula "not s"), we stay in this state. When the switch is turned on, the light switches to green (G). As long as the switch stays on, it then transistions from green to yellow to red to yellow and back to green. At every point in this sequence, if the switch is turned of, we transition back to the state Off. We need two different states for yellow to ensure that the automaton does not transition from green to yellow and then back to green. For the other lane, the automaton would look similar, except red and green are switched. This automaton describes one of the many possible implementations that would (hopefully) satisfy the required properties.

System Implementation

Implementing such a (deterministic) finite state machine in C (or really any programming language) is straight forward. We create an enum that allows us to refer to the states in a human-readable manner:

// colors for the traffic light: enum color {Red, Yellow, Green, Off};
main.c:56-57

We then track the state of the automaton in a variable of this type:

// Automaton state variables: enum color stateA = Off;
main.c:64-65

The transition relation of the automaton can be implemented in form of a switch instruction that checks which state we are in and updates the state to the value corresponding to its successor:

// Advances light A by one step. Also only function // to affect the switching direction dir! void stepA() { if (!switchState) { stateA = Off; return; } switch (stateA) { case Red: stateA = Yellow; break; case Yellow: if (dir) { stateA = Green; dir = !dir; } else { stateA = Red; dir = !dir; } break; case Green: stateA = Yellow; break; case Off: if (switchState) { stateA = Green; dir = false; } break; } }
main.c:91-121

Note that we did model the two different yellow states by an additional variable dir that is either 1 or 0. This variable is used to decide whether we come from red or green. It is now easy to extend the program for the other three lights at our crossing:

// Light D shall mimic light A (opposing lanes) void stepD() { stateD = stateA; } // Advances light C by one step. No need to switch dir // since this is already handled by stepA()! void stepC() { if (!switchState) { stateC = Off; return; } switch (stateC) { case Red: stateC = Yellow; break; case Yellow: if (!dir) { stateC = Red; } else { stateC = Green; } break; case Green: stateC = Yellow; break; case Off: if (switchState) { stateC = Red; } break; } } // Light B shall mimic light C (opposing lanes) void stepB() { stateB = stateC; }
main.c:123-161

For finding the right successor, we need to evaluate boolean expressions like "switchState" that depend on external factors. The switch position can be read in from the command line between each step, so which position the switch is in depends on the inputs at runtime:

void getUserInput() { char input[2] = "-"; while (!(input[0]=='1' || input[0]=='0')) { regular_print("Please enter 0 or 1 to indicate traffic light status!"); scanf("%1s",input); } switchState = (input[0]=='1'?true:false); }
main.c:250-257

You are free to implement the system in any way you like and do not need to proceed like just explained, but it is certainly helpful to think about how the system should behave and such an automaton can also help colleagues understand what the system is supposed to do. Another advantage is that you can use the automaton states in your specification.

Depending on your development process, you create the specification before you start thinking about the actual design and implementation. In this case, the specification already talks about states of your system and this often translates naturally into an automaton-backed implementation.

Specification

The requirements included the demand that our system fulfills certain properties. Each of these properties can be expressed by an automaton. For this we use a finite automaton here that accept a sequence of states when a property violation occurs. You are free to define the automaton the other way or use a ω-automaton like Büchi or Muller. The three properties from the requirements correspond to the following automata:

property automaton for "(never) red followed by green"
Figure: property automaton for "(never) red followed by green"
property automaton for "(never) green followed by red"
Figure: property automaton for "(never) green followed by red"
property automaton for "(never) off followed by yellow"
Figure: property automaton for "(never) off followed by yellow"

Note that the edges (and not the nodes) in this automata are labeled with the possible states of the implementation. The automata are allowed to follow an edge if the current state of the implementation is equal to one of the labels on the edge. In other words, the label "G v R" is a guard condition and a short form of the formula "state == G v state == R". This also means that the states in the specification automata cannot generally be associated with a state of the implementation. In our particular case however such an assignment would be possible, e.g. the state 1 in the first automaton corresponds to situations where the traffic light displays red.

We can also take these three automata and combine them into a bigger one. The states of the new automaton can be labeled by triples that consist of the state labels of the individual automata. This results in the following automaton:

joined property automaton constructed from the previous three properties
Figure: joined property automaton constructed from the previous three properties

Here we can identify the three accepting states into a common error state and also find better names for the rest of the states:

joined property automaton with relabeld states and identified error states
Figure: joined property automaton with relabeld states and identified error states

The state that we named "Y" however also represents the initial state where we do not yet know what the first state of the traffic light system will be, so the name "Y" might be a bit misleading here. In other words, "0,0,0" is a state that is neither red nor green nor off.

In our system, we can also add this automaton representing our specification and update its state every time the system itself gets updated. This way, if the specification automaton enters the error state, we know for sure that the specification is violated. In the implementation, instead of directely adding the specification automaton, we just check its transfer relation after every step:

bool successorsValid( enum color firstColor, enum color secondColor) { // switching off can easily be captured in the beginning: if (secondColor == Off) { return true; } // now look at other transitions: switch (firstColor) { case Red: // it shall switch to Yellow or stay Red: return secondColor == Yellow || secondColor == firstColor; case Yellow: // three possibilities: switch to green, to red, or stay yellow: return secondColor == Green || secondColor == Red || secondColor == firstColor; case Green: // it shall switch to Yellow or stay Green: return secondColor == Yellow || secondColor == firstColor; case Off: // it shall stay Off or start with Red or Green: return secondColor == firstColor || secondColor == Red || secondColor == Green; } }
main.c:108-208

This function can be used for all four lights. When it returns false for one of the lights, we know that the specification is violated. The property checks for the complete system is shown here:

bool propertiesHold() { bool violationOccurred = false; if (stateA==Green && dir) { debug_print("[%05u] Violation of invariant: When light A is green, the direction has to be false!\n",stepNumber); violationOccurred = true; } if (!(stateA==stateD)) { debug_print("[%05u] Violation of opposing equality property for A<->C!\n",stepNumber); violationOccurred = true; } if (!(stateB==stateC)) { debug_print("[%05u] Violation of opposing equality property for B<->D!\n",stepNumber); violationOccurred = true; } if (!successorsValid(lastA,stateA)) { debug_print("[%05u] Violation of sequence for A!\n",stepNumber); violationOccurred = true; } if (!successorsValid(lastB,stateB)) { debug_print("[%05u] Violation of sequence for B!\n",stepNumber); violationOccurred = true; } if (!successorsValid(lastC,stateC)) { debug_print("[%05u] Violation of sequence for C!\n",stepNumber); violationOccurred = true; } if (!successorsValid(lastD,stateD)) { debug_print("[%05u] Violation of sequence for D!\n",stepNumber); violationOccurred = true; } //update for next time: lastA=stateA; lastB=stateB; lastC=stateC; lastD=stateD; return !violationOccurred; }
main.c:210-247

We track for each light the last state, check whether the successor state is valid, and update the last state afterwards for the next time we check. We also check whether opposing lights always show the same color (the corresponding automaton is trivial and left as excercise for the reader).

One additional check is implemented that makes sure that the variable dir is always set to 0 when light A is showing green. This is an auxiliary invariant that is useful to check because of the sloppy way we distinguish between the two yellow states. When this invariant is violated, the light would switch from green to yellow and back to green, what is not what we want. In retrospective, this way of implementing the system is error-prone and should be refactored. It is kept this way here to show that strict adherence to the theoretical design is not strictly necessary, but definitely a good idea in order to avoid errors.

Whenever a property is violated, we print a short message on the error output stderr to inform the user which properties are violated, without stopping the system. These messages can also be turned of by removing the comment from line 22. There in the beginning of the file are some lines that start with a "#". These are so called preprocessor commands. The preprocessor is a program that (as the name suggest) runs over the program before the compiler and makes some changes in the file depending on which preprocessor variables are set. Here is the relevant part of our program where preprocessor commands are used:

#include <stdio.h> #include <stdbool.h> // do not define DEBUG to remove debug output //#define DEBUG // do not define REGULAROUTPUT to suppress output to stdout also: //#define REGULAROUTPUT // For verification, define VERIFY in next line: #define VERIFY #ifdef VERIFY extern void __VERIFIER_error(void); extern int __VERIFIER_nondet_int(); extern void __VERIFIER_assume(int ) ; #define VERIFIER_ERROR() __VERIFIER_error() #endif #ifndef VERIFY #define VERIFIER_ERROR() do {} while (0) #endif #ifdef DEBUG #define debug_print(...) \ fprintf(stderr, __VA_ARGS__) #endif #ifndef DEBUG #define debug_print(...) do {} while (0) #endif #ifdef REGULAROUTPUT #define regular_print(...) \ fprintf(stdout, __VA_ARGS__) #endif #ifndef REGULAROUTPUT #define regular_print(...) do {} while (0) #endif // colors for the traffic light: enum color {Red, Yellow, Green, Off}; #ifdef REGULAROUTPUT // matching indices to enum values is dirty, do not do this: const char * colorNames[] = {"Red\t", "Yellow", "Green", "Off\t"}; #endif
main.c:17-61

By removing the comment from line 22 (line 6 in the previous listing), we define the preprocessor variable DEBUG. This way, the preprocessor will replace any function call to debug_print(...) by a call to fprintf(stderr,...). In case DEBUG is not defined, every call to debug_print(...) gets replaced by the effective noop do {} while (0) (a do-while-loop with empty body and unsatisfiable condition). The first two preprocessor commands instruct the preprocessor to inline the content of some header files, which themselves might also include other header files. Since we use some functions from the standard library, we need to import the corresponding headers. If you do not plan printing output or using the bool type, you can omit the inclusion of stdio and stdbool. You can run the preprocessor alone to see what the result looks like. For gcc you do this with this command:

gcc -E main.c -o main.i

Now main.i contains the preprocessed file.

Verification

Now we want to verify that our program fulfills the specification. In order to do this we need to adapt our program in a way that it can be understood by a verifier. The Competition on Software Verification(SVCOMP) has a clear set of rules on how this can be done and all of the participating verifiers understand programs that respect these rules. Basically, we need to tell the verifier which values are non-deterministic (e.g. user input) and when an error has occured. In order to make our program work when compiled with gcc as well as when run by a verifier, we use a preprocessor variable VERIFY. If it is set, this allows us to replace the normal program semantics by the one the verifiers understand. If it is not set, we follow our regular semantics:

#ifdef VERIFY extern void __VERIFIER_error(void); extern int __VERIFIER_nondet_int(); extern void __VERIFIER_assume(int ) ; #define VERIFIER_ERROR() __VERIFIER_error() #endif #ifndef VERIFY #define VERIFIER_ERROR() do {} while (0) #endif
main.c:29-37

For places where an error (specification violation) occurs, we add a call to our preprocessor macro VERIFIER_ERROR. If VERIFY is set, this will expand to a call to __VERIFIER_nondet_error(void). This call will tell the the verifier that an error has been reached. If VERIFY is not set, the macro VERIFIER_ERROR expands to effectively nothing.

Now the only thing that is missing is how to replace the reading of the user input from command line by telling the verifier that the value of switchState shall be nondeterministically chosen to be either 0 or 1:

#ifndef VERIFY void getUserInput() { char input[2] = "-"; while (!(input[0]=='1' || input[0]=='0')) { regular_print("Please enter 0 or 1 to indicate traffic light status!"); scanf("%1s",input); } switchState = (input[0]=='1'?true:false); } #endif #ifdef VERIFY void getUserInput() { switchState = __VERIFIER_nondet_int(); __VERIFIER_assume(switchState==0 || switchState==1); } #endif
main.c:249-264

We do this by using the function __VERIFIER_nondet_int, which tells the verifier to treat the return value of this call as a nondeterministic (signed) integer value. As we only want the values 0 and 1 for switchState, we further limit this range by a call to __VERIFIER_assume, where we pass a condition as argument that has to hold at this point. This way, you can model a wide variety of nondeterministic values. E.g. you could pass the condition switchState % 7 == 0 to only allow multiples of 7 as values.

Using CPAchecker

Now we want to verify our program according to the SVCOMP-ruleset with CPAchecker. You can either download the rease version from the CPAchecker homepage and unpack it:

curl -O https://cpachecker.sosy-lab.org/CPAchecker-1.7-unix.tar.bz2
tar -xf CPAchecker-1.7-unix.tar.bz2
cd CPAchecker-1.7-unix

or clone the repo and compile it:

git clone https://github.com/sosy-lab/cpachecker
cd cpachecker
ant build

Cloning and compiling is preferred because this way you always get the newest version. From now on we assume that you are in the CPAchecker folder and that you also copied main.c into that folder. We run our automatic verification like this:

$ ./scripts/cpa.sh -predicateAnalysis -spec sv-comp-reachability -preprocess ./main.c
Running CPAchecker with default heap size (1200M). Specify a larger value with -heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.
Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 1.7-svn (Java HotSpot(TM) 64-Bit Server VM 1.8.0_171) started (CPAchecker.run, INFO)

line 280: Dead code detected: return 0; (CFACreationUtils.addEdgeToCFA, INFO)

MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions. (PredicateCPA:JavaSMT:Mathsat5SolverContext.<init>, WARNING)

Using predicate analysis with MathSAT5 version 5.5.0 (59014c8d54e1) (Dec  5 2017 11:43:02, gmp 6.1.0, gcc 4.8.5, 64-bit, reentrant) and JFactory 1.21. (PredicateCPA:PredicateCPA.<init>, INFO)

MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions. (ARGCPA:JavaSMT:Mathsat5SolverContext.<init>, WARNING)

MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions. (ARGCPA:JavaSMT:Mathsat5SolverContext.<init>, WARNING)

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner.<init>, INFO)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Stopping analysis ... (CPAchecker.runAlgorithm, INFO)

Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

The listing also includes the output. In The end it states "Verification result: TRUE" which tells us that CPAchecker was able to prove that the call to __VERIFIER_error() can never be reached. It also tells us that further information about the analysis is visualized in the report under output/Report.html. For details about what is shown in the report, please refer to the chapter CPAchecker's HTML Report.

Instead of a predicate analysis (-predicateAnalysis), CPAchecker also provides other kinds of powerful analysis. Explaining what they do is out of scope here, just keep in mind that software verification is a hard problem. Because of this, no verifier is guaranteed to terminate with the right answer. If CPAchecker does not terminate for one kind of analysis, it still might for a different kind of analysis. Other "popular" analysis that you can try are -valueAnalysis or -kInduction, just two name two. You can also try to make the problem easier, e.g. by trying to separate the specified properties and verifying each one individually.

Each of the three mentioned analyses are able to prove our program correct, you can have a look at their reports here:

Using Ultimate Automizer

Since we adapted our program to be verifiable by verifiers participating in the Competition on Software Verification (SV-COMP), we can also try to verify our program using another participant. Ultimate Automizer has a web interface that lets you verify small programs right away from your web browser. For more control and access to Ultimate's log files you can also download the latest version from the github release page. We choose the latter and download the latest version of Ultimate Automizer. After that, we are ready to unpack. We also want to add the specification file for SV-COMP that is currently not shipped with Ultimate Automizer:

~ $ ls
UltimateAutomizer-linux.zip
~ $ unzip UltimateAutomizer-linux.zip
~ $ ls
UltimateAutomizer-linux UltimateAutomizer-linux.zip
~ $ cd UltimateAutomizer-linux
~/UltimateAutomizer-linux $ curl -O https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/svcomp19/c/properties/unreach-call.prp

Now we are inside the Ultimate-Automizer folder and have the right specification named unreach-call.prp. We will assume that the program (our main.c) that we want to verify is also put into that folder. To run Ultimate, we will execute the following command:

python3 Ultimate.py --spec ~/src/sv-benchmarks/c/properties/unreach-call.prp --file main.c --full-output --architecture 32bit

This will currently finish relatively quickly and claim that the verification result is unknown. If we look at the output, this might have to do with the fact that the program was not preprocessed, so we preprocess the file and start Ultimate again, this time on the preprocessed file

gcc -E main.c main.i
python3 Ultimate.py --spec ~/src/sv-benchmarks/c/properties/unreach-call.prp --file main.i --full-output --architecture 32bit

This time Ultimate takes much longer and after around 500 seconds, it spits out a loop invariant with which it is able to prove the program correct:

[...]
Derived loop invariant: ((((((((((!(stateD == stateA) || !(stateC == ~color~0~Off)) || \old(lastA) == ~color~0~Red) && ((!(stateD == stateA) || dir == 0bv8) || !(stateC == ~color~0~Off))) || !(stateB == stateC)) || !(stateA == ~color~0~Off)) || !(\old(lastA) == \old(lastD))) && (((((((((0bv32 == switchState || !(stateD == stateA)) || dir == 0bv8) || !(\old(lastC) == ~color~0~Yellow)) || !(stateA == ~color~0~Red)) || !(\old(lastB) == ~color~0~Yellow)) || !(\old(lastD) == ~color~0~Yellow)) || !(stateB == stateC)) || !(stateC == ~color~0~Green)) || !(\old(lastA) == \old(lastD)))) && (((((!(\old(lastD) == ~color~0~Red) || (((0bv32 == switchState || !(stateD == stateA)) || dir == 0bv8) || !(stateA == ~color~0~Yellow)) || !(stateB == stateC)) || !(\old(lastC) == ~color~0~Green)) || !(\old(lastA) == \old(lastD))) || !(stateC == ~color~0~Yellow)) || !(\old(lastB) == ~color~0~Green))) && (((((((((0bv32 == switchState || !(stateD == stateA)) || !(\old(lastB) == ~color~0~Off)) || !(\old(lastC) == ~color~0~Off)) || !(\old(lastD) == ~color~0~Off)) || !(stateB == stateC)) || !(dir == 0bv8)) || !(stateC == ~color~0~Red)) || !(stateA == ~color~0~Green)) || !(\old(lastA) == \old(lastD)))) && (((((((((0bv32 == switchState || !(stateD == stateA)) || !(\old(lastC) == ~color~0~Yellow)) || !(\old(lastB) == ~color~0~Yellow)) || !(\old(lastD) == ~color~0~Yellow)) || !(stateB == stateC)) || !(dir == 0bv8)) || !(stateC == ~color~0~Red)) || !(stateA == ~color~0~Green)) || !(\old(lastA) == \old(lastD)))) && (((((((((0bv32 == switchState || !(stateD == stateA)) || !(\old(lastB) == ~color~0~Red)) || !(\old(lastD) == ~color~0~Green)) || !(stateA == ~color~0~Yellow)) || !(stateB == stateC)) || !(\old(lastC) == ~color~0~Red)) || !(dir == 0bv8)) || !(\old(lastA) == \old(lastD))) || !(stateC == ~color~0~Yellow))
- StatisticsResult: Ultimate Automizer benchmark data
  CFG has 12 procedures, 100 locations, 2 error locations. SAFE Result, 559.9s OverallTime, 84 OverallIterations, 20 TraceHistogramMax,
[...]

(Currently, Ultimate (the version from the SV-COMP'1)) crashes with a NullPointerException after showing this result, hence finally reporting "UNKNOWN" on the verification task, but this might be different if you use an older/newer version of Ultimate).

results matching ""

    No results matching ""