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.