Vos systèmes, écrits comme du code.

message POINT_CLOUD "Point cloud" { nearest: float32 }
message BRAKE_CMD "Brake command" { force: float32; emergency: bool }
message ENGAGE "Engage" { on: bool }

const MAX_SPEED = 40.0

requirement REQ-AEB "Emergency braking" {
  text "The car shall brake within 40 ms of an obstacle closer than 30 m."
  verified-by TP-AEB
}

component Lidar "Lidar" {
  out cloud: can sends POINT_CLOUD
}

component Hmi "Driver panel" {
  out bus: can sends ENGAGE
}

/// The driving computer: it brakes when an obstacle is close.
component Adcu "Driving computer" {
  satisfies REQ-AEB
  in sense: can { handler POINT_CLOUD -> on_cloud }
  in hmi: can receives ENGAGE
  out brake: can sends BRAKE_CMD
  var speed: float32 = 0 unit m/s

  fn on_cloud(nearest: float32) ```arche
    if state == Autonomous and nearest < 30.0 {
      send brake BRAKE_CMD { force: 8000.0, emergency: true }
    }
  ```

  states {
    state Manual
    state Autonomous
    Manual -> Autonomous on ENGAGE [self.speed < MAX_SPEED]
    Autonomous -> Manual on ENGAGE
  }
}

component Brakes "Brakes" {
  in cmd: can receives BRAKE_CMD
}

system Car "Car" {
  part lidar: Lidar
  part hmi: Hmi
  part adcu: Adcu
  part brakes: Brakes
  lidar.cloud -> adcu.sense { latency 1ms }
  hmi.bus -> adcu.hmi
  adcu.brake -> brakes.cmd
}

test-plan TP-AEB "Emergency braking" {
  case TC-AEB-01 "Obstacle at 20 m" {
    verifies REQ-AEB
    at 0ms do send(hmi.bus, ENGAGE(on=True))
    at 10ms expect adcu.state == "Autonomous"
    at 10ms do send(lidar.cloud, POINT_CLOUD(nearest=20.0))
    within 40ms expect sent("BRAKE_CMD") >= 1
  }
}