Integration verification across software and hardware for a simple embedded system

Citations Over TimeTop 10% of 2021 papers

Abstract

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.

Related Papers

• → A kripke logical relation between ML and assembly(2011)60 cited
• → Formal specification and verification of a broadcasting protocol: a refinement-based approach(2020)1 cited
• → Construction of Verified Compiler Front-Ends with Program-Checking(2000)16 cited
• → Calculating Certified Compilers for Non-deterministic Languages(2015)1 cited
• → Formally Verifying a Compiler: What Does It Mean, Exactly? (Invited Talk)(2016)