Formalized Requirements in SLEEC DSL language
The stakeholders corrections after analyzing the well-formedness of the rules using our N-Tool are commented and in blue.
def_start
// Events before driving starts
event UserTurnOnSystem
event UserTurnOffSystem
event TurnOnSensors
event TurnOffSensors
event CheckSystemComponents
event SystemReady
event TakeUserInput
event CalculateShortestPath
event ReadyToDrive
event GetReadyToDrive
event AskIfUserReadyToDrive
event DisplayCarInformation
// Events during driving
event CarDriving
event SlowDown // But not stop completely
// Different than temporarily stopping just by hazards,
// i.e. situation is dangerous and we’re not just temporarily
// stopping for lights
event TurnOnHazardsAndTemporarilyStop
event TemporarilyStopCar // Different than parking, system not turned off
event ParkVehicle // On road shoulder or parking area
// Parking also implies stopping car and turning of system
event DisplayError // Error is internal, i.e car systems not properly working
event DisplayAlert // Alert is external, includes information
event DisplayRoute
event ChangeSpeed
event ChangeLanes
event ChangeCurrentDriving
event TakeNewInput
event TakeShortestPath
event MaintainEqualDistance
event StayCenteredinLane
event SeeTrafficLight
event WaitUntilChanges
event RecordPeople
// User requests related
event UserChangeRoute
event UserCancelPath
event UserRequestSpeedChange
event AskForClarification
// Priority vehicle related
event PriorityVehicleNearby
event MakeSpace // Such as emergency corridor or use the shoulder
// Measures before driving starts
measure destinationExists: boolean
measure pathExists: boolean
// Events during driving
// Sth in front of car, i.e pedestrian, animal, stationary vehicle
measure objectInPath: boolean
measure carsInFront: boolean // Moving thing in front
measure carsBehind: boolean
measure actionIsLegal: boolean
//******** Resolve situation 2 (ADD event)
event StopAutonomousAssistance
*********************************************************************** */
// Priority vehicle related
measure userRequestedLaneChange: boolean
measure ambulanceBehindCar: boolean
measure ambulanceOnOppositeSide: boolean
measure ambulanceNextToCar: boolean
// Other moving vehicles on road, either next to, in front, behind
measure environmentClear: boolean
measure riskLevel: scale(low, medium, high)
measure withinLane: boolean
measure multipleLanes: boolean // Whether 1 lane or multiple
measure commandClear: boolean
measure laneExists: boolean
measure userTurnedOffSystem: boolean
measure recognizeInput: boolean
measure redLight: boolean
measure yellowLight: boolean
measure greenLight: boolean
measure previousLight: scale(red, yellow, green)
measure doorClosed: boolean
measure seatBeltOn: boolean
measure userSaysYes: boolean
measure peopleConsentObtained: boolean
def_end
rule_start
R1 when UserTurnOnSystem then TurnOnSensors
//****** Resolve concern 10 (ADD rule R1b and R1bb)
// Uncomment R1b and R1bb
// R1b when UserTurnOnSystem then not TurnOffSensors
//R1bb when UserTurnOffSystem then TurnOffSensors eventually
*********************************************************************** */
//************************************************************************
//**** Resolve situation 1 (REFINE existing corrected rule: R1b)
// comment R1b, and uncomment R1b below.
// R1b when UserTurnOnSystem and (not {userTurnedOffSystem}) then not TurnOffSensors
*********************************************************************** */
R1_cont when TurnOnSensors then CheckSystemComponents
R2 when SystemReady then TakeUserInput
R3 when TakeUserInput then CalculateShortestPath
unless ((not {destinationExists}) or (not {pathExists})) then DisplayError
R3_cont when CalculateShortestPath then DisplayRoute
R4 when UserRequestSpeedChange and {environmentClear} then ChangeSpeed
unless ({riskLevel} > low)
unless (not {actionIsLegal})
R5 when UserChangeRoute then CalculateShortestPath
unless (not {commandClear}) then AskForClarification
otherwise not ChangeCurrentDriving
R6 when UserCancelPath then ParkVehicle
unless ({riskLevel} > low) then WaitUntilChanges
R7 when CarDriving and ({carsInFront} and {carsBehind}) then MaintainEqualDistance
R8 when CarDriving and {objectInPath} then TemporarilyStopCar
unless ({riskLevel} > low) then ChangeLanes
unless (not {multipleLanes}) then TurnOnHazardsAndTemporarilyStop
unless (not {objectInPath}) then CarDriving
//invalid rules
R9 when CarDriving and {withinLane} then StayCenteredinLane
unless ({userRequestedLaneChange} and ({environmentClear} and ({riskLevel} = low)))
then ChangeLanes
unless ((not {withinLane}) or (not {laneExists})) then DisplayAlert
R10 when UserTurnOffSystem then ParkVehicle
R10_1 when ParkVehicle and {userTurnedOffSystem} then TurnOffSensors
R11 when PriorityVehicleNearby then DisplayAlert
R12 when PriorityVehicleNearby and ({ambulanceBehindCar} and (not {ambulanceOnOppositeSide}))
then ChangeLanes
unless ({ambulanceNextToCar} or (not {multipleLanes})) then MakeSpace
unless ({riskLevel} > low)
R13 when SeeTrafficLight and ({redLight} and {recognizeInput}) then TemporarilyStopCar
unless (not {redLight}) then TakeNewInput // unless is being used as an ‘until’ here
R14 when SeeTrafficLight and ({yellowLight} and {recognizeInput}) then SlowDown
unless (not {yellowLight}) then TakeNewInput
unless ({previousLight} = red) then GetReadyToDrive
R15 when SeeTrafficLight and ({greenLight} and {recognizeInput}) then CarDriving
unless {objectInPath} then WaitUntilChanges
R16 when SeeTrafficLight and (not {recognizeInput}) then SlowDown
R16_cont when SlowDown and {environmentClear} then CarDriving
// Rules 17 and 18 combined
R17 when SystemReady and (not (({doorClosed} or {seatBeltOn}) or {destinationExists}))
then DisplayAlert otherwise AskIfUserReadyToDrive
R19 when AskIfUserReadyToDrive and {userSaysYes} then CarDriving
//******* Resolving situation 3 (REFINE rule) comment R19 and uncomment R19 below
R19 when AskIfUserReadyToDrive and (not {userSaysYes}) then StopAutonomousAssistance
*********************************************************************** */
//** Resolve concern 1 (ADD rule r17b)
// R17b when SystemReady and ({doorClosed} and (({seatBeltOn} and {destinationExists}) and (not {userSaysYes}))) then AskIfUserReadyToDrive
*********************************************************************** */
// Resolve concern (ADD 3 rules, 17bb, 17bbb, and 17bbbb,and REFINE r19)
// Uncomment 17bb, 17bbb, and 17bbbb, r19b, and comment r19
// R17bb when SystemReady and ({doorClosed} and (({seatBeltOn} and {destinationExists}) and (not {userSaysYes}))) then not CarDriving
// R17bbb when SystemReady and ((not {userSaysYes}) and (((not {doorClosed}) or (not{seatBeltOn})) or (not {destinationExists}))) then DisplayError
// R17bbbb when DisplayError then not CarDriving
// R19b when AskIfUserReadyToDrive and (not {userSaysYes}) then not CarDriving
*********************************************************************** */
//****** Resolve situation 2 (REFINING , previous resolved rule, R17bbbb)
// comment R17bbbb and uncomment the rule below.
// R17bbbb when DisplayError then StopAutonomousAssistance
*********************************************************************** */
// Resolve situation 4 (REFINE previous solved rule r17bb)
// comment R17bb and uncomment the rule below.
R17bb when SystemReady and ({doorClosed} and (({seatBeltOn} and {destinationExists}) and (not {userSaysYes}))) then StopAutonomousAssistance
*********************************************************************** */
R20 when SystemReady then DisplayCarInformation
R26 when UserTurnOffSystem then TurnOffSensors eventually
R21 when CalculateShortestPath then TakeShortestPath
unless ({riskLevel} > low)
unless (not {actionIsLegal})
R22 when SystemReady then not RecordPeople
unless {peopleConsentObtained}
R23 when SystemReady then not RecordPeople
unless {peopleConsentObtained}
// *** Resolve redundancies (Delete rule r23 ) **********************
//Comment R23
//************************************************************************
// Resolve concern 2 (ADD rule R24)
// Uncomment R24
// R24 when SystemReady and (not {actionIsLegal}) then ChangeCurrentDriving
//************************************************************************
/** **********************************************************************
/** Resolve concern 6 (ADD rule R25)
/** Uncomment R25
R25 when CarDriving and (not {peopleConsentObtained}) then not RecordPeople
*********************************************************************** */
/** **********************************************************************
/** Resolve concern 12 (ADD rule R27I-R27XII)
/** Add a rule for all car event, to ensure that the recording is consented
/** Uncomment rules R27I to R27XII
R27I when UserTurnOnSystem and (not {peopleConsentObtained}) then not RecordPeople
R27II when TurnOnSensors and (not {peopleConsentObtained}) then not RecordPeople
R27III when SystemReady and (not {peopleConsentObtained}) then not RecordPeople
R27IV when ReadyToDrive and (not {peopleConsentObtained}) then not RecordPeople
R27V when AskIfUserReadyToDrive and (not {peopleConsentObtained}) then not RecordPeople
R27VI when CarDriving and (not {peopleConsentObtained}) then not RecordPeople
R27VII when SlowDown and (not {peopleConsentObtained}) then not RecordPeople
R27VIII when ChangeSpeed and (not {peopleConsentObtained}) then not RecordPeople
R27IX when ChangeLanes and (not {peopleConsentObtained}) then not RecordPeople
R27X when ChangeCurrentDriving and (not {peopleConsentObtained}) then not RecordPeople
R27XI when MaintainEqualDistance and (not {peopleConsentObtained}) then not RecordPeople
R27XII when StayCenteredinLane and (not {peopleConsentObtained}) then not RecordPeople
*********************************************************************** */
rule_end
concern_start
// Safety of the driver and of others in the environment
c1 when SystemReady and ((not {userSaysYes}) and (((not {doorClosed}) or
(not{seatBeltOn})) or (not {destinationExists}))) then CarDriving
// Legal - road rules must be followed
c2 when SystemReady and (not {actionIsLegal}) then not ChangeCurrentDriving
c3 when SeeTrafficLight and ({redLight} and {recognizeInput}) then not TemporarilyStopCar
// Autonomy - user must remain in control as much as possible
c4 when SystemReady and ({doorClosed} and (({seatBeltOn} and {destinationExists}) and (not {userSaysYes}))) then not AskIfUserReadyToDrive
c5 when AskIfUserReadyToDrive and (not {userSaysYes}) then CarDriving
// Privacy - use of cameras attached to car
c6 when CarDriving and (not {peopleConsentObtained}) then RecordPeople
// Accuracy - for deciding routes and destinations
c7 when TakeUserInput and ((not {destinationExists}) or (not {pathExists})) then not DisplayError
// Emergency vehicle related
c8 when PriorityVehicleNearby and ({ambulanceBehindCar} and ((not {ambulanceOnOppositeSide})
and ((not {ambulanceNextToCar}) and ( {multipleLanes} and ({riskLevel} < medium) ))))
then not ChangeLanes
//autonomy
c9 when ReadyToDrive then not ReadyToDrive eventually
c10 when UserTurnOnSystem then TurnOffSensors
c11 when UserTurnOffSystem then not TurnOffSensors eventually
//privacy
c12 when ChangeSpeed and (not {peopleConsentObtained}) then RecordPeople
concern_end
purpose_start
// Safely transport user from A to B
P1 exists CarDriving and (({riskLevel} > low) and {actionIsLegal}) while TakeShortestPath
// Maintain user autonomy
P2 exists AskIfUserReadyToDrive and (({doorClosed} and {seatBeltOn}) and {destinationExists})
P3 exists DisplayCarInformation while SystemReady
// Ensure emergency vehicles are able to carry out their function without unreasonable impediment
P4 exists MakeSpace while PriorityVehicleNearby
// Enable user freedom of movement
P5 exists UserChangeRoute while CarDriving
P6 exists UserCancelPath while CarDriving
P7 exists UserRequestSpeedChange while CarDriving
P8 exists CarDriving and {userRequestedLaneChange}
purpose_end