Project Overview
SanDisk develops high-performance storage firmware that must undergo rigorous regression testing before release. As firmware systems increase in complexity, manually creating and maintaining regression test sequences becomes time-consuming, difficult to scale, and prone to incomplete coverage. This creates bottlenecks in the development cycle and increases the risk of subtle defects escaping into production.
MidGARD is the automated solution our team is designing to address this problem. The system will generate regression test sequences directly from formal TLA+ specifications. By leveraging the TLC model checker to explore valid system behaviors, MidGARD will transform formally verified state spaces into structured, reproducible, and high-coverage test suites. Rather than relying on manually written test flows, engineers will be able to derive tests systematically from formal models.
The initial concept for this project was provided by our sponsor in the form of a Capstone project proposal. MidGARD represents our refined system design developed in collaboration with the sponsor.
Technologies
MidGARD is built using a focused set of tools chosen for their reliability, performance, and support for formal modeling and graph‑based analysis. Each technology plays a specific role in enabling automated test generation from TLA+ specifications.
TLA+ Formal Specification Language
We use TLA+ to formally describe system behavior in a mathematically precise way, ensuring that all generated tests originate from verified system logic. The VSCode TLA+ extension supports authoring, validating, and maintaining these specifications throughout development.
Rust Programming Language
Rust powers the MidGARD toolchain, giving us memory‑safe performance for graph processing and deterministic test generation. Cargo and the petgraph crate allow us to build a modular, efficient pipeline capable of handling large state spaces.
TLC Model Checker (OpenJDK ≥ 11.0.6)
TLC explores all valid behaviors of a TLA+ specification and produces the raw state graph that MidGARD analyzes. We run TLC using OpenJDK to ensure compatibility, reproducibility, and freedom from Oracle licensing restrictions.
Graphviz & DOT Visualization
Graphviz generates the DOT graphs that represent system state transitions, which we then clean and analyze inside MidGARD. The Graphviz Interactive Preview extension helps us inspect and validate graph structure during development.
Visual Studio Code & Extensions
VSCode is our primary development environment, supported by Rust‑Analyzer, TLA+, Graphviz Preview, and Live Share. These tools streamline collaboration, debugging, and consistent development across the team.
Cargo Tooling & Rust Ecosystem
We rely on Cargo extensions and Rust’s ecosystem to manage dependencies, run tests, and support graph‑analysis workflows. This tooling keeps the codebase maintainable and ready for future extensions.
Documentation & Deliverables
We maintain a professionally written reference manual and a fully documented private GitHub repository. These deliverables ensure SanDisk can adopt, maintain, and extend MidGARD as needed.