Probabilistic-CCSL TransLator

Train Gate

Train Gate is a railway control system which controls access to a bridge for several trains. The bridge is a critical shared resource that may be accessed only by one train at a time. The scheduling of the trains to access the bridge follows the first-in-first-out (FIFO) strategy. When a train approaches the bridge, if the bridge is occupied or there are trains have arrived earlier, the controller informs the train to stop and wait until its previous trains have left the bridge. Otherwise, the train starts to reach the bridge (within 7-15 time units) and cross the bridge (within 3-5 time units). We consider the following properties on the train gate system (the number of trains is 3).

A1. Two trains can not cross the bridge at the same time.

cross0 is if c[0] then ac else nc;

cross1 is if c[1] then ac else nc;

cross0 excludes(p=0.96) cross1;

A2. The time for all trains to cross the bridge should be greater than 120 time units.

infClk1 is appr[0] inf appr[1];

infClk2 is appr[2] inf infClk2;

supClk1 is leave[0] sup leave[1];

supClk2 is leave[2] sup supClk1;

de is infClk2 delayFor 120 on tu;

de causes(p=0.96) supClk2;

A3. The time for a single train from approaching the gate to completely cross the gate should be within [40, 250] time units.

de1 is appr[1] delayFor 40 on tu;

de2 is appr[1] delayFor 250 on tu;

de1 causes leave[1];

leave[1] causes(p=0.95) de2;

A4. The waiting time for a train (from stop to go) should be less than 200 units of time.

The PrCCSL specifications of the above properties of train gate system is illustrated below:

de3 is stop[0] delayFor 200 on tu;

go[0] causes(p=0.95) de;

Download the Specifications of Train Gate

Figure 1. Verification results of Train Gate system

Bang Bang Control

Bang Bang Control regulates the temperature of a boiler by controlling when the boiler is turned on and off. Initially, the boiler is turned off and the boiler’s LED flashes every 5 seconds. After 40 seconds, if the boiler is cold, i.e., the temperature of the boiler is less than the user-defined reference temperature (represented by ref), the boiler is turned on. After 20 seconds, the boiler is turned off and the bang bang control cycle repeats. We consider the following properties on the system:

B1. If the water of boiler becomes cold, i.e., the temperature of water is less than the user-defined threshold, the boiler should be turned on to heat the water within 5 seconds.

cold_de5 is cold delayFor 5 on sec;

turnOn causes(p=0.98) cold_de5;

B2. When the boiler is off, the LED should flash periodically with a period of 5 seconds.

DenseClockType OffTime{

reference idealClk,

factor    off*1.0,

offset    { },

reset    {turnoff} };

Clock offTime: OffTime;

Clock flash, prdClk;

prdClk is periodicOn offTime period 5;

flash coincides(p=0.98) prdClk;

B3. When boiler is warmed up after being heated for sufficient time, the temperature of boiler should

approach the reference temperature, i.e., temperature should be within [ref-1, ref+1] degree.

DenseClockType temp{

reference idealClk,

factor   tempRate,

offset   { },

reset   { }

};

Clock boiler_temp: temp;

B4. The total energy for the boiler working for one hour should be less than 18kJ.

The PrCCSL specifications of properties for boiler system are presened below:

DenseClockType energy{

reference idealClk,

factor    4.5*On,

offset    {(flash, 5.0), (turnOn, 12.0), (turnOff, 9.0)},

reset     {}

};

Clock boiler_energy: energy;

Download the Specifications of Bang Bang System

Autonomous Vehicle

An autonomous vehicle (AV) reads the road signs, e.g., “speed limit”, “stop” or “right/left turn”, and adjusts speed and movement accordingly. To achieve the function of traffic sign recognition, a camera captures sign images and relays the images to a sign recognition device periodically. We apply ProTL to analyze the following properties on AV:

C1. A Periodic acquisition of camera must be carried out every 500ms with a jitter of 50ms, i.e., any two consecutive triggering of Camera should be within [450, 550]ms.

cmrTrigf is cmrTrig filterBy 01(1);

cmrTrigDe1 is cmrTrig delayFor 450 on ms;

cmrTrigDe2 is cmrTrig delayFor 550 on ms;

cmrTrigDe1 precedes(p=0.96) cmrTrigf;

cmrTrigf precedes(p=0.96) cmrTrigDe2;

C2. If the vehicle detects a left turn sign, it should start to turn left within 300ms.

Clock leftSign, turnLeft, leftSignDe;

leftSignDe is leftSign delayFor 300 on ms;

turnLeft precedes(p=0.98) leftSignDe;

C3. If the vehicle detects a stop sign, it should start to brake within 200ms;

stopSignDe is stopSign delayFor 200 on ms;

startBrake precedes(p=0.95) stopSignDe;

Download the Specifications of Autonomous Vehicle System

Cooperative Automotive System

Cooperative Automotive System (CAS) includes distributed and coordinated sensing, control, and actuation over three vehicles which are running in the same lane. A lead vehicle can run automatically by recognizing traffic signs on the road. The following vehicle must set its desired velocity identical to that of its immediate preceding vehicle. Vehicles should maintain sufficient braking distance to avoid rear-end collision while remaining close enough to guarantee communication quality. Vehicle movement relies on availability of environmental information, e.g., traffic signs, obstacles, etc. The following properties are analyzed:

D1. The movement of the lead vehicle regarding environmental information, the follow vehicle should adjust its movement towards the lead one within a certain time, e.g., 500ms.

leadBrakeDe is leadBrake delayFor 500 on ms;

followBrake precedes(p=0.99) leadBrakeDe;

D2. Authenticity property: If a vehicle receives a message, its preceding vehicle must have sent a corresponding message before, i.e., the protocol should be resistant to message spoofing attack.

msgRec subclock(p=0.95) msgSent;

D3. Freshness property: The vehicles should not accept an “obsolete” message, namely, the difference between the current time and the timestamp of the accepted message should be less than the predefined time threshold.

oldMsg is if time-ts>thre then msgAcpt else nc;

msgAcpt excludes(p=0.95) oldMsg;

D4. The follower vehicle (V1) should not overtake its leading vehicle (V0) when the vehicles run at the positive direction of x-axis.

xdir is if direction==1 then ac else nc;

overtake is if x1>=x0 then ac else nc;

xdir excludes(p=0.95) overtake;

Download the Specifications of Cooperative Automotive System

Google Sites

Report abuse