小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
10期
2261-2266
,共6页
钱振江%唐洪英%李康杰%黄皓%宋方敏
錢振江%唐洪英%李康傑%黃皓%宋方敏
전진강%당홍영%리강걸%황호%송방민
文件系统%微内核架构%形式化设计%形式化验证%正确性断言%Isabelle/HOL
文件繫統%微內覈架構%形式化設計%形式化驗證%正確性斷言%Isabelle/HOL
문건계통%미내핵가구%형식화설계%형식화험증%정학성단언%Isabelle/HOL
file system%microkernel architecture%formal design%formal verification%correctness assertion%Isabelle/HOL
文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语义和系统状态转换,分析和归纳文件系统的功能正确性断言.以实现的微内核安全操作系统(Verified Trusted Oper-ating System,VTOS)为例,阐述在Isabelle/HOL定理证明器环境中构建状态自动机模型的方法,并对VTOS文件系统的形式化设计和功能正确性断言进行一致性验证,结果显示,VTOS文件系统的设计和实现符合预期的正确性规格说明.
文件繫統作為數據存儲和管理的功能模塊,其正確性是操作繫統安全性的重要方麵.採用形式化方法對微內覈架構文件繫統進行設計,使用操作繫統對象語義模型(OSOSM)框架提齣微內覈架構文件繫統的狀態自動機模型,併依此描述繫統調用的功能語義和繫統狀態轉換,分析和歸納文件繫統的功能正確性斷言.以實現的微內覈安全操作繫統(Verified Trusted Oper-ating System,VTOS)為例,闡述在Isabelle/HOL定理證明器環境中構建狀態自動機模型的方法,併對VTOS文件繫統的形式化設計和功能正確性斷言進行一緻性驗證,結果顯示,VTOS文件繫統的設計和實現符閤預期的正確性規格說明.
문건계통작위수거존저화관리적공능모괴,기정학성시조작계통안전성적중요방면.채용형식화방법대미내핵가구문건계통진행설계,사용조작계통대상어의모형(OSOSM)광가제출미내핵가구문건계통적상태자동궤모형,병의차묘술계통조용적공능어의화계통상태전환,분석화귀납문건계통적공능정학성단언.이실현적미내핵안전조작계통(Verified Trusted Oper-ating System,VTOS)위례,천술재Isabelle/HOL정리증명기배경중구건상태자동궤모형적방법,병대VTOS문건계통적형식화설계화공능정학성단언진행일치성험증,결과현시,VTOS문건계통적설계화실현부합예기적정학성규격설명.
