MOdel-based DEsign & Verification for Safety-Critical Embedded Systems

Traffic Lights Controller

This case study represents the design of traffic lights controller in order to manage North-South (NS) and East-West (EW) roads traffic as shown in Figure below. The NS is main road and potentially allowed green light most of the time. The sensor is attached at EW road to check the presence of vehicle. When EW sensor is activated and NS light is green for enough time then EW light is turned green to pass the traffic on EW road. Emergency sensor is also attached at the NS and EW intersection to manage the passage of emergency vehicles.

Traffic Lights Controller

Following behavioral requirements are captured at higher abstraction level through SYSML State Machine Diagram (SMD):

1) NS light should stay green until one of the EW sensor is activated.
2) If NS green timer is three and NS light is red, then NS light should turn to green.
3) NS light should turn to yellow from green upon the activation of emergency sensor even if the value of NS timer is three.
4) NS green timer should increment on every clock for max. count of three. However, NS green timer should reset to zero on controller reset, or upon NS yellow light. Similar is the case with EW green timer.
5) EW light turn from red to pre green (to enable NS light to turn yellow) in case NS timer is three and EW senor is activated.
6) EW light should turn to green at next clock if it is currently pre green. Similarly, EW light should turn to red if it is currently yellow.
7) EW light should turn to yellow from green if emergency sensor is activated or EW timer is reached to three

We represent structural aspects of traffic lights controller in SYSML Block Definition Diagram (BDD) as shown in Figure below

Structural Aspects

Clock Behavior and NS / EW Timer are implemented in SYSML activity diagram, as shown in Figure below, which are further used in SMD

Clock Behavior and Timer

Behavior of traffic light controller is captured in State Machine Diagram (SMD) as shown in is Figure below

Behavior of Traffic Light Controllers

Verification aspects of traffic lights controller are represented in SVOCL by means of SystemVerilog Assertions as shown in is Figure below

SystemVerilog Assertions in SVOCL