Case Study: C-130J Hercules Aircraft
Lockheed Aeronautical Systems Company
Operational Flight Programs
- Process and transfer information
- 200 K lines of source code
Tabular specification of requirements
- straight-forward code specification and proof
Correctness (not safety) verification