某资料档案库楼板裂缝成因分析及加固处理

通过对某资料档案库楼板裂缝展布规律、缝宽及实际承受荷载的实测和分析,采用PKPM软件对结构在设计荷载和实际使用荷载两种工况下的安全性进行验算,找出楼板裂缝产生的原因,评价了结构的安全性。为保证结构的安全性和耐久性．提出了楼板裂缝处理的工程措施。     

蛟河市池水橡胶坝工程复核计算分析

池水橡胶坝工程是池水灌区渠首工程,位于蛟河市蛟西大桥下游272米处,在蛟河支流拉法河下游,流域面积995平方公里。橡胶坝原设计标准为50年一遇洪水,设计洪水流量980立方米/秒,灌溉面积700公顷。橡胶坝岸墙断裂、错位,充水系统报废,坝袋老化达不到设计要求,配电线路老化失修,交通桥破坏达不到设计标准,存在安全隐患,金属设备锈蚀老化,橡胶坝上下游淤积较严重等问题,针对上述等问题建议对该橡胶坝做以下工作:进行闸室的整体稳定性、抗渗稳定性、橡胶坝过水能力、消能防冲和结构强度等复核计算.     

一种基于模型检测的二进制程序脆弱性分析框架

针对二进制程序脆弱性分析的实际需求,提出了一种基于模型检测的二进制程序脆弱性分析框架。首先定义了二进制程序的抽象模型,描述了基于有限状态自动机的软件脆弱性形式化表示和基于事件系统的软件安全属性表示方法。在此基础上,提出了基于模型检测的脆弱性分析过程和算法。根据该分析框架,设计并实现了二进制程序脆弱性分析工具原型。通过脆弱性分析实验,详细说明了该框架的工作原理,验证了该分析方法的有效性。     

一种基于UPPAAL的Web服务组合模型检测方法

Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义。为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法,考虑到Web服务组合中的实时特征,在采用软件体系结构描述语言XYG/ADL对Web服务组合进行描述的基础上,将其实时描述部分XYZ/RE转换至时间自动机模型,组合后系统应满足的性质用分支时序逻辑CTL公式表示,最后应用模型检测工具UPPAAL实现了Web服务组合正确性的自动化验证。     

采用了剪枝优化的子类型关系判定算法

静态类型化XML处理语言为处理XML数据提供了新的途径,但现有的此类语言大多数效率较低.研究此类语言的一个重要问题——子类型关系的判定,并使用剪枝优化策略对XDuce的子类型关系判定算法进行优化.实验数据显示,优化后算法的执行效率平均提高20%.该策略具有普遍性,对所有使用类似算法的静态类型化XML处理语言都有效.     

模型检测在软件测试中的应用研究

以测试为基础的模型或规格是产生测试用例的一种很有潜力技术。在这种方法中,先要建立一个系统的规格或模型,再由规格或模型产生测试用例。文章对结合模型检测来进行测试的方法进行了研究,从整体上对测试进行考虑,不仅包含了对系统所希望具有的功能进行测试,还包括了对系统不应具有的功能进行测试。通过这种方法,我们可以进一步保证系统的正确性和可靠,大大降低人力和资源的开销,为进一步优化测试奠定了基础。     

基于Java内存模型的并发程序模型检测

为了提高性能,Java内存模型允许编译器在优化过程中改变代码的执行顺序,同时该技术也会造成共享数据的更新顺序与本来的执行顺序不同。在多线程Java并发程序中,这些代码乱序执行会引起很多难以发现的错误。现有的Java程序模型检测技术并没有考虑这些顺序改变的问题。因此,本文提出了一种建立包含多线程交互及线程内代码乱序执行的完整模型,并利用模型检测工具进行穷举检测的算法。该算法可以发现原有技术无法发现的新问题,更好地检测高可靠性要求的Java并发程序。     

基于启发式行为监测的手机病毒防治研究

快速发展的移动通信技术给人们带来新的应用和服务的同时,也吸引了手机病毒的攻击。本文总结了手机病毒的传播途径和共有特性,比较现有的防毒技术,结合手机的特点,提出一种基于启发式行为监测的手机病毒防治技术,采用隐马尔科夫模型启发式分析程序的行为,以阻止病毒的恶意行为,保护手机安全。     

802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

Efficient SAT-based bounded model checking for software verification

This paper discusses our methodology for formal analysis and automatic verification of software programs. It is applicable to a large subset of the C programming language that includes pointer arithmetic and bounded recursion. We consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. We perform this analysis via a translation to a Boolean circuit representation based on modeling basic blocks. The program is then analyzed by a back-end SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program.