一种基于B方法的形式化开发方法
B方法是目前被广泛应用的一种形式化开发方法,然而B方法在实际的应用中仍然面临着许多的问题.为了能更简单高效的应用形式化方法来开发软件和系统,基于B方法提出了一种新的形式化方法(B*)来对软件和系统进行建模、实现和验证.和B方法一样,B*以离散数学和口计算机语言为基础,使用一阶数理逻辑及集合论开发和验证软件,确保正确性、鲁棒性、一致性以及安全性等,并基于严格的数学理论为软件和硬件系统提供精确的规约、开发和验证方法.提出B*方法的动机是希望能更简单高效的用形式化方法来开发软件和系统,为了达到这个目标B*将数组、链表、树、图等数据结构抽象到集合,并在集合抽象层上对软件进行验证,最后开发自动转换工具,将B*程序转换到C程序,生成可执行代码.
航空电子软件 形式化开发 代码转换 B方法
黄昱 马殿富 赵永望 赵宪琦
北京航空航天大学计算机学院 北京 100191
国内会议
江西九江
中文
278-287
2014-09-01（万方平台首次上网日期，不代表论文的发表时间）