科研之友
微信
新浪微博
Facebook
分享链接
摘要
计算机并发性程序形式化验证一直是软件安全领域的难题。软件并发性漏洞难以被发现，一旦发生问题，会造成不可估量的安全问题。形式化验证基于严格的数学推导基础，采用语言、语义、推理证明三位一体方法，构建形式逻辑系统，以确保被验证系统的安全性能。传统的形式化验证方法由于人工参与多、验证工作量大、验证效率低等不足，难以对计算机并发程序进行严谨高效的模型描述与验证。研究了一种可双向转换的并发性程序形式化验证方法，解决了人工抽象建模存在的工作量大且易出错的问题，并且保证了源码层与抽象层验证的一致性，大幅提升了形式化验证的效率。
