操作系统是整个计算机系统的核心与基石,其可靠性与安全性至关重要.操作系统的故障或漏洞可能会导致系统崩溃、数据丢失、隐私泄露和安全攻击等问题,特别是在安全攸关系统中,一旦操作系统发生错误,就可能会造成重大人员伤亡或财产损失....操作系统是整个计算机系统的核心与基石,其可靠性与安全性至关重要.操作系统的故障或漏洞可能会导致系统崩溃、数据丢失、隐私泄露和安全攻击等问题,特别是在安全攸关系统中,一旦操作系统发生错误,就可能会造成重大人员伤亡或财产损失.一直以来,如何保障操作系统的安全性和可靠性对学术界和工业界都是一个重大挑战.目前验证操作系统安全性的方法有软件测试、程序静态分析、形式化方法等.其中,形式化方法是最有潜力确保操作系统安全可信的方法,通过使用形式化方法,建立数学模型并进行系统的形式化分析和验证,从而发现潜在的错误和漏洞.在操作系统中,形式化方法可以用于验证操作系统的功能正确性、完整性以及系统安全性等.在已有的针对操作系统形式化验证的成果基础上,提出了一个面向嵌入式操作系统的形式化验证方案,采用VCC(verified C compiler)、CBMC(C bounded model checker)以及PAT(process analysis toolkit)工具分别对操作系统单元层面、模块层面和系统层面进行验证.该方法已成功应用到某操作系统的任务调度架构案例中,对于嵌入式操作系统的分析验证具有一定的通用性。展开更多
传统的基于文档的系统工程(Text-Based Systems Engineering,TSE)方法在动车组系统设计中存在需求与设计表达不一致、可追溯性差、系统重用性不足、多学科集成困难等问题,引入基于模型的系统工程(Model-Based Systems Engineering,MBSE...传统的基于文档的系统工程(Text-Based Systems Engineering,TSE)方法在动车组系统设计中存在需求与设计表达不一致、可追溯性差、系统重用性不足、多学科集成困难等问题,引入基于模型的系统工程(Model-Based Systems Engineering,MBSE)方法,提出了一种适用于动车组的基于MBSE的联合仿真设计方法。该方法中涵盖对系统需求、功能、行为、物理的分析建模,同时利用这种SysML模型建立Simulink模型并驱动,通过将这2个模型相融合,可以验证系统是否满足性能需求。以动车组车门系统为例,使用基于MBSE的联合仿真方法,验证开门场景的性能。证明了该方法可以减少传统的试错成本,在系统设计早期,提高系统的准确性和可靠性。展开更多
文摘操作系统是整个计算机系统的核心与基石,其可靠性与安全性至关重要.操作系统的故障或漏洞可能会导致系统崩溃、数据丢失、隐私泄露和安全攻击等问题,特别是在安全攸关系统中,一旦操作系统发生错误,就可能会造成重大人员伤亡或财产损失.一直以来,如何保障操作系统的安全性和可靠性对学术界和工业界都是一个重大挑战.目前验证操作系统安全性的方法有软件测试、程序静态分析、形式化方法等.其中,形式化方法是最有潜力确保操作系统安全可信的方法,通过使用形式化方法,建立数学模型并进行系统的形式化分析和验证,从而发现潜在的错误和漏洞.在操作系统中,形式化方法可以用于验证操作系统的功能正确性、完整性以及系统安全性等.在已有的针对操作系统形式化验证的成果基础上,提出了一个面向嵌入式操作系统的形式化验证方案,采用VCC(verified C compiler)、CBMC(C bounded model checker)以及PAT(process analysis toolkit)工具分别对操作系统单元层面、模块层面和系统层面进行验证.该方法已成功应用到某操作系统的任务调度架构案例中,对于嵌入式操作系统的分析验证具有一定的通用性。
文摘传统的基于文档的系统工程(Text-Based Systems Engineering,TSE)方法在动车组系统设计中存在需求与设计表达不一致、可追溯性差、系统重用性不足、多学科集成困难等问题,引入基于模型的系统工程(Model-Based Systems Engineering,MBSE)方法,提出了一种适用于动车组的基于MBSE的联合仿真设计方法。该方法中涵盖对系统需求、功能、行为、物理的分析建模,同时利用这种SysML模型建立Simulink模型并驱动,通过将这2个模型相融合,可以验证系统是否满足性能需求。以动车组车门系统为例,使用基于MBSE的联合仿真方法,验证开门场景的性能。证明了该方法可以减少传统的试错成本,在系统设计早期,提高系统的准确性和可靠性。
