Modular Verification of Hybrid System Code with VCC

TL;DR

This paper introduces a modular verification methodology for hybrid system code using VCC, incorporating explicit time models, timers, and deadlines to reason about time-dependent behaviors in concurrent C programs.

Contribution

It defines a novel approach to object-modular reasoning about hybrid systems in VCC by modeling time explicitly and managing timed objects through timers and deadlines.

Findings

Successfully models explicit time in VCC for hybrid systems

Ensures deadlines are eventually destroyed to prevent interference with time flow

Provides a framework for verifying time-dependent properties in concurrent C code

Abstract

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.