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.