期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证 被引量：4

Formal Modeling and Verification of Task-Management Requirement for SpaceOS2 Based on Event-B
下载PDF
导出
摘要 随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法 Event-B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模,依靠不变式来保证模型的正确性,并且在Rodin平台上对模型进行了形式化验证,结果表明模型是正确的. With the development of space technology in China, the software applied in spacecraft becomes more complex and larger in scale. It is necessary to improve the correctness, reliability and security of software to achieve a high level. Among the approaches, the formal method is an important one. A formal method based on Event-B is introduced to describe the requirement for task model of SpaceOS2. The cor- rectness of this model is formally guaranteed via virtual of invariants. The correctness of the model is veri- fied by using the Rodin platform.
作者 谭彦亮 杨桦 乔磊
机构地区 北京控制工程研究所
出处 《空间控制技术与应用》 2014年第4期57-62,共6页 Aerospace Control and Application
基金 国家自然科学基金资助项目(91118007)
关键词 任务管理 形式化模型 形式化验证 Event—B task management formal model formal verification Event-B
分类号 TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献6

  • 1WALKER B J, KEMMERER R A, POPEK L. Specifi- cation and verification of the UCLA Unix security kernel [J]. Communications of the ACM, 1980,23(2):118- 131.
  • 2BEVIER W. A Verified operating system kernel [ D]. Austin: University of Texas, 1987.
  • 3BIRRELL A D,GUTTAG J V, HORNING J J, et al. Synchronisation primitives for a multiprocessor: a formal specification [J]. ACM SIGOPS Operating Systems Re- view, 1987,21 (5) :94-102.
  • 4KLEING, ELPHINSTONE K. SeIA: formal verification of an OS kernel [ C ]//Jeanna Neefe, SOSP' 09 Pro- ceedings of the ACM SIGOPS 22 symposium on Oper- ating Systems Principles. New York: ACM Press, 2009 : 207-220.
  • 5ABRIALJ R. Modeling in Event-B: system and software engineering [ M ]. Cambridge: Cambridge University Press, 2010 : 12-64.
  • 6ABRIALJ R, BUTLER M, HALLERSTEDE S, et al. Rodin:an open toolset for modeling and reasoning in E-vent-B [ J ]. International Journal on Software Tools Technology Transfer, 2010, 12 ( 6 ) : 447-466.

同被引文献37

  • 1JOSEPH M, PANDYA P. Finding response times in a real-time system[J].The Computer Journal, 1986, 29 (5) .- 390-395.
  • 2DAVIS R I, BURNS A. Response time upper bounds for fixed priority real-time systems [ C ]. Real-Time Systems Symposium, Barcelona, Spain, November 30-December 3, 2008.
  • 3MAKI-TURJA J, NOLIN M. Efficient implementation of tight response-times for tasks with offsets [J]. Real-time System, 2008, 40:77 116.
  • 4BRYLOW D, PALSBERG J. Deadline analysis of interrupt-driven software[J]. IEEE Transactions on Soft-ware Engineering, 2004, 30(10): 634-655.
  • 5JONATHAN K, DORSA S, SANJIT A S. Timing analysis of interrupt-driven programs under context bounds[C]. Formal Methods in Computer-Aided Design, Austin, Texas, USA, October 30-November 2, 2011.
  • 6JEFFAY K, STONE D L. Accounting for interrupt handling costs in dynamic priority task systems[C]. Real-Time Symposium, NC, USA, December, 1993.
  • 7BRANDENBURG B B, LEONTYEV H, ANDERSON J M. An overview of interrupt accounting techniques for multiprocessor real-time systems[J].Journal o{ Systems Architecture, 2011, 57: 638-654.
  • 8RANDAL E BRYANT, DAVID R O' HALLARON. Computer systems: a programmer's perspective[M]. 2nd ed. New Jersey: Pearson Prentice Hall, 2011.
  • 9SEBASTIAN A, ROBERT I D, CLAIRE M. Improved cache related preemption delay aware response time analysis for fixed priority pre- emptive systems[J].Real-time System, 2012, 48: 499-526.
  • 10WILHELM R, ENGBLOM J, ERMEDAHL A, et al. The worst-case execution-time problem-overview of methods and survey of tools[J]. ACM Transactions on Embedded Computing Systems, 2008, 7 ( 3 ) : 1- 53.

引证文献4

二级引证文献24

空间控制技术与应用
2014年 第4期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部