# Child Presence Detection System (CPDS)

A formally modelled controller for an in-vehicle Child Presence Detection System,
written in [Dezyne](https://verum.com/verumdezyne) and verified against requirements
drawn from the Euro NCAP CPD test protocol and an internal CPDS specification.

The project pairs a model-checked Dezyne component (`CpdController`) with a set
of system-level temporal properties (`.sure` files). Both halves are verified
mechanically — the model with `dzn verify`, the properties with `vsmAssure` —
and then code-generated to C++ for integration into a vehicle stack.

---

## What the controller does

`CpdController` implements the Euro NCAP escalation ladder:

```
Off ──arm──> Armed ──vehicleLocked──> Sensing
              │                        │  │
              │ deactivate       child │  │ empty
              v                  found │  v
        Deactivated                ┌───┘  Off
              │                    v
              │ arm          InitialWarn ──cancel──> Silenced
              v                    │                    │
            Armed             tEscalate            tEscalate
                                   │                    │
                                   v                    v
                              Escalation ◀──child── Rechecking
                                  │  │                │  │
                            cancel│  │tIntervene      │  │empty
                                  v  v                v  v
                              Recheck  Intervention   Off

  doorOpened from any active phase ──> Off
  criticalTemp from any active phase ──> Intervention
```

Phase progression maps to Euro NCAP states **S0 Off → S1 Armed/Scanning →
S2 Child Confirmed → S3 Notify Driver → S4 Exterior Alert → S6 Notify Carers
→ S5 HVAC Intervention → S7 Allow Access → S8 Emergency Services → S9 Standby**.
The controller has **zero local variables** — phase is the interface state of
the `ICpd` provided port, and every other condition is derived from required-port
state booleans. This keeps the model amenable to model checking.

---

## Repository layout

```
Models/
  interfaces/         Port contracts (ICpd, ISensor, IClimate, ...)
  components/
    CpdController.dzn   Main orchestrator (12 invariants, 9 event handlers)
    CpdSystem.dzn       Top-level system wrapping CpdController

Requirements/
  cpd_euro_ncap.sure    Euro NCAP-derived temporal properties (11 assurances)
  cpd_extras.sure       Internal CPDS spec properties (13 assurances)
  cpd_design_gaps.sure  Properties currently held / regression targets (4)

usecase_source/         Source documents (Euro NCAP PDF, Gherkin tests,
                        REQUIREMENT_DEFINITION.txt, VSS catalogue)

src/                    Hand-written C++ glue templates for required ports
main.cpp                Entry point — wires port lambdas, runs the system
CMakeLists.txt          Two-stage build (dzn code → compile)
cmake/                  Helper scripts (forwarding-header writer)
vsm-project.json        VSM project config (paths, top-level system, queue sizes)

build/                  CMake build tree (generated/, cmake/, templates-base/)
.dezyne/                vsmAssure cache and diagrams
```

---

## Ports

| Port | Direction | Interface | Purpose |
|---|---|---|---|
| `api`            | provided | `ICpd`       | Vehicle-facing API (arm, vehicleLocked, doorOpened, userCancel, userDeactivate; warningOn/Off, escalationOn, interventionOn, allClear, deactivated, rearmed) |
| `sensor`         | required | `ISensor`    | Cabin scan (childPresent / cabinEmpty) |
| `signal`         | required | `ISignal`    | Exterior horn + lights |
| `driverNotify`   | required | `INotifier`  | Driver app push (Req_CPDS_02_*) |
| `carerNotify`    | required | `INotifier`  | Predefined-contact push (Req_CPDS_05_*) |
| `door`           | required | `IDoor`      | Unlock for emergency access (5.2.3b) |
| `climate`        | required | `IClimate`   | HVAC + temperature watch (5.2.3c, 5.2.5c) |
| `emergency`      | required | `IEmergency` | eCall / TPS / direct contact (5.2.3a) |
| `telltale`       | required | `ITelltale`  | Deactivation indicator (3.2.11.7) |
| `tEscalate`      | required | `ITimer`     | 90 s warning → escalation (4.2.4.1) |
| `tIntervene`     | required | `ITimer`     | Intervention deadline (5.2.5) |
| `tRecheck`       | required | `ITimer`     | 90 s recheck after cancel (4.2.7.3) |

---

## Toolchain

The project uses a Dezyne distribution from a sibling monorepo. Adjust paths
in [CMakeLists.txt](CMakeLists.txt) and [vsm-project.json](vsm-project.json)
if your install lives elsewhere.

| Tool | Used for | Path (current setup) |
|---|---|---|
| `dzn verify` (via `ide`) | Model checking — deadlock, livelock, illegal, deterministic, compliance | `~/src/dezyne-monorepo/packages/distribution/build/ide` |
| `dzn code`               | C++ code generation from `.dzn` files                                    | `~/src/dezyne-monorepo/packages/distribution/build/dzn` |
| `vsm-project assure`     | Verifies `.sure` requirements via `vsmAssure`                            | `~/src/dezyne-monorepo/apps/vsm-project/build/main.js` |
| Dezyne C++ runtime       | Linked into the executable                                                | `~/src/dezyne-monorepo/packages/distribution/build/runtime/c++` |

---

## Verifying the model

Run `dzn verify` on the controller:

```sh
~/src/dezyne-monorepo/packages/distribution/build/ide \
    -v verify -I . Models/components/CpdController.dzn
```

Expected: every interface and the component pass `deadlock`, `unreachable`,
`livelock`, `deterministic`, `illegal`, and `compliance`. The component carries
twelve named invariants (`INV-01`..`INV-12`) tying interface phase to required-port
state — every reachable configuration must satisfy all of them.

---

## Verifying the requirements

Run `vsm-project assure` from the project root:

```sh
node ~/src/dezyne-monorepo/apps/vsm-project/build/main.js assure
```

Expected (28 assurances total):

```
Requirements/cpd_design_gaps.sure … OK (4/4)
Requirements/cpd_euro_ncap.sure   … OK (11/11)
Requirements/cpd_extras.sure      … OK (13/13)

Summary: 28 passed, 0 failed across 3 files.
```

Results are cached in `.dezyne/sure-cache.json`.

### Where requirements live, and why split

- **Static safety** ("X must be true whenever phase is Y") lives in component
  `invariant` blocks inside [CpdController.dzn](Models/components/CpdController.dzn).
- **Temporal / causal properties** ("after event A, eventually B fires") live in
  the `.sure` files. These cannot be expressed as invariants because they talk
  about events over time, not states.

Two `vsmAssure` shape constraints applied throughout:

1. No OR-combined state predicates inside `while(...)` — the underlying
   `mcf_generation.py` rejects `COr(CEquals,...)`.
2. No `eventually api.<out>()` causal targets — provided-out events are not
   reliably observable in the trace model. Target the required-port side-effects
   (e.g. `signal.activate`, `door.unlock`) that fire in the same atomic handler.

---

## Building and running

The build is a two-stage CMake setup: `dzn code` first generates C++ from every
`.dzn` model, then CMake compiles those generated sources together with the
Dezyne C++ runtime, the hand-written glue in `src/`, and `main.cpp`.

```sh
cmake -S . -B build/cmake
cmake --build build/cmake
./build/cmake/CpdController
```

[main.cpp](main.cpp) currently wires every required-port `in.*` lambda to a
`// TODO` body — this is the integration seam where real sensor / vehicle
adapters plug in. Replace each lambda, then add an event loop that pumps real
events into `system.api.in.*`.

---

## Source documents

See [usecase_source/](usecase_source/) for the originals that drive the model:

- `REQUIREMENT_DEFINITION.txt` — internal CPDS spec (Req_CPDS_00..10), defines
  state ladder S0..S9, timing constants (T_DETECT, T_ACK_1..4, T_SNOOZE),
  sensor catalogue.
- `euro-ncap-cpd-test-and-assessment-protocol-v13.pdf` — Euro NCAP CPD test
  procedure; sections 4.1, 4.2, 5.2, 3.2.11 are referenced throughout the
  model and `.sure` files.
- `TEST CASES_Gherkin.txt` — BDD test scenarios anchored to `Req_CPDS_*` IDs.
- `ChildDetection_vss.json` — VSS signal mapping.
- `CPD_Dezyne_Model.pdf` / `Child Detection Protection System_*.pdf` — design
  notes and reference architecture.

---

## Project conventions

- Phase transitions live exclusively inside `ICpd` (the provided interface).
  The component never fires a `phase = ...` assignment — it fires the
  corresponding `api.<out>()` event and lets the interface advance.
- Required-port state booleans (`sensor.idle`, `climate.cooling`,
  `tEscalate.idle`, ...) are the only auxiliary state. The component declares
  no variables of its own.
- Comments in `.dzn` and `.sure` files reference Euro NCAP section numbers
  and `Req_CPDS_*` IDs verbatim — keep these stable when editing so traceability
  to the source documents survives.
