Project Overview
Mission Statement
Automating the generation of visual diagrams from formal specifications to bridge the gap between formal verification and stakeholder communication at SanDisk Corporation.
The Challenge
SanDisk has launched an initiative to write designs using TLA+ (Temporal Logic of Actions) for formal verification. However, design artifacts need to be shared between teams who are more comfortable with visual formats like flowcharts and UML diagrams rather than pseudo code.
Our Solution
We're developing an automated pipeline that:
- Takes PlusCal pseudo code as input
- Generates PlantUML sequence and activity diagrams
- Produces locked PDFs only when the PlusCal passes model-checking
- Ensures synchronization between PlusCal and PlantUML contexts
Impact
This breakthrough will benefit SanDisk in three important ways:
- Time Reduction: Significantly reduce time required to create formally verified visual figures
- Adoption Encouragement: Help firmware engineers adopt PlusCal as a stepping-stone to TLA+
- Culture Change: Foster a culture of formal methods adoption within SanDisk's design process
