home
Real-world Use Cases Normative Requirements Repository

AutoCar(Autonomous Car)


AutoCar

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
	  

FOOTER

Praesent tincidunt sed tellus ut rutrum. Sed vitae justo condimentum, porta lectus vitae, ultricies congue gravida diam non fringilla.

Contact

name@domain.com

TAGS

Health care Transport Manifacture Education Environment Social care Deployed Design Prototype