Proposed solution

Our solution connects TLA+ modeling, trace generation, Rust orchestration, and NVMe command execution into a single practical workflow for repeatable device validation.

Overview

We are building a command line toolchain that reads specification traces and executes matching NVMe command sequences on a device under test. It captures logs and artifacts so results can be analyzed and replayed.

Selling our Product

Implementation details

• Trace parser converts specification output into structured steps.
• Executor maps steps to NVMe commands and handles configuration.
• Result packager keeps logs and metadata for each run.

Technologies

• TLA+ and PlusCal. We use TLA+ to model valid device behaviors and constraints, with PlusCal where algorithmic notation helps. The specifications become the single source of truth that test sequences must respect. This enables specification-centric testing rather than hand-written test scripts.
• TLC model checker in simulate mode. Instead of PlusPy, we rely on TLC to explore non-deterministic choices and produce concrete traces. TLC’s simulate mode gives broader coverage, avoids illegal sequences that cause noise, and improves repeatability since each run records the seed and choices.
• Rust executor bound to NVMe-CLI. The runtime is a Rust tool that reads TLC traces and issues the corresponding NVMe commands. Rust provides safety and performance for low-level operations, and a strong CLI experience for consistent, scripted runs.
• NVMe-CLI. We use the standard NVMe command line utility to interact with the SSD under test. Mapping trace steps to NVMe-CLI keeps the execution path transparent and easy to audit, and it makes replay straightforward on any configured test system.
• Instrumentation convention. We define a repeatable way to instrument TLA+ specifications so conceptual states map to the physical states of the NVMe device and test host. This convention is what links the model to real commands and ensures that observed outcomes can be reasoned about in the spec.
• Development environment in VS Code. The team uses VS Code as the IDE. Required extensions include Rust-Analyzer, TLA+, Graphviz Preview, Live Share, and a PDF viewer. This set supports spec editing, trace visualization, collaborative reviews, and code navigation in one place.
• OpenJDK 11 or newer. TLC runs on the JVM. Using OpenJDK ensures a consistent and open Java runtime for model checking across developer machines and lab hosts.
• Ubuntu test environment. Development and execution target a current Ubuntu distribution. This standardizes the shell, package manager, and NVMe-CLI availability across systems.
• NVMe PCIe SSD device under test. A secondary NVMe SSD is required for exercising commands safely without impacting the system drive. Hardware access is controlled and documented as part of the run configuration.
• Git and GitHub during development, ZIP for archival. Day-to-day work uses Git with a private remote for collaboration. For long-term archival on the course server, we export a complete ZIP of the final code and documentation so the site does not depend on an external repository.