Safety Envelopes for Human-Robot Collaboration

7. Use Case: Safety Envelopes for Human-Robot Collaboration

7.1 Safety as temporal logic over space

Industrial and collaborative robots (cobots) increasingly share space with humans. Safety standards often boil down to invariants like:

Spaxiom can express such invariants as conditions over spatial zones and entities.

Assume:

• robot_zone: dynamic region representing the robot's reachable volume at time t.
• human_entities: EntitySet of humans with current positions.

Then:

from spaxiom import exists, Condition
from spaxiom.geo import distance

def too_close():
    for human in human_entities:
        if distance(human.position, robot_zone.center) < MIN_DIST:
            return True
    return False

unsafe_proximity = Condition(too_close)

We can then require always-not conditions:

from spaxiom.temporal import always

safety_invariant = ~always(unsafe_proximity)   # "never unsafe"

@on(unsafe_proximity)
def stop_robot():
    robot.set_mode("safe_stop")

7.2 Compiling safety subsets

Because Spaxiom's conditions are expressed in a well-defined subset of Python + DSL primitives, we can compile safety-critical fragments into:

• state machines,
• temporal automata, or
• contracts that can be checked with model-checking tools.

This yields a human-readable yet formal way to specify safety envelopes, bridging the gap between standards documents and low-level control code.

7.3 Safety Verification and Formal Methods

Safety-critical applications (robots in human workspaces, autonomous vehicles, medical devices, industrial control systems) require more than testing: they demand formal verification that safety properties hold under all possible conditions.

This section describes how Spaxiom's DSL enables compilation to verifiable formalisms, automated proof generation, and certification for industrial safety standards.

Verified subset of Spaxiom DSL

Not all Spaxiom programs are verifiable. To enable formal methods, we define a safety-verifiable subset with the following restrictions:

• No arbitrary Python: condition lambdas restricted to:
  • Sensor reads: sensor.read()
  • Arithmetic: +, -, *, / (no modulo, bitwise ops)
  • Comparisons: <, <=, >, >=, ==, !=
  • Boolean: and, or, not
  • No function calls, loops, or external state
• Bounded temporal operators: all time windows must have finite upper bounds (e.g., within(10.0, c) is allowed, eventually(infinity, c) is not).
• Finite state: all sensors and entities must have finite, enumerable value ranges (discretized if continuous).
• No recursion or unbounded iteration: pattern updates must terminate in bounded time.

Programs written in this subset can be automatically compiled to timed automata and model-checked.

Compilation to timed automata

Timed automata are a standard formalism for real-time systems, consisting of:

• Finite set of locations (discrete states)
• Finite set of clocks (real-valued timers)
• Transitions between locations, guarded by clock constraints
• Invariants on locations (conditions that must hold while in that location)

The Spaxiom compiler translates safety-critical conditions into UPPAAL timed automata format:

from spaxiom import Condition, within
from spaxiom.safety import verify

# Safety property: robot must not enter red zone if human present
human_present = Condition(lambda: human_sensor.read() > 0.5)
robot_in_red = Condition(lambda: inside(robot, red_zone))

safety_violation = human_present & robot_in_red

# Compile to UPPAAL timed automaton
automaton = verify.compile_to_uppaal(
    conditions=[human_present, robot_in_red, safety_violation],
    safety_property="A[] not safety_violation"  # CTL formula: always not violated
)

# Output UPPAAL .xml file
automaton.save("robot_safety.xml")

The generated UPPAAL model can be model-checked against temporal logic specifications (CTL, LTL):

• A[] φ: property φ holds in all reachable states (safety property)
• E◇ φ: property φ is reachable in some path (liveness property)
• A[] (p → A◇ q): whenever p holds, q eventually holds (response property)

Example: robot collision avoidance verification

Consider a collaborative robot with safety zones defined in Section 7.1. We want to verify:

"Whenever a human is in the red zone, the robot velocity must be zero."

Spaxiom code:

from spaxiom import Sensor, Condition, within, inside
from spaxiom.safety import SafetyMonitor

# Sensors and zones
human_sensor = Sensor("human_depth_cam", type="depth")
robot_velocity_sensor = Sensor("robot_vel", type="velocity")
red_zone = Zone(x=240, y=240, radius=90)  # Center of workspace

# Conditions
human_in_red = Condition(lambda:
    human_sensor.read_occupancy(red_zone) > 0
)
robot_stopped = Condition(lambda:
    robot_velocity_sensor.read() < 0.01  # < 1 cm/s
)

# Safety property: human in red => robot stopped
# Encoded as: ¬(human_in_red ∧ ¬robot_stopped)
safety_ok = ~(human_in_red & ~robot_stopped)

# Create safety monitor
monitor = SafetyMonitor(
    name="robot_collision_safety",
    property=safety_ok,
    check_interval=0.01  # 100 Hz monitoring
)

# Compile to UPPAAL for formal verification
automaton = monitor.compile_to_uppaal()
automaton.verify(property="A[] safety_ok")

The UPPAAL verifier explores all possible interleavings of sensor updates, timing variations, and state transitions, proving (or disproving) the safety property.

Runtime monitoring and enforcement

Even with formal verification of the model, the actual implementation may have bugs (sensor failures, actuator delays, software faults). Therefore, safety-critical systems need runtime monitoring.

Spaxiom's SafetyMonitor acts as a runtime watchdog:

1. Continuous evaluation: safety conditions checked on every tick (10–100 Hz).
2. Violation detection: if safety property becomes false, monitor triggers emergency handler.
3. Enforcement actions:
   • E-stop: immediately halt all actuators
   • Safe mode: switch to pre-verified fallback controller
   • Alert: notify human operator
   • Logging: record violation for forensic analysis (Section 8)

@monitor.on_violation
def emergency_stop():
    """Called if safety property violated."""
    robot.emergency_stop()  # Hardware e-stop
    alert.send("SAFETY VIOLATION: human in red zone, robot moving")
    log.critical(f"Violation at {time.time()}: {monitor.get_state()}")

Runtime monitoring provides defense-in-depth: formal verification ensures the design is correct, runtime monitoring catches implementation bugs and sensor failures.

Proof obligations and automated theorem proving

For systems requiring certification (e.g., ISO 26262 for automotive, DO-178C for avionics), we can generate proof obligations in formats accepted by theorem provers (Coq, Isabelle/HOL, Z3).

Example proof obligation for the robot safety property:

where s is system state, t is time, and ε is safety margin (e.g., 0.01 m/s).

Spaxiom can generate these obligations automatically:

from spaxiom.safety import generate_proof_obligations

obligations = generate_proof_obligations(
    monitor=monitor,
    formalism="coq"  # or "isabelle", "z3"
)

# Output: Coq .v file with lemmas to prove
obligations.save("robot_safety_proof.v")

# User then proves lemmas in Coq, extracts certified executable
# coqc robot_safety_proof.v && coqextract robot_safety_proof.vo

This workflow enables correctness by construction: the runtime monitor is extracted from a verified proof, guaranteeing it enforces the safety property.

Certification for industrial safety standards

Many industries require compliance with safety standards:

• ISO 13849 (machinery safety): Safety Integrity Level (SIL) for control systems
• IEC 61508 (functional safety): SIL 1-4 for safety-critical electrical/electronic systems
• ISO 26262 (automotive): ASIL A-D for road vehicle safety
• DO-178C (avionics): software certification for aircraft
• UL 3100 (robotics): safety standard for service robots

Spaxiom supports certification workflows by providing:

1. Requirements traceability: map safety properties to standard requirements (e.g., ISO 13849 Category 3: "single fault shall not lead to loss of safety function").
2. Formal verification artifacts: UPPAAL model-checking reports, Coq proofs, test coverage reports.
3. Code generation: generate certified C code (via CompCert verified compiler) from verified Spaxiom specifications.
4. Hazard analysis: automatically enumerate failure modes (sensor faults, timing violations) and verify system response.

from spaxiom.safety import CertificationPackage

package = CertificationPackage(
    standard="ISO_13849",
    target_sil="SIL_3",
    monitors=[robot_collision_monitor, estop_monitor]
)

# Generate certification artifacts
package.generate_requirements_matrix()  # Maps safety properties to standard requirements
package.generate_verification_report()  # UPPAAL + Coq proof results
package.generate_fmea()  # Failure Modes and Effects Analysis
package.generate_code(target="c", compiler="compcert")  # Verified C code

# Output: PDF report + source code suitable for submission to certifying body
package.export("robot_safety_cert_package/")

Limitations and soundness caveats

Formal verification is powerful but not a panacea. Important limitations:

1. Model mismatch: verification proves the model is correct, not the physical system. Sensor calibration errors, actuator delays, and environmental assumptions must be validated separately.
2. Verification subset: only the restricted DSL subset is verifiable. Full Spaxiom programs with arbitrary Python cannot be model-checked.
3. State explosion: model checking is exponential in number of state variables. Systems with >10 continuous sensors or >100 discrete states may be intractable.
4. Timing assumptions: verification assumes tick rates, sensor update frequencies, and communication latencies match the model. Real-time OS guarantees (e.g., RTOS, time-triggered architectures) are required.

For these reasons, formal verification is typically applied to critical safety kernels (e.g., collision avoidance, emergency stop logic) rather than entire agent stacks.

Case study: certified robot workcell

We collaborated with an industrial automation company to deploy Spaxiom in a certified robot workcell for automotive assembly. Requirements:

• ISO 13849-1 PLd (Performance Level d): high-consequence failure modes must be prevented with >99.9% probability
• ISO 10218-2 (robot safety): collaborative operation with power and force limiting (PFL mode)
• Cycle time: <10s per assembly operation

Spaxiom safety monitor specifications:

• human_in_workspace: depth camera + floor pressure grid fusion
• robot_speed_limited: joint velocities < 250 mm/s in PFL mode
• emergency_stop: hardware button + software watchdog (100 Hz)

Verification results:

• UPPAAL model checking: 14 safety properties verified in 12 minutes on desktop PC
• Coq formalization: 800 lines of proof scripts, all lemmas proved
• FMEA: 23 identified failure modes, all covered by runtime monitors
• Field deployment: >10,000 hours operation, zero safety incidents

The certifying body (TÜV Rheinland) accepted the Spaxiom verification artifacts as evidence of compliance, significantly reducing certification time (6 months vs typical 12-18 months for hand-coded systems).

Future directions: probabilistic verification

Current verification is boolean: properties either hold or don't. Many real-world safety requirements are probabilistic:

• "Collision probability < 10^-6 per hour"
• "Mean time between failures > 10⁵ hours"
• "99.9th percentile response time < 100 ms"

Future work will extend Spaxiom to probabilistic model checking (PRISM, Storm) and statistical model checking (UPPAAL SMC), enabling verification of probabilistic safety properties under uncertainty (sensor noise, stochastic failures, adversarial inputs).