Skip to content

ROADMAP.adoc

Latest commit

 

History

History
72 lines (65 loc) · 3.41 KB

ROADMAP.adoc

File metadata and controls

72 lines (65 loc) · 3.41 KB

Lustreiser Roadmap

Table of Contents

Phase 0: Scaffold (COMPLETE)

  • ✓ RSR template with full CI/CD (17 workflows)

  • ✓ CLI with subcommands (init, validate, generate, build, run, info)

  • ✓ Manifest parser (lustreiser.toml)

  • ✓ Codegen stubs

  • ✓ Idris2 ABI module stubs

  • ✓ Zig FFI bridge stubs

  • ✓ README with Lustre-specific architecture

Phase 1: Control Flow Analysis

  • ❏ Parse manifest to extract dataflow topology

  • ❏ Build directed acyclic graph (DAG) of node dependencies

  • ❏ Identify input/output streams and their types

  • ❏ Detect feedback loops requiring pre/fby operators

  • ❏ Validate that the dataflow graph is acyclic (modulo pre)

  • ❏ Extract timing requirements from manifest declarations

  • ❏ Map user-declared I/O to Lustre node ports

Phase 2: Lustre Node Generation

  • ❏ Generate .lus files from the analysed dataflow graph

  • ❏ Emit correct node declarations with typed input/output streams

  • ❏ Insert pre and fby temporal operators for stateful streams

  • ❏ Generate → (followed-by) for stream initialisation

  • ❏ Produce combinational nodes (no state) for pure transformations

  • ❏ Support nested node instantiation (hierarchical composition)

  • ❏ Generate assertion nodes for runtime monitoring (assert)

Phase 3: Clock Calculus

  • ❏ Assign base clock to top-level nodes

  • ❏ Implement when operator for clock downsampling

  • ❏ Implement merge operator for clock recombination

  • ❏ Type-check clock expressions (every stream has exactly one clock)

  • ❏ Support multi-rate systems (sensors at different frequencies)

  • ❏ Generate clock annotations in Lustre output

  • ❏ Verify clock consistency across node boundaries

Phase 4: WCET Analysis and Timing Proofs

  • ❏ Integrate worst-case execution time (WCET) analysis

  • ❏ Model generated C code paths for timing bounds

  • ❏ Prove in Idris2 that WCET fits within declared clock period

  • ❏ Detect unbounded constructs (recursion, dynamic allocation) and reject them

  • ❏ Generate timing certificates for each node

  • ❏ Support multiple clock domains with independent WCET budgets

  • ❏ Produce machine-readable timing reports (for DO-178C evidence)

Phase 5: Idris2 Timing Proofs (ABI Layer)

  • ❏ Define LustreNode type with timing metadata

  • ❏ Define Clock type with period and phase

  • ❏ Define DataflowStream with element type and clock

  • ❏ Define TemporalOperator (Pre, Fby, When, Merge) with clock proofs

  • ❏ Define WCET bounded-time type with formal deadline proofs

  • ❏ Prove that node composition preserves timing bounds

  • ❏ Prove that clock calculus transformations are sound

  • ❏ Prove stream buffer layouts fit in static memory

  • ❏ Generate C headers from verified ABI definitions

Phase 6: Ecosystem Integration

  • ❏ SCADE interop — import/export .lus files compatible with SCADE Suite

  • ❏ Kind2 model checker integration for property verification

  • ❏ Lv6 compiler backend for reference compilation

  • ❏ PanLL panel for interactive dataflow visualisation

  • ❏ BoJ-server cartridge for Lustre generation as a service

  • ❏ VeriSimDB backing store for timing analysis results

  • ❏ Integration tests with real embedded targets (ARM Cortex-M, RISC-V)

  • ❏ Examples: flight controller, PID loop, watchdog timer, sensor fusion

  • ❏ Publish to crates.io