L4虚拟内存子系统的形式化验证

摘要： 第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制,聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型,该模型涉及映射机制所有操作、地址空间所有管理操作... （共22页）