计算机科学
計算機科學
계산궤과학
Computer Science
2015年
8期
203-214
,共12页
嵌入式操作系统%形式化验证%建模%Isabelle/HOL%VCC
嵌入式操作繫統%形式化驗證%建模%Isabelle/HOL%VCC
감입식조작계통%형식화험증%건모%Isabelle/HOL%VCC
Embedded operating system%Formal verification%Modeling%Isabelle/HOL%VCC
描述了一个汽车电子嵌入式实时操作系统的分层形式模型:在低层,该操作系统的顺序内核承担基础设施的角色,实施任务、ISR和系统服务等并发执行体之间的切换;而在高层,该操作系统向用户提供可并发执行的系统服务.两个层次的模型具有不同的配置状态视图和操作粒度.作为最重要的安全相关特性,应用与OS之间的存储隔离保护机制在顺序内核的模型中得以体现.建立了操作系统的实现正确性定理,包括相应的仿真关系和实现不变量.根据该操作系统两个部分模型的特点及相应代码的实现语言情况,选择组合应用定理证明器Isabelle/HOL和程序验证工具VCC的方式,有效完成了该操作系统的形式化验证.
描述瞭一箇汽車電子嵌入式實時操作繫統的分層形式模型:在低層,該操作繫統的順序內覈承擔基礎設施的角色,實施任務、ISR和繫統服務等併髮執行體之間的切換;而在高層,該操作繫統嚮用戶提供可併髮執行的繫統服務.兩箇層次的模型具有不同的配置狀態視圖和操作粒度.作為最重要的安全相關特性,應用與OS之間的存儲隔離保護機製在順序內覈的模型中得以體現.建立瞭操作繫統的實現正確性定理,包括相應的倣真關繫和實現不變量.根據該操作繫統兩箇部分模型的特點及相應代碼的實現語言情況,選擇組閤應用定理證明器Isabelle/HOL和程序驗證工具VCC的方式,有效完成瞭該操作繫統的形式化驗證.
묘술료일개기차전자감입식실시조작계통적분층형식모형:재저층,해조작계통적순서내핵승담기출설시적각색,실시임무、ISR화계통복무등병발집행체지간적절환;이재고층,해조작계통향용호제공가병발집행적계통복무.량개층차적모형구유불동적배치상태시도화조작립도.작위최중요적안전상관특성,응용여OS지간적존저격리보호궤제재순서내핵적모형중득이체현.건립료조작계통적실현정학성정리,포괄상응적방진관계화실현불변량.근거해조작계통량개부분모형적특점급상응대마적실현어언정황,선택조합응용정리증명기Isabelle/HOL화정서험증공구VCC적방식,유효완성료해조작계통적형식화험증.
