摘要
软件正确性是软件可信性的重要属性。在实际软件开发和设计中,需要不断地对软件进行修改,从而软件越来越正确。为了讨论软件的动态近似正确性,基于概率进程代数的ε-互模拟,建立软件越来越正确的形式化描述。定义ε-极限互模拟,用来反应软件实现与规范之间的关系,给出一些特殊的ε-极限互模拟。提出ε-互模拟极限,用其刻画规范是软件实现的极限形式,同时证明ε-互模拟极限的一些性质。
The correctness of software is a key attribution for truStworthiness of software. In the real development and design, the software is modified constantly in order to get correctness, and the software is correct more and more. This paper focuses on the dynamic characterization of correctness. Based on ε- bisimulation of probabilistic process algebra,ε- limit bisimulation is defined which reflects the relation between implementation and its specification, and some special ε- limit bisimulations are showed, ε- bisimulation limit is presented, which states that specification is the limit of implementations. Some important pro- perties are proved.
出处
《计算机工程与应用》
CSCD
2013年第11期15-19,60,共6页
Computer Engineering and Applications
基金
安徽省自然科学基金(No.1308085QF117)
安徽高校省级自然科学研究重点项目(No.KJ2011A248)
安徽高校省级自然科学研究一般项目(No.KJ2012Z347)
上海市高可信计算重点实验室开放项目(No.07DZ22304201004)
关键词
可信性
正确性
形式化
进程代数
trustworthiness
correctness
formalization
process algebra
