Back to Project Page

Firefighter Scenario

A case study showcasing SLEEC@run.time in an emergency-response setting

This scenario is used in “A Process to Enforce Ethical Requirements of Autonomous Systems at Runtime” (SEAMS 2026).
See the related process documentation here.

Case Study Ref. Code

Scenario Overview

The firefighter scenario consists of an uncrewed aerial vehicle (UAV) designed to support wildfire and urban fire response operations. The UAV collaborates with human firefighters, bystanders, and remote teleoperators to improve situational awareness and early intervention. Its primary tasks include detecting potential fires, such as warehouse fires, using a thermal camera, localizing the fire with a depth camera, and reporting the situation by transmitting video footage of the surveyed building to teleoperators. When appropriate, the UAV can also deploy onboard water spraying to help contain the fire until human firefighters arrive on site.
In addition to these functional capabilities, the firefighter UAV must address SLEEC considerations that arise from interacting with people. For example, activating an onboard loudspeaker alarm near bystanders may cause social disturbances, while transmitting video footage can raise legal or ethical privacy concerns when individuals are present in the monitored area.

Yaman, Sinem Getir, et al. "Specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agents."
Journal of Systems and Software 220 (2025): 112229.

Elicited SLEEC Rules

  1. Rule 1
    WHEN CameraStart AND personNearby
    THEN SoundAlarm
  2. Rule 2
    WHEN CameraStart AND personNearby
    THEN SoundAlarm WITHIN 2 seconds
  3. Rule 3
    WHEN SoundAlarm
    THEN not GoHome WITHIN 5 minutes
  4. Rule 4
    WHEN CameraStart
    THEN SoundAlarm
    UNLESS personNearby THEN GoHome
    UNLESS temperature > 35

Rule Formal Specification and Analysis

Below is the formal specification of the firefighter scenario in ASMETA language.

firefighterHeader.asm


module firefighterHeader 

import ../libraries/StandardLibrary
import ../libraries/SLEECLibrary
export *

signature:	
    /* DOMAIN-SPECIFIC SIGNATURE */
    
    //domains
    domain Temperature subsetof Real
    enum domain WindScale = {LIGHT,MODERATE,STRONG}
    enum domain CapabilityID = {DONOTHING,SOUNDALARM,GOHOME}
    
    //Events and sensed variables
    monitored batteryCritical: Boolean
    monitored cameraStart: Boolean
    monitored alarmRinging: Boolean //To not confuse with the obligation soundAlarm
    monitored personNearby: Boolean
    monitored temperature: Temperature 
    monitored windSpeed: WindScale
    static alarmdeadline: Integer //constant
    
    //Capabilities
    static goHome: Capability
    static soundAlarm: Capability
    static id: Capability -> CapabilityID //not in lib, since it depends on CapabilityID that is model-specific
    
/* CONSTANT (DOMAIN-GENERAL) SIGNATURE */	
    //NEW (compact, aggregated output)
    controlled info: Capability -> Prod(CapabilityID,TCType,Integer,TimerUnit,CapabilityID) //examples: (GOHOME,AFTER,5,MIN,undef), (GOHOME,WITHIN,8,MIN,SOUNDALARM)
    //out outObligation: CapabilityID //OLD
    out outObligation: CapabilityID -> Boolean //NEW: any due obligation (there could be more than one) is activated through a flag
    out outConstraint: CapabilityID -> Prod(TCType,Integer,TimerUnit,CapabilityID)

    
definitions:
        
/* DOMAIN-SPECIFIC DEFINITIONS*/
    
    domain Temperature = {-5.0:50.0}
    
    function alarmdeadline = 30
    
    function id($c in Capability) = 
        switch $c
            case doNothing : DONOTHING
            case goHome : GOHOME
            case soundAlarm : SOUNDALARM
        endswitch	
    
    
/* CONSTANT (DOMAIN-GENERAL) DEFINITIONS */	
    //with no time constraint
    rule r_setObligation($c in Capability) = 
    par 
        doObligation($c) := true //NEW
        constraint($c) := none
        info($c) := (id($c),undef,undef,undef,undef)
        //prepare out locations
        outObligation(id($c)) := true //true if doObligation is true 
        outConstraint(id($c)) := undef //(undef,undef,undef,undef) 
    endpar
    
    //complete overloading
    rule r_setObligation($c in Capability, $type in TCType, $t in Integer, $u in TimerUnit, $alt in Capability) = 
    par 
        doObligation($c) := true //NEW
        r_setTimeConstraint[$c,$type,$t,$u]
        if isDef($alt) then otherwiseC($c) := $alt endif
        info($c) := (id($c),$type,$t,$u,id($alt))
        //prepare out locations
        outObligation(id($c)) := true  //NEW
        outConstraint(id($c)) := ($type,$t,$u,id($alt))
    endpar

firefighter.asm


asm firefighter

import ../libraries/StandardLibrary
import ../libraries/SLEECLibrary
import firefighterHeader

signature: 
    
definitions:
    

    /* DOMAIN-SPECIFIC CONTROL RULES*/
    
        
    //default: no obligation to do
    rule r_doNothing = r_setObligation[doNothing]
    
    rule r_soundAlarm = r_setObligation[soundAlarm]
            
    rule r_soundAlarmWithinTwoSeconds = r_setObligation[soundAlarm,WITHIN,2,SEC,doNothing]
    
    rule r_goHome = r_setObligation[goHome]
        
    rule r_goHomeAfterFiveMinutes = r_setObligation[goHome,AFTER,5,MIN,doNothing]

    rule r_goHomeWithinOneMinute = r_setObligation[goHome,WITHIN,1,MIN,doNothing]
    
    
    //legal, social
    rule r_Rule1 =
        if cameraStart and personNearby then r_soundAlarm[] endif 	
    
    //legal, ethical	
    rule r_Rule2 =
        if cameraStart and personNearby then r_soundAlarmWithinTwoSeconds[] endif
            
    //legal		
    rule r_Rule3 =
        //if alarmRinging then r_goHomeAfterFiveMinutes[] endif 
        r_SLEEC[alarmRinging,<<r_goHomeAfterFiveMinutes>>]
        
    rule r_RuleA =
        //if batteryCritical and temperature < 25.0 then r_goHomeWithinOneMinute[] endif 
        r_SLEEC[batteryCritical and temperature < 25.0,<<r_goHomeWithinOneMinute>>]
        
    //emphatatic	
    rule r_Rule4 =
        r_SLEEC[cameraStart, <<r_soundAlarm>>, personNearby, <<r_goHome>>, temperature > 35.0, <<r_doNothing>>]
        
        
    /* CONSTANT (DOMAIN-GENERAL) RULES*/
    

    //reset of all locations that contribute to the out location output
    rule r_Reset =
            forall $c in Capability do 
                par
                info($c) := (undef,undef,undef,undef,undef)
                outConstraint(id($c)) := undef //(undef,undef,undef,undef)
                doObligation($c) := false //NEW
                outObligation(id($c)) := false //NEW
                constraint($c) := undef
                otherwiseC($c) := undef
            endpar
    
    
    invariant inv_I0 over  doObligation, outObligation: (forall $c in Capability with (doObligation($c) = outObligation(id($c)) ))
    
    
    
    /* DOMAIN-SPECIFIC RULES*/
        
    main rule r_Main =  
        seq	
            r_Reset[] //reset of out locations in sequential order, otherwise the function resetting updates will not be visible to the other rules in one machine step
            //par 
            //Rule1 and Rule2 are redundant (inconsistent update on secondary attributes of the doOblication) 
            //r_Rule1[]
            //r_Rule2[]
            //r_Rule3[] //Rule1 and RuleA are in conflict (inconsistent update on doOblication: e.g. doObligation updated to soundAlarm and goHome) [From the source spec: they are conflicting rules: RuleA requires GoHome to take place, but Rule3 forbids it.
            r_Rule4[] 
            r_RuleA[]
            //example of SLEEC rule covering all modeling constructs
            //r_SLEEC[cameraStart, <<r_soundAlarm>>, personNearby, <<r_goHomeWithinOneMinute>>, temperature > 35.0, <<r_goHomeAfterFiveMinutes>>]
            //endpar
        endseq

default init s0:

Enforcement Subsystem Development and Running

Below we report a runtime execution trace produced by the enforcement subsystem, showing input conditions, rule evaluation, and applied actions.

Enforcement output

[INFO] Executing new step.
[INFO] Received input conditions: 
    ('batteryCritical': False, 
    'cameraStart': True,
    'alarmRinging': False, 
    'personNearby': True,
    "temperature': 10.0,
    'windSpeed': 'STRONG', 
    'alarmdeadline': 30} 

[INFO] ASM step performed for ID 1 with delay 40.33 ms

[INFO] ASM output: 
    ['outObligation(GOHOME)': 'true',
    'outConstraint(SOUNDALARM)': 'undef',
    'outobligation(DONOTHING)': 'false',
    'outobligation(SOUNDALARM)': 'false',
    'outConstraint(GOHOME)': 'undef',
    'outConstraint(DONOTHING)': 'undef"}

[INFO] Enforcement applied.

Enforcement output (from the terminal)

Enforcement Subsystem Architecture
Click to enlarge the enforcement subsystem output.