Figure 1:
Proposed SA-ARTIS-agent architecture.
Figure 2:
Overview of single traffic monitoring station.
Table 1.
Formal verification of the traffic monitoring system.
| Query | Formula | Result |
|---|---|---|
| Is MTM3 signal’s green light working? | EF (MTM Signal.MTM3 Red=0 and MTM Signal.MTM3 Yellow=0 and MTM Signal.MTM3 Green=1) | Satisfied |
| Is MTM3 signal’s yellow light working? | EF (MTM Signal.MTM3 Red=0 and MTM Signal.MTM3 Yellow=1 and MTM Signal.MTM3 Green=0) | Satisfied |
| Is MTM3 signal’s red light working? | EF (MTM Signal.MTM3 Red=1 and MTM Signal.MTM3 Yellow=0 and MTM Signal.MTM3 Green=0) | Satisfied |
| Is MTM4 signal working? | EF ((MTM Signal.MTM4 Red=1 and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=0) or (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=1 and MTM Signal.MTM4 Green=0) or (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=1)) | Satisfied |
| Is MTM4 signal’s green light working? | EF (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=1) | Satisfied |
| Is MTM4 signal’s yellow light working? | EF (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=1 and MTM Signal.MTM4 Green=0) | Satisfied |
| Is MTM4 signal’s red light working? | EF (MTM Signal.MTM4 Red=1 and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=0) | Satisfied |
Figure 3:
Timed Petri-Net model of the Muslim Town Mor signal.
Figure 4:
Self-adaptive SIMBA-Agent architecture.
Figure 5:
Flow chart describing the agent’s initiation and working process.