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 generates regression test sequences directly from formal TLA+ specifications. By leveraging the TLC Model Checker to explore valid system behaviors, MidGARD transforms model-checking output into structured, reproducible test sequences that can support more consistent regression testing. Rather than relying only on manually written test flows, engineers can use MidGARD 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.
