Coq proofs for the schedulability analysis of tasks with offsets

We have formalized and proven in Coq the approximated analysis technique presented by Tindell to bound the response time of tasks with offsets.

This work has allowed us to:

• underline implicit assumptions made in Tindell’s informal analysis;
• ease the generalization of the verified analysis;
• generate a certifier and an analyzer.

Links

• The Work-in-Progress paper “Toward a Coq-certified Tool for the Schedulability Analysis of Tasks with Offsets” to appear at RTSS’17 can be found here.
• The proofs can be found here.