Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets
| Autor: | Xiaojie Guo, Pascal Fradet, Jean-François Monin, Sophie Quinton |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
010302 applied physics
Correctness Computational complexity theory Programming language Computer science Proof assistant 02 engineering and technology Work in process computer.software_genre 01 natural sciences 020202 computer hardware & architecture Scheduling (computing) Automated theorem proving TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0103 physical sciences 0202 electrical engineering electronic engineering information engineering Task analysis Microsoft Windows computer |
| Zdroj: | RTSS |
| Popis: | This paper presents the first steps toward a formally proven tool for schedulability analysis of tasks with offsets. We formalize and verify the seminal response time analysis of Tindell by extending the Prosa proof library, which is based on the Coq proof assistant. Thanks to Coq’s extraction capabilities, this will allow us to easily obtain a certified analyzer. Additionally, we want to build a Coq certifier that can verify the correctness of results obtained using related (but uncertified), already existing analyzers. Our objective is to investigate the advantages and drawbacks of both approaches, namely the certified analysis and the certifier. The work described in this paper as well as its continuation is intended to enrich the Prosa library. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|