Thesis Topic Details
Topic ID: |
3080 | |
Title: |
A Foundational model of the ARM11 Memory Management Unit | |
Supervisor: |
Gerwin Klein | |
Research Area: |
Formal Methods, Operating Systems | |
| Associated Staff | ||
|---|---|---|
Assessor: |
June Andronick | |
| Topic Details | ||
Status: |
Active | |
Type: |
Research | |
Programs: |
CS CE BIOM SE | |
Group Suitable: |
No | |
Industrial: |
No | |
Pre-requisites: |
-- | |
Description: |
The aim of this topic is a fully formal description of the ARM11 MMU in Isabelle/HOL. The model should include memory translation and access control, the page table format, the TLB, instruction and data fetch, and optionally caches. The longer-term purpose of this model is to use it as a foundational basis for proving the absence of page faults and the correct placement of TLB and cache flush operations in the seL4 microkernel. | |
Comments: |
This topic requires previous knowledge of Isabelle/HOL and the ARM11 hardware architecture. | |
| Past Student Reports | ||
| No Reports Available. Contact the supervisor for more information.
Check out all available reports in the CSE Thesis Report Library. NOTE: only current CSE students can login to view and select reports to download. |
||