基于IP的存储网技术

文章分析存储网技术的现状,比较几个基于IP的存储网技术方案(FCIP、iFCP和iSCSI),并探讨目前基于IP的存储网技术所面临的问题。     

UML状态机到B形式化规约的转换

文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点．将其转换为B形式化模型，然后在B工具环境中遵循B方法的精化原则和正确性验证方法，开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则，涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明．这套转换规则行之有效。     

ODBC体系结构分析

当今活跃的数据库研究与应用领域,以关系数据库为代表的产品已走向成熟。小型数据库(如Foxpro,Access,Paradox,Dbase,Betrieve等)百花争艳,大型数据库(如Oracle,Sybase,Ingres,Informix,DB2,MS SQL Server等)分割天下。面对这样的局面,作为用户感到既喜又忧:喜的是用户可以有充分的选择自由,并在竞争中得到利益的保障;忧的是各数据库产品间难以互通,给应用程序的移植带来困难。因此,如何解决异构型数据库之间的数据共享,便成为人们多年来研究的课题。ODBC(Open Data—base Connectivity     

自由曲面高斯图闭域包含测试算法设计

提出了一种闭域包含点检测算法,对曲线边先进行包含测试,再找到相交线段,其中对抛物曲线段用二分查找法找到相交线段。由于曲边数远小于逼近多边形的边数n·m,该算法时间复杂度仅为o(n·lnm),加快了检测速度。     

一种改进的用于并发程序静态切片的程序依赖图

分析了Krinke切片算法，发现当对程序循环体内嵌套有一个或多个线程的结构时会产生切片不精确的现象．原因是Krinke算法的数据结构所定义的线程间数据依赖关系过于粗糙，相应的切片算法对程序执行路径的合法性约束不够严格。提出一种改进的并发程序依赖图，引入跨线程边界循环一承载数据依赖关系。给出了添加跨线程边界循环一承载数据依赖关系的算法。实例分析表明，作用在新的并发程序依赖图上的切片算法克服了Krinke算法的切片不精确现象。     

计算机辅助软件工程的发展趋势

文章结合具体应用和软件开发的方法介绍了 CASE 技术在软件研制和设计当中的作用及其今后的发展。     

基于形式语言B的一种新的时态规约方案

提出一套利用B方法中经典AMN记号表达时态规约的函数结构方案以支持实时软件系统的规约和验证。该方案中,时间类型表示为B方法中系统内部支持的非负整数集合,所有依赖于时间的变量都表示成定义域为时间的全函数。该方案可以方便地表达“过去”、“现在”、“稳定”、“跳变”等时态概念。定义了时间类型、“现在”以及与时间有关的变量的宏操作等抽象机,这些抽象机已经通过B工具的一致性验证。可以在实时系统的B形式化规约中直接使用。