Project Details
Background
SanDisk is serious about the quality of their popular storage products and strives to be best-in-class in upholding their global brand. The company has moved toward formal verification using TLA+ to catch subtle bugs that traditional review processes miss.
Technical Requirements
- Parse and analyze PlusCal pseudo code specifications
- Generate PlantUML sequence diagrams from PlusCal algorithms
- Generate PlantUML activity diagrams showing system flow
- Integrate with TLA+ model checker for verification
- Produce locked PDF documents with LaTeX formatting
- Ensure synchronization between PlusCal source and generated diagrams
Deliverables
- Complete and well-commented codebase
- Detailed documentation and reference manual
- GitHub repository with development history
- Professional literature for SanDisk product teams
Academic Significance
This project exposes students to cutting-edge formal methods invented by Leslie Lamport (ACM Turing Award winner), used by major companies like AWS, Microsoft, Oracle, Google, LinkedIn, MongoDB, and others. There's potential for grant funding from the TLA+ Foundation.