Radl形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.

移动实时事务的相对时间正确性及其实现

随着移动通信技术的迅速发展 ,人们提出了新的应用要求 :在移动环境下处理实时事务 .而移动通信的带宽有限性引起较大的数据访问延迟 ,有时甚至由于网络传输的断接而使得事务得不到所需访问的数据 ,这些严重影响了移动环境下实时事务截止期的满足 .实时事务的时间要求 (典型地为截止性 )的满足通常比事务执行的逻辑结果的完全正确更为重要 .该文提出了移动环境下实时事务的“相对”时间正确性标准 ,只要事务访问的数据的陈旧度 (staleness)在控制的范围内 ,就不一定要求实时事务访问的数据在事务提交时是有效的 .文中提出了移动实时事务的相对时间正确性标准、保证事务相对时间正确性标准的算法及移动实时事务执行模型 .所有这些策略一方面降低了移动实时事务的并发控制代价 ,另一方面以牺牲事务的“绝对”时间正确换取事务截止期的满足 ,这与实时数据库“宁愿要部分正确但及时的结果而不愿要绝对正确但过时的结果”的系统目标是相一致的 .实验表明 :相对时间正确性标准的提出及相应的事务执行模型能提高系统中满足截止期事务的比率 ,从而提高了系统性能 .