From 792b4f1b17e34f98658a749ffd4f8b0fd715101c Mon Sep 17 00:00:00 2001 From: Julien Calixte Date: Thu, 2 Jul 2026 23:52:13 +0200 Subject: [PATCH] feat: add BLE blueprint illustration A central with two lifecycles: an adapter/scan machine (doubly gated by Permission + a powered-on radio) and a per-peripheral link machine, with a bespoke specimen mocking the scanner and connected-device screens. --- src/components/StateMachine.vue | 18 ++ src/data/bleBlueprint.ts | 388 ++++++++++++++++++++++++++ src/data/blueprint.ts | 22 ++ src/data/blueprints.ts | 3 + src/specimens/BleSpecimen.vue | 481 ++++++++++++++++++++++++++++++++ 5 files changed, 912 insertions(+) create mode 100644 src/data/bleBlueprint.ts create mode 100644 src/specimens/BleSpecimen.vue diff --git a/src/components/StateMachine.vue b/src/components/StateMachine.vue index c00f224..9675c7d 100644 --- a/src/components/StateMachine.vue +++ b/src/components/StateMachine.vue @@ -112,6 +112,15 @@ const KIND_LABELS: Record = { signout: "signOut()", reset: "reset()", unlock: "unlock()", + powerOn: "powerOn()", + powerOff: "powerOff()", + startScan: "startScan()", + stopScan: "stopScan()", + discover: "discover(p)", + connect: "connect()", + discoverServices: "discoverServices()", + exchange: "read / write / subscribe", + disconnect: "disconnect() / drop", } const KIND_ORDER: SmKind[] = [ "submit", @@ -131,6 +140,15 @@ const KIND_ORDER: SmKind[] = [ "revoke", "expire", "clear", + "powerOn", + "powerOff", + "startScan", + "stopScan", + "discover", + "connect", + "discoverServices", + "exchange", + "disconnect", ] // Lay the legend out left-to-right, wrapping to a new row when it would overflow diff --git a/src/data/bleBlueprint.ts b/src/data/bleBlueprint.ts new file mode 100644 index 0000000..ce87ee7 --- /dev/null +++ b/src/data/bleBlueprint.ts @@ -0,0 +1,388 @@ +// The BLE blueprint, as data. Transcribed by hand from the ontology `ble` +// README + ble.als. A *feature* — a device acting as a Bluetooth Low Energy +// *central*: it scans for advertising peripherals, connects to one, and +// reads/writes/subscribes to its GATT characteristics over a link that may drop +// at any time. It composes the Permission capability, which owns the consent +// lifecycle that gates startScan(). +// +// BLE has TWO independent lifecycles, so it renders two state machines: +// 1. adapter + scan (central-level) — the radio power and the scan loop, +// doubly gated by Permission + a powered-on radio; +// 2. per-peripheral link — Disconnected → Connecting → Connected → Ready, +// with drop/disconnect returns and on-Ready GATT exchange. + +import type { Blueprint, StateMachine } from "./blueprint" + +// ── Machine 1 · adapter + scan (central) ─────────────────────────────────── +// The README nests ScanIdle/Scanning inside a PoweredOn superstate; the flat +// diagram unfolds that superstate into its two substates. powerOn() enters at +// ScanIdle; powerOff() forces the central dormant from either substate (two +// edges back to PoweredOff). discover(p) is the OS callback that accumulates +// peripherals while Scanning — a self-loop. +const BLE_ADAPTER_MACHINE: StateMachine = { + initId: "poweredoff", + caption: "Adapter + scan · central", + field: "adapter : AdapterState · scan : ScanState", + nodes: [ + { id: "poweredoff", x: 60, y: 150, w: 130, h: 44, label: "PoweredOff" }, + { id: "scanidle", x: 360, y: 150, w: 120, h: 44, label: "ScanIdle" }, + { id: "scanning", x: 660, y: 150, w: 120, h: 44, label: "Scanning" }, + ], + edges: [ + // forward path (arcs up, labels above the row) + { from: "poweredoff", to: "scanidle", label: "powerOn()", kind: "powerOn", off: -34 }, + { + from: "scanidle", + to: "scanning", + label: "startScan() [granted]", + kind: "startScan", + off: -34, + }, + // recurring OS callback while scanning + { from: "scanning", to: "scanning", label: "discover(p)", kind: "discover", off: 0 }, + // returns (arc below the row; deeper = wider span) + { from: "scanning", to: "scanidle", label: "stopScan()", kind: "stopScan", off: -55 }, + { from: "scanidle", to: "poweredoff", label: "powerOff()", kind: "powerOff", off: -95 }, + { from: "scanning", to: "poweredoff", label: "powerOff()", kind: "powerOff", off: -145 }, + ], +} + +// ── Machine 2 · per-peripheral link ──────────────────────────────────────── +// Disconnected → Connecting → Connected → Ready. established()/connectFail() are +// the two OS resolutions of a connect() attempt. On Ready, read/write/subscribe +// leave the state unchanged (self-loop). disconnect()/drop returns to +// Disconnected from either Connected or Ready, invalidating cached handles. +const BLE_LINK_MACHINE: StateMachine = { + initId: "disconnected", + caption: "Link lifecycle · per peripheral", + field: "peripheral.link : LinkState", + nodes: [ + { id: "disconnected", x: 40, y: 150, w: 140, h: 44, label: "Disconnected" }, + { id: "connecting", x: 290, y: 150, w: 125, h: 44, label: "Connecting" }, + { id: "connected", x: 525, y: 150, w: 125, h: 44, label: "Connected" }, + { id: "ready", x: 760, y: 150, w: 95, h: 44, label: "Ready" }, + ], + edges: [ + // forward path (arcs up, labels above the row) + { from: "disconnected", to: "connecting", label: "connect()", kind: "connect", off: -34 }, + { from: "connecting", to: "connected", label: "established()", kind: "succeed", off: -34 }, + { + from: "connected", + to: "ready", + label: "discoverServices()", + kind: "discoverServices", + off: -34, + }, + // on-Ready GATT operations — state unchanged (self-loop) + { from: "ready", to: "ready", label: "read / write / subscribe", kind: "exchange", off: 0 }, + // returns to Disconnected (arc below the row; deeper = wider span) + { from: "connecting", to: "disconnected", label: "connectFail()", kind: "fail", off: -55 }, + { from: "connected", to: "disconnected", label: "disconnect()", kind: "disconnect", off: -100 }, + { + from: "ready", + to: "disconnected", + label: "disconnect() / drop", + kind: "disconnect", + off: -150, + }, + ], +} + +export const ble: Blueprint = { + slug: "ble", + name: "BLE", + tagline: + "A device acting as a Bluetooth Low Energy central — scan for advertising peripherals, connect to one, and read/write/subscribe to its GATT characteristics over a link that may drop at any time.", + role: "feature", + composesCount: 1, + + sig: { + header: "Central", + fields: [ + { name: "permission", type: "one Permission", note: "consent state (owned by Permission)" }, + { name: "adapter", type: "one AdapterState", note: "radio power: PoweredOff | PoweredOn" }, + { name: "scan", type: "one ScanState", note: "ScanIdle | Scanning" }, + { name: "discovered", type: "set Peripheral", note: "peripherals seen while scanning" }, + ], + types: [ + "AdapterState = PoweredOff | PoweredOn", + "ScanState = ScanIdle | Scanning", + "LinkState = Disconnected | Connecting | Connected | Ready", + "Peripheral { link : LinkState, characteristics, subscriptions : set Characteristic }", + "scan = Scanning ⟹ permission = Granted ∧ adapter = PoweredOn (doubly gated)", + "some p.characteristics ⟹ p.link = Ready", + "subscriptions ⊆ characteristics", + ], + }, + + functions: [ + { + id: "permission", + name: "Permission", + fig: "01", + caps: ["Permission"], + verb: "Hold the single consent status and gate startScan() behind it; delegate request/grant/deny to the Permission capability.", + state: [["permission.status", "PermissionStatus"]], + behaviors: [ + { + sig: "requestPermission()", + pre: "permission.status = NotAsked", + eff: "delegates to Permission.request; rest of Central preserved", + }, + { + sig: "grant()", + pre: "permission.status = Requested", + eff: "delegates to Permission.grant; rest of Central preserved", + }, + { + sig: "deny()", + pre: "permission.status = Requested", + eff: "delegates to Permission.deny; scan ← ScanIdle", + }, + ], + invariants: [ + "scan = Scanning ⟹ permission.status = Granted — consent is one of the two scan gates", + "Granted and Denied are terminal from the capability's view — the app cannot re-prompt the OS dialog", + ], + failures: [ + "Location coupling — Android < 12 requires ACCESS_FINE_LOCATION to scan; a confusing permission prompt blocks scanning entirely if location is denied", + ], + perf: [], + notes: [ + "The three permission behaviors compose Permission's transitions with a frame condition on the rest of Central. On Web, navigator.bluetooth.requestDevice() has the browser render the chooser — silent enumeration is impossible.", + ], + }, + { + id: "power", + name: "Power", + fig: "02", + caps: ["BLE"], + verb: "Track the adapter's on/off state; force the central fully dormant the moment the radio powers off.", + state: [ + ["adapter", "AdapterState"], + ["scan", "ScanState"], + ], + behaviors: [ + { + sig: "powerOn()", + pre: "adapter = PoweredOff", + eff: "adapter ← PoweredOn; scan ← ScanIdle", + }, + { + sig: "powerOff()", + pre: "adapter = PoweredOn", + eff: "adapter ← PoweredOff; scan ← ScanIdle; discovered ← ∅", + }, + ], + invariants: [ + "adapter = PoweredOff ⟹ scan = ScanIdle ∧ every known peripheral is Disconnected — a dead radio is fully dormant", + "scan = Scanning ⟹ adapter = PoweredOn — a live radio is the second scan gate", + ], + failures: [ + "Adapter off mid-session — the user toggles Bluetooth off in Control Center / Settings; every link drops and subscriptions are lost, so the app must observe adapter state and clean up", + ], + perf: [], + notes: [ + "powerOn/powerOff are OS/user events, not app calls — the app reacts to them. Losing the radio is modelled as the central collapsing to its dormant state.", + ], + }, + { + id: "scan", + name: "Scan", + fig: "03", + caps: ["BLE", "Permission"], + verb: "Discover advertising peripherals once doubly gated (Granted + PoweredOn) and accumulate them into the discovered set.", + state: [ + ["scan", "ScanState"], + ["discovered", "set Peripheral"], + ], + behaviors: [ + { + sig: "startScan()", + pre: "permission = Granted; adapter = PoweredOn; scan = ScanIdle", + eff: "scan ← Scanning", + }, + { + sig: "discover(p)", + pre: "scan = Scanning", + eff: "discovered ← discovered ∪ {p}", + }, + { sig: "stopScan()", pre: "scan = Scanning", eff: "scan ← ScanIdle" }, + ], + invariants: [ + "scan = Scanning ⟹ permission = Granted ∧ adapter = PoweredOn — scanning is doubly gated", + ], + failures: [ + "Scan drain — startScan() never paired with stopScan(); a continuous radio scan drains the battery and Android throttles or drops results", + ], + perf: [ + "First advertisement — a discovered peripheral surfaces within ~1 s of startScan() under normal RF conditions", + ], + notes: [ + "discover(p) is an OS callback fired repeatedly while Scanning — a self-loop that grows the discovered set without changing state.", + ], + }, + { + id: "connect", + name: "Connect", + fig: "04", + caps: ["BLE", "Peripheral"], + verb: "Establish the link to a chosen peripheral and tear it down; resolve both the successful connection and involuntary drops.", + state: [["peripheral.link", "LinkState"]], + behaviors: [ + { sig: "connect(p)", pre: "p.link = Disconnected", eff: "p.link ← Connecting" }, + { sig: "established(p)", pre: "p.link = Connecting", eff: "p.link ← Connected" }, + { sig: "connectFail(p)", pre: "p.link = Connecting", eff: "p.link ← Disconnected" }, + { + sig: "disconnect(p)", + pre: "p.link ≠ Disconnected", + eff: "p.link ← Disconnected; characteristics, subscriptions ← ∅", + }, + ], + invariants: [ + "p.link = Disconnected ⟹ no p.characteristics ∧ no p.subscriptions — a dropped link invalidates every cached handle", + ], + failures: [ + "Silent disconnect — the peripheral moves out of range or its battery dies; link → Disconnected with no app-initiated call and cached handles go stale", + ], + perf: [ + "Connection establishment — Connecting → Connected within ~2–3 s of connect() (bounded by the connection interval)", + ], + notes: [ + "disconnect(p) covers both an app-initiated teardown and an involuntary drop (out of range, peripheral power-off) — either way, cached handles are invalidated.", + ], + }, + { + id: "discover-services", + name: "Discover", + fig: "05", + caps: ["Peripheral", "Characteristic"], + verb: "Enumerate the peripheral's GATT services and characteristics once the link is Connected, promoting it to Ready.", + state: [ + ["peripheral.link", "LinkState"], + ["peripheral.characteristics", "set Characteristic"], + ], + behaviors: [ + { + sig: "discoverServices(p, cs)", + pre: "p.link = Connected", + eff: "p.link ← Ready; p.characteristics ← cs", + }, + ], + invariants: [ + "some p.characteristics ⟹ p.link = Ready — GATT handles exist only after service discovery completes", + ], + failures: [ + "Stale handle reuse — reconnect and reuse cached handles without re-discovering; reads/writes target invalid handles and return GATT errors (invariant #5 exists to prevent this)", + ], + perf: [], + notes: [ + "Ready is the only state in which characteristic handles are valid; a drop clears them, so handles must be re-discovered after every reconnect.", + ], + }, + { + id: "exchange", + name: "Exchange", + fig: "06", + caps: ["Peripheral", "Characteristic"], + verb: "Read, write, and subscribe to characteristic values over a Ready link, against discovered characteristics only.", + state: [ + ["peripheral.characteristics", "set Characteristic"], + ["peripheral.subscriptions", "set Characteristic"], + ], + behaviors: [ + { + sig: "subscribe(p, ch)", + pre: "p.link = Ready; ch ∈ p.characteristics", + eff: "p.subscriptions ← p.subscriptions ∪ {ch}", + }, + { + sig: "unsubscribe(p, ch)", + pre: "p.link = Ready", + eff: "p.subscriptions ← p.subscriptions ∖ {ch}", + }, + { + sig: "read/write(p, ch)", + pre: "p.link = Ready; ch ∈ p.characteristics", + eff: "one-shot GATT op; no link/subscription change", + }, + ], + invariants: [ + "p.subscriptions ⊆ p.characteristics — cannot subscribe to a characteristic that was never discovered", + "reads/writes are permitted only against a Ready peripheral's discovered characteristics", + ], + failures: [ + "Encryption mismatch — an encrypted characteristic is accessed without a completed bond; the op fails with a GATT insufficient-authentication error until pairing completes", + ], + perf: [ + "Notification latency — subscribed-characteristic updates delivered within the negotiated connection interval (7.5 ms – 4 s)", + "MTU negotiation — completed before the first large read/write, or payloads truncate to the 23-byte default", + ], + notes: [ + "read/write/subscribe leave the link in Ready — a self-loop. They are the recurring work of a connected session.", + ], + }, + { + id: "validate", + name: "Validate", + fig: "07", + caps: ["BLE"], + verb: "Treat every peripheral payload as untrusted attacker-controllable input; bounds-check before parsing and never forward raw device identity.", + state: [["peripheral.characteristics", "set Characteristic"]], + behaviors: [], + invariants: [ + "the peripheral is an untrusted external device — its payloads are validated on receipt, never parsed as trusted", + "raw MAC, unparsed characteristic bytes, and the peripheral display name never cross to the app's own backend — only derived, validated domain values do", + ], + failures: [ + "Untrusted payload — a malformed characteristic value from a rogue or buggy peripheral crashes or overflows the parser unless its length is validated on receipt", + ], + perf: [], + notes: [ + "Telemetry defence in depth: peripheral name (PII), raw MAC (a tracking vector), and characteristic values (health/biometric data) must never appear in analytics events — only coarse counters and standard-service UUIDs.", + ], + }, + ], + + coreInvariants: [ + "scan = Scanning ⟹ permission.status = Granted ∧ adapter = PoweredOn — scanning requires both consent and a live radio (two independent gates)", + "adapter = PoweredOff ⟹ scan = ScanIdle ∧ every discovered peripheral is Disconnected — a dead radio is fully dormant", + "some p.characteristics ⟹ p.link = Ready — GATT characteristic handles exist only after service discovery completes", + "p.subscriptions ⊆ p.characteristics — cannot subscribe to a characteristic that was never discovered", + "p.link = Disconnected ⟹ no p.characteristics ∧ no p.subscriptions — a dropped link invalidates every cached handle and subscription", + ], + + composition: { + caps: [ + { id: "core", label: "Central", sub: "adapter, scan, discovered", core: true }, + { id: "permission", label: "Permission", sub: "status (consent)" }, + { id: "peripheral", label: "Peripheral", sub: "link, characteristics" }, + { id: "gatt", label: "Characteristic", sub: "GATT value handle" }, + ], + funcs: ["Permission", "Power", "Scan", "Connect", "Discover", "Exchange", "Validate"], + links: [ + ["permission", "Permission"], + ["core", "Permission"], + ["core", "Power"], + ["core", "Scan"], + ["permission", "Scan"], + ["peripheral", "Scan"], + ["core", "Connect"], + ["peripheral", "Connect"], + ["peripheral", "Discover"], + ["gatt", "Discover"], + ["peripheral", "Exchange"], + ["gatt", "Exchange"], + ["core", "Validate"], + ["gatt", "Validate"], + ], + }, + + stateMachines: [BLE_ADAPTER_MACHINE, BLE_LINK_MACHINE], + + related: [ + { name: "Permission", relation: "composes · gates startScan" }, + { name: "Geolocation", relation: "sibling · permission-gated" }, + { name: "PushNotification", relation: "sibling · permission-gated" }, + ], +} diff --git a/src/data/blueprint.ts b/src/data/blueprint.ts index 2ca49f0..833104d 100644 --- a/src/data/blueprint.ts +++ b/src/data/blueprint.ts @@ -78,6 +78,17 @@ export type SmKind = | "signout" | "reset" | "unlock" + // BLE adapter + scan lifecycle (central) + | "powerOn" + | "powerOff" + | "startScan" + | "stopScan" + | "discover" + // BLE per-peripheral link lifecycle + | "connect" + | "discoverServices" + | "exchange" + | "disconnect" export interface SmEdge { from: string @@ -119,6 +130,17 @@ export const SM_COLORS: Record = { signout: "#b79cff", reset: "#67d0c0", unlock: "#4fb3a6", + // BLE adapter+scan: green power-on / magenta power-off / blue scan / purple stop / teal discover + powerOn: "#7fdca0", + powerOff: "#ff5c8a", + startScan: "#8fd0ff", + stopScan: "#b79cff", + discover: "#67d0c0", + // BLE link: blue connect / amber service-discovery / teal exchange / magenta drop + connect: "#8fd0ff", + discoverServices: "#ffb84d", + exchange: "#67d0c0", + disconnect: "#ff5c8a", init: "#4f7099", } diff --git a/src/data/blueprints.ts b/src/data/blueprints.ts index 11e6d71..0567ac6 100644 --- a/src/data/blueprints.ts +++ b/src/data/blueprints.ts @@ -9,11 +9,13 @@ import { grid } from "./gridBlueprint" import { calendar } from "./calendarBlueprint" import { rememberMe } from "./rememberMeBlueprint" import { passwordAuth } from "./passwordAuthBlueprint" +import { ble } from "./bleBlueprint" import ListSpecimen from "@/specimens/ListSpecimen.vue" import GridSpecimen from "@/specimens/GridSpecimen.vue" import CalendarSpecimen from "@/specimens/CalendarSpecimen.vue" import RememberMeSpecimen from "@/specimens/RememberMeSpecimen.vue" import PasswordAuthSpecimen from "@/specimens/PasswordAuthSpecimen.vue" +import BleSpecimen from "@/specimens/BleSpecimen.vue" export interface RegistryEntry { blueprint: Blueprint @@ -24,6 +26,7 @@ export const REGISTRY: Record = { list: { blueprint: list, specimen: ListSpecimen }, grid: { blueprint: grid, specimen: GridSpecimen }, calendar: { blueprint: calendar, specimen: CalendarSpecimen }, + ble: { blueprint: ble, specimen: BleSpecimen }, "password-auth": { blueprint: passwordAuth, specimen: PasswordAuthSpecimen }, "remember-me": { blueprint: rememberMe, specimen: RememberMeSpecimen }, } diff --git a/src/specimens/BleSpecimen.vue b/src/specimens/BleSpecimen.vue new file mode 100644 index 0000000..6382480 --- /dev/null +++ b/src/specimens/BleSpecimen.vue @@ -0,0 +1,481 @@ + + + + +