Name
Abstract | ||
|---|---|---|
Periodic real-time programs are ubiquitous: they control robots, radars, medical equipment, etc. They consist of a set of tasks, each of which executes (in a separate thread) a specific job, periodically. A common synchronization mechanism for such programs is via Priority Inheritance Protocol (PIP) locks. PIP locks have low programming overhead, but cause deadlocks if used incorrectly. We address the problem of verifying safety and deadlock freedom of such programs. Our approach is based on sequentialization - converting the periodic program to an equivalent (non-deterministic) sequential program, and verifying it with a model checker. Our algorithm, called pipVerif, is iterative and optimal - it terminates after sequentializing with the smallest number of rounds required to either find a counterexample, or prove the program safe and deadlock-free. We implemented pipVerif and validated it on a number of examples derived from a robot controller. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/FMCAD.2013.6679402 | Formal Methods in Computer-Aided Design |
Keywords | Field | DocType |
iterative methods,program verification,protocols,safety-critical software,synchronisation,PIP locks,PIPVERIF,deadlock freedom,equivalent sequential program,iterative algorithm,model checker,nondeterministic sequential program,optimal algorithm,periodic real-time program verification,priority inheritance protocol locks,programming overhead,safety verification,sequentialization,synchronization mechanism | Synchronization,Programming language,Model checking,Computer science,Iterative method,Deadlock,Theoretical computer science,Thread (computing),Real-time computing,Priority inheritance,Counterexample,Robot | Conference |
Citations | PageRank | References |
3 | 0.38 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sagar Chaki | 1 | 687 | 41.58 |
| Arie Gurfinkel | 2 | 939 | 55.15 |
| Ofer Strichman | 3 | 1071 | 63.61 |