Premiers pas › Tutoriel

Premiers pas

Tutoriel : une pompe à eau, du modèle au firmware

Ce tutoriel construit pas à pas un petit système en arche-lang : un contrôleur de pompe, démarré et arrêté depuis un pupitre opérateur, qui pilote un moteur. En chemin, il vérifie le modèle, relie une exigence à la part qui la satisfait et au test qui la vérifie, exécute ce test dans le simulateur, place le contrôleur sur un microcontrôleur, génère son firmware Rust et met l'ensemble du projet en CI.

Chaque bloc arche ci-dessous s'ajoute, dans l'ordre, à un unique fichier, pump.arche, à placer dans un dossier vide. (Le test du tutoriel compile exactement ces blocs : ils reflètent donc le langage tel qu'il est.) Les commandes se lancent depuis ce dossier ; si archec n'est pas dans votre PATH, utilisez node <arche-lang>/dist/cli.js.

Chaque déclaration et chaque propriété sont décrites dans la référence du langage ; les commandes, dans la référence des commandes.

1. Le projet, ses données et ses messages#

project Pump "Water pump" {
  version "0.1"
}

type Flow = float32 unit l/min range 0..120

message START: bool "Start"
message STOP: bool "Stop"
message FLOW_RATE "Flow rate" { rate: Flow }

const MAX_FLOW = 100 unit l/min

Un message porte un nom en majuscules et transporte soit un type — ici un booléen —, soit des champs, comme rate, de type Flow : un nombre doté d'une unité et d'une plage. Les unités s'écrivent telles quelles (l/min, m/s², °C) : archec vérifie que ce que l'on compare ou additionne relève bien de la même grandeur.

archec check pump.arche

2. Les composants et leurs ports#

component Controller "Pump controller" {
  in cmd: can "Commands" receives START, STOP
  out motor: can "Motor" sends FLOW_RATE

  var target: float32 = 0 unit l/min

  fn regulate "Flow loop" {
    wcet 200us
    ```arche
    if state == Running {
      send motor FLOW_RATE { rate: target }
    }
    ```
  }

Un port indique sa direction, son type (can — un type de port, ici le type standard) et les messages qu'il reçoit ou émet. Le corps d'une fonction s'écrit dans le langage d'action, dans un bloc ```arche : state == Running teste l'état de la part, send motor FLOW_RATE { … } émet sur un port, et goto Fault changerait d'état. archec le vérifie — les noms, leurs types, ce qu'émet le port — puis le traduit : en Python, exécuté par le simulateur Arche, et en Rust ou en C pour le firmware (étape 7). wcet donne son coût dans le pire cas, utilisé par l'analyse temporelle de l'étape 6. (Un corps peut toujours être écrit en Python, dans un bloc ```python, pour ce que le langage d'action n'exprime pas : une bibliothèque, une liste.)

3. Une machine à états#

  states {
    state Idle "Stopped"
    state Running "Pumping"
    state Fault
    Idle -> Running on START [self.target <= MAX_FLOW]
    Running -> Idle on STOP
    * -> Fault on dry_run / log('dry run')
  }
}

La machine démarre dans son premier état. on START définit une transition franchie à l'arrivée du message ; […] en est la garde et / … l'action. * -> Fault part de n'importe quel état. Le linter parcourt la machine et signale les états inatteignables, les états sans issue et les déclencheurs qu'aucun port ne reçoit.

Le reste du système :

component Motor "Motor driver" {
  in drive: can "Drive" receives FLOW_RATE
}

component Panel "Operator panel" {
  out buttons: can "Buttons" sends START, STOP
}

system Station "Pumping station" {
  part panel: Panel
  part ctrl: Controller
  part motor: Motor
  panel.buttons -> ctrl.cmd
  ctrl.motor -> motor.drive
}

Un system correspond à un modèle dans Arche : ses parts sont des instances des composants, et a.p -> b.q relie deux ports par un lien. archec vérifie que ce qu'émet une extrémité est bien reçu par l'autre.

archec build pump.arche -o out
arche --project out

out/ est le projet Arche — le YAML que lit l'application Arche.

4. Une exigence, et qui la satisfait#

requirement REQ-START "Start on command" {
  text "The pump shall start within 100 ms of a START command."
  priority high
  method test
}

trace satisfies Station.ctrl -> REQ-START

Le texte d'une exigence est passé au crible pour repérer les formulations invérifiables (« as fast as possible », « TBD »…). trace satisfies indique que le contrôleur la satisfait ; le test de l'étape suivante indique qu'elle est vérifiée.

5. Un test, exécuté dans le simulateur#

test-plan TP-START "Starting" {
  case TC-START-01 "START starts the pump" {
    verifies REQ-START
    at 0ms do ctrl.target = 50.0
    at 10ms do send(panel.buttons, START(True))
    within 100ms expect ctrl.state == "Running"
  }
}

Un cas de test est une chronologie : at tel instant, faire quelque chose ; within tel délai, attendre quelque chose. archec test construit le projet et exécute ses plans de test dans le simulateur Arche (arche-cli) :

archec test pump.arche -o out --coverage

La commande indique quels cas réussissent, quelles exigences ils vérifient, et quelle part des machines à états, des messages et des fonctions les tests ont parcourue.

6. Où il s'exécute#

component Mcu "Pump MCU" {
  kind processor
  cores 1
  hal stm32
  chip "stm32f446re"
  inout can0: can "CAN"
}

system PumpHw "Pump hardware" {
  part mcu: Mcu
  component bus "CAN bus" {
    kind bus
    bitrate 500kbps
  }
  mcu.can0 -> bus
}

deployment Onboard "On the pump" {
  system Station
  platform PumpHw
  binary pump_fw "pump.elf" on mcu {
    thread ctl "Control" { runs ctrl; period 10ms; step regulate; priority 10 }
  }
}

La plateforme est elle aussi un système : des processeurs et des bus. Un deployment y place le système logique sans le modifier : le contrôleur s'exécute sur un thread du MCU, toutes les 10 ms, en appelant regulate.

archec analyze pump.arche

donne la charge de chaque cœur et le temps de réponse de chaque thread au regard de son échéance (ici 200 µs sur 10 ms : 2 %).

7. Le firmware#

archec gen pump.arche --target embassy -o generated

écrit une crate Rust par binaire pour le runtime asynchrone Embassy — generated/embassy/pump_fw/ :

  • src/arche.rs, régénéré à chaque fois : les messages et leur codec CAN, un canal par lien, la machine à états de la part ctrl (CtrlState, CtrlEvent, CtrlMachine::next), son trait de comportement (CtrlBehaviour) et la tâche du thread ctl. À l'arrivée d'un START, la tâche fait avancer la machine avant d'appeler la part. (Les noms viennent de la part, et non de son composant : deux parts d'un même composant donnent deux structs.)
  • src/app.rs, écrit une seule fois puis laissé à votre charge : la struct de la part (Ctrl), avec target à sa valeur initiale et sa machine, la garde à implémenter (guard_target_le_max_flow) et chaque fonction : regulate est déjà en Rust, traduite depuis son corps ```arche (un corps Python serait laissé en commentaire, à porter).
  • src/main.rs, Cargo.toml et .cargo/config.toml pour le STM32F446RE.
cd generated/embassy/pump_fw && cargo build --release

8. En CI#

archec ci pump.arche -o out --coverage-min 50 --junit report.xml

exécute en une seule commande tout ce que vérifie un pipeline — lint, format, timing, TARA, build, les tests et leur couverture —, affiche une ligne par étape de contrôle, écrit un rapport JUnit pour le serveur de CI et renvoie le code 1 si l'une d'elles échoue.

9. Partager des composants : les bibliothèques#

Un composant utilisé par plusieurs projets se range dans une bibliothèque : un dossier contenant un library.arche qui la nomme et en donne la version.

library pump-parts "Pump parts" {
  version "1.2.0"
}

Les versions cohabitent côte à côte : shared/pump-parts@1.2.0/, shared/pump-parts@2.0.0/. Un projet indique où se trouvent les bibliothèques et quelles versions il accepte, puis inclut un fichier de la version retenue :

project Pump "Water pump" {
  libraries "../shared"
  uses pump-parts "^1.2"
}

include "pump-parts/motor.arche"

^1.2 désigne la version 1.2 ou ultérieure, avant la 2.0 — la plus récente disponible, sauf si arche.lock en décide autrement :

archec lib pump.arche          # each library, the version used, the others there are
archec lib pump.arche lock     # arche.lock: the versions and a fingerprint of their files

Une fois verrouillée, la version est conservée jusqu'au prochain verrouillage, et toute bibliothèque dont les fichiers ont changé sous un même numéro de version est signalée.

Pour aller plus loin#

  • patterns.md — chaque déclaration, avec ses propriétés et un exemple.
  • commands.md — chaque commande.
  • Les exemples : examples/physics (des équations, 30 lignes), examples/autonomous-car (une pile complète : exigences, déploiement, plans de test, génération de code), examples/kacao (un vrai projet, 68 fichiers).