Integration verification across software and hardware for a simple embedded system
| Autor: | Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Correctness
Computer science business.industry Interface (computing) Proof assistant 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre Application software 01 natural sciences Instruction set Software 010201 computation theory & mathematics Embedded system 0202 electrical engineering electronic engineering information engineering Compiler business Formal verification computer |
| Zdroj: | PLDI |
| DOI: | 10.1145/3453483.3454065 |
| Popis: | The interfaces between layers of a system are susceptible to bugs if developers of adjacent layers proceed under subtly different assumptions. Formal verification of two layers against the same formal model of the interface between them can be used to shake out these bugs. Doing so for every interface in the system can, in principle, yield unparalleled assurance of the correctness and security of the system as a whole. However, there have been remarkably few efforts that carry out this exercise, and all of them have simplified the task by restricting interactivity of the application, inventing new simplified instruction sets, and using unrealistic input and output mechanisms. We report on the first verification of a realistic embedded system, with its application software, device drivers, compiler, and RISC-V processor represented inside the Coq proof assistant as one mathematical object, with a machine-checked proof of functional correctness. A key challenge is structuring the proof modularly, so that further refinement of the components or expansion of the system can proceed without revisiting the rest of the system. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|