摘要：在分析安全关键软件防危性测评的必要性基础上,提出了适合于评估关键软件防危性的评估指标,给出了防危性评估指标与可靠性评估指标之间的关系。总结了4种传统测评方法评估高防危性需求软件的局限性。研究了基于重要性采样及压力测试技术测评高防危性软件的可行性,并详细讨论了其具体实施过程,其间结合核电安全关键控制系统进行了例证。最后就该领域内的相关工作及发展方向进行了展望。

摘要：首先将软件的UML状态机模型转换为模型检测工具MOCHA的输入语言REACTIVEMODULES,在MOCHA中进行正确性验证,利用模型检测工具针对错误情况给出的反例路径,尽早修改软件的UML设计模型;然后将已验证过的UML模型转换为定理证明工具B方法的抽象规约,利用B方法的精化、验证及代码生成功能,直接生成正确的C代码。并给出了从UML状态机到REACTIVE MODULES建模语言及B AMN抽象规约的转换规则。实验结果表明,该方法可在软件工程中有效地提高高可信嵌入式软件开发和验证的效率。

摘要：设计并实现一个类C语言PointerC的出具证明编译器后端。该后端采用最强后条件演算同步处理整型断言和指针断言实现整型验证条件和指针验证条件的证明,能够完全自动地产生目标级程序的指针安全性证明,处理常见递归数据结构中的非一致性别名问题。后端包括独立的定理检查器,能够检验携证明代码的完整性。

摘要：形式化方法是指有严格数学基础的软件和系统开发方法，可支持计算机系统及软件的规约、设计、验证与演化等活动。随着高可信软件的兴起，形式化方法的关注度日益提高。其作用不仅体现在人们对计算系统规律认识的深入，更体现在对计算系统开发、运行和演化的工具与平台构建的基础性支持。近年来，形式化方法也在向生物科学、物理科学等领域交叉渗透。

摘要：形式化方法是指有严格数学基础的软件和系统开发方法，可支持计算机系统及软件的规约、设计、验证与演化等活动。随着高可信软件的兴起，形式化方法的关注度日益提高。其作用不仅体现在人们对计算系统规律认识的深入，更体现在对计算系统开发、运行和演化的工具与平台构建的基础性支持。近年来，形式化方法也在向生物科学、物理科学等领域交叉渗透。