Modular Verification of Hybrid System Code with VCC
This work addresses verification challenges for hybrid systems in safety-critical domains, representing an incremental improvement by adapting existing deductive verification tools.
The authors tackled the problem of verifying hybrid system code by developing an object-modular reasoning methodology using VCC, which includes defining an explicit time model and timed objects like Timers and Deadlines to ensure safety properties, with results demonstrating that all Deadlines are eventually destroyed to prevent deadlocks.
We present a methodology for object-modular reasoning about hybrid system code using VCC, a deductive verifier for concurrent C code. We define in VCC an explicit time model, in which the passage of time must respect the invariants of certain timed objects. Fields that change automatically with changes to time are then defined as volatile fields with suitable invariants. We also define two types of timed objects that prevent time from advancing past a given expiration: Timers (which represent assumptions about the upper limit on the time it takes to do something) and Deadlines (which represent assertions about these limits). The difference between the two is that once the expiration time of a Deadline is reached, the Deadline and time itself are permanently deadlocked. Our methodology includes showing that all Deadlines are eventually destroyed, proving that they do not interfere with the flow of time.