资料下载
×
基于Event-B的航天器内存管理系统
消耗积分:2 |
格式:rar |
大小:2.33 MB |
2017-12-29
分享资料个
内存管理系统位于操作系统内核的最底层，为上层提供内存分配和回收机制．在航天器这类安全攸关的关键系统中，其可靠性和安全性至关重要，必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束，因此，系统通常采用较为复杂的数据结构和算法来管理内存空间，同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性．对复杂内存管理系统的形式化验证也会比之前的验证工作带来更多难题，主要体现在：内存管理模块中的复杂数据结构的形式化描述，操作的规范语义，行为的建模，内部函数的规范及断言定义与循环不变式的定义，实时性验证等方面．针对这些问题，深入分析实际的航天器操作系统内存管理系统的特性：探索基于分层迭代的语义描述与验证的一般性方法与理论，并应用这些理论方法来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统．该研究成果有望直接应用于我国新一代的航天器系统．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
