基于时序逻辑的Open Solaris内核进程形式化描述与求精

摘要

XYZ系统理论基于Manna-Pnueli线性时序逻辑，其中时序逻辑语言XYZ/E既是一个时序逻辑系统，又可作为可执行程序的不同抽象层次的系统描述。作为验证软件可靠性和生产软件工具引擎，具有重要理论价值和实践意义。 形式化分析操作系统内核进程通常是基于专用操作系统，这将导致开发和维护的难度都很大。而对通用操作系统内核进程进行形式化分析，由于没有充分开放的授权，给实际应用带来专利壁垒。Open Solarls是Sun公司开发的一个多任务、多用户操作系统，具有高度实时性、最佳利用率、高可用性、高性能、极高安全性及平台选择多样性。其基于CDDL(通用开发和发布许可)开放标准，给研究操作系统和工业应用带来一次契机。 本文阐述了Open Solaris内核进程机制与现行的Sun Solaris业界开放标准(CDDL)，基于XYZ/E语言描述了多任务操作系统内核进程机制，使用Sun DTrace工具细化分析了内核进程数据结构、内核进程的创建、系统调度，采用动态取值分析内核进程编程思想；结合软件设计模式给出内核进程结构流程图，描述了内核进程体系结构。论文重点分析了内核进程数据结构、内核进程创建、系统调用等过程以及时钟概念，并对其进行XYZ/AE的描述和XYZ/EE编程。最后，给出了内核进程规范；实现多任务、多用户操作系统内核进程的描述；对内核进程进行了逐步求精与初步验证工作。

目录

文摘

英文文摘

声明

第一章绪论

1.1形式化方法概述

1.2 Open Solaris概述

1.2.1开源的Open Solaris系统

1.2.2 UNIX与Open Solaris的对比

1.3国内外研究现状

1.4本文研究意义

1.5本文组织结构

第二章时序逻辑语言XYZ/E的程序语义

2.1 XYZ/E系统概述

2.2 XYZ程序与语言成份的语义

2.2.1 XYZ/E语言算子

2.2.2条件元和单元

2.2.3选择语句与并行语句

2.2.4过程与过程调用

2.2.5通信命令

2.3本章小结

第三章描述Open Solaris操作系统内核进程

3.1 OpenSolaris操作系统内核进程简介

3.1.1进程模型

3.1.2调度与调配器

3.1.3进程间通信

3.1.4进程权限

3.1.5锁机制

3.1.6 Open Solaris的实时性

3.1.7 Open Solaris的关键技术

3.1.8 Open Solaris与Linux2.6比较

3.2内核进程数据结构

3.3描述Open Solaris内核进程要素

3.3.1进程创建

3.3.2描述系统调用

3.3.3时钟

3.3.4 Open Solaris的实时性

3.3.5 Open Solaris内核进程规范

3.4本章小结

第四章Open Solaris内核进程求精与验证

4.1第一层Open Solaris内核进程规范描述

4.2逐步求精到第二层

4.3逐步求精到第三层

4.4逐步求精到第四层

4.5初步验证工作

4.6本章小结

第五章相关工作比较

5.1内核进程形式化分析

5.2与MK++、SZRTOS比较

第六章总结与展望

6.1 工作总结

6.2展望

参考文献

攻读硕士学位期间参加的科研项目和发表(录用)的论文

致谢