基于重写技术的程序开发与验证

完整地介绍了一个基于重写技术的程序开发和验证系统,重点展示验证子系统的理论、方法 和技术.验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式,从而进一步保 证程序开发过程的正确性.验证子系统所采用的主要技术是以成批证明方法和证据测试集为 特色的重写归纳方法.     

代数语言规约的ML原型翻译系统

形式化的规约说明对于提高软件开发的正确性和效率有很大作用,一个形式化的规约说明语言开发环境如图1所示。目前有的原型系统是用常规高级语言,即一般的过程语言来写的,如C。这种原型环境涉及大量低层细节.程序繁琐冗长,且和计算机状态相联系,破坏了原有规约的证明特性。     

FSbench:一个机群文件系统基准程序

FSbcnch是一种通用的基于Unix平台的机群文件系统基准程序,它使用独特的时间同步机制来测试文件系统真实并发时的性能,扩展了SPEC SFS的负载测试方法并用来测试多种机群文件系统,提供了多种测试共享文件的模式,可以测试共享文件的并行存取性能。     

暖风机性能测控系统程序开发

本文介绍了汽车暖风机测试装置性能测控系统的硬件构成，以及用VB开发的上位计算机工控软件的设计，着重讨论了在编制过程中遇到的问题及解决方法。     

基于重写方法的程序开发系统的设计和实现

本文介绍了一个基于重写方法的程序开发系统的设计和实现。该系统使用代数规范说明语言和扩展的函数式语言合成而形成的混合语言进行程序设计。系统将代数规范转换为合流的重写系统，并以平行最外方法辅以必要归约进行计算。该文详细介绍了系统的原理和实现技术，并以一些实例说明了系统的特点。     

重写系统中解决发散现象的扩充技术

本文介绍和提出用于解决发散问题的各种基于保守扩充技术的方法.我们特别地用实例证明了这几种新方法可以对带AC算子的重写系统进行归纳完备化.     

一种基于算法骨架的函数式程序变换技术

如何提高函数式程序设计语言在传统冯·诺依曼机器上的执行速度.及效率,一直是该领域中研究的主要论题,对此,并行图归约技术、并行闭包归约、并行编译、并行程序转换等等技术相继成为改善这种状况的措施。     

函数式语言编译器中的G-Machine技术研究

函数式程序设计语言具有程序简洁,易于进行推理和正确性证明等优点。抽象机技术完成函数式程序设计语言的规约计算到传统体系结构的状态转移计算之间的转换,是函数式语言编译技术的核心。本文基于SpinelessG-Machine抽象机的图规约机模型,并在其基础上进行了改进,通过增加闭包,构造全懒惰表达式等,得到了一个更容易理解和易于优化的抽象机模型。并且在此模型上使用了扩展MKAP指令和G-code窥孔优化等方法提高抽象机的效率。     

一个面向分布式程序的测试系统框架

提出了一个面向分布式程序的测试系统框架TFDS(test system framework for distributed software system),并介绍了它在异构网络中的一个实现原型PSET*(distributed progra m structure and event trace, revised version).框架的主要功能是对分布式程序进行单 元测试和集成测试.包括面向规约设计和源码分析的静态部分和面向程序执行和事件序列分 析的动态部分.在构件的基础上,PSET*的功能可以较容易     

一种基于模重写系统的攻击者推理方法

为了解决安全协议验证中攻击者模等式理论推理的可操作性问题,提出并设计了一种基于模重写系统的攻击者推理方法。该方法建立在一个反映两种密码原语代数特性的联合理论实例之上,由一组定向的重写规则和非定向的等式构成,前者进一步转化为项重写系统TRS(Term Rewriting System),而后者则转化为有限等价类理论,通过定义项间的模重写关系,使二者构成一个可以反映攻击者针对联合理论代数项操作能力的模重写系统。实例分析表明,该模型为攻击者模等式推理规则赋予了明确的操作语义,可以使攻击者达到对安全协议代数项规约、推理的目的。     

模型转换的重写逻辑构架研究

规则式的模型转换技术在模型驱动构架的模型转换实施中占有重要地位,但目前诸实施对于转换规则的定义存在多种解释、转换的协调方面、终止性和一致性等数学属性缺乏支持。该文提出一种Maude重写逻辑基础的构架(RLBA)以实施模型转换,通过产生式规范、多方法风格的重写规则集设计、OC(对象配置)和OM(对象消息)重写规则分类等技术并结合模型检查工具,为自动产生元模型和模型的面向对象可执行代数规范、转换规则的严格形式化定义、转换协调方面的刻画、终止性和一致性等的验证提供支持。     

基于Vxworks系统的打印机设备驱动程序的开发

在一个复杂的嵌入式应用系统中,使用嵌入式操作系统会提高研发效率,同时高性能的操作系统也会给整个系统的安全稳定运行提供可靠保障。本文则在此基础上对Vxworks系统的打印机设备驱动程序的开发做出一番探讨,并且成功实现驱动程序的开发。     

基于ATML的可移植TPS开发技术研究

针对当前自动测试系统存在的互操作性差、TPS可移植性难问题,研究了基于ATML标准的可移植TPS开发技术.设计了兼容ATML标准的可移植TPS开发方法,分析了ATML模型结构,形成了AT-ML模型与现有TPS软件平台之间的对接表,并开发了ATML兼容工具,从而实现了基于ATML的可移植TPS开发技术,解决了TPS移植问题,为实现具有通用性、开放性、互操作性的ATS软件及武器装备全寿命周期测试信息共享奠定了基础.     

基于Lua的Linux内核测试工具开发

为减小传统的通过编写大量代码来调用Linux内核及驱动接口进行测试的编程难度,缩短测试周期,采用将Lua脚本语言载入Linux内核并使用脚本语言进行内核及驱动测试的方法,设计并实现一种简易Linux内核驱动测试工具。实验结果表明,该工具所占用的Linux内核空间小,使用灵活方便,可对内核及驱动模块进行准确有效的测试。     

基于DLMS的预付费电能表管理系统设计

针对现有预付费电能表管理系统管理协议不统一、系统运行稳定性及安全性差等不足,以RFID预付费电能表为对象提出了一种基于DLMS标准协议的管理系统设计方案。介绍了系统的模块化构成,实现了售电操作、用户信息管理、系统通信等模块的设计。阐述了管理系统的安全性设计方法,经实验结果和实际应用验证,此系统完全符合技术要求,具有广阔的应用前景。     

基于UML的实时系统开发

面向对象技术已经成为软件开发的主流，在实时系统的开发中，面向对象技术的应用也越来越多。UML是面向对象的标准建模语言，为适应实时系统开发的特殊性，Rational公司对UML进行了扩展，即实时UML(UML-RT)。文章介绍了实时UML，并描述了一个使用Rose RealTime开发工具开发的一个实例。     

基于混合逻辑动态的制造系统建模方法研究

针对制造系统中连续和离散并存的混杂特性,在分析目前混杂系统典型建模方法的基础上,提出采用针对复杂工业过程、集成控制对象定性知识和逻辑规则的混合逻辑动态(MLD)模型对制造系统进行建模方法研究,讨论了制造系统抽象的一般规律,建立了一个具体制造生产线的MLD模型,为今后相关性能分析和控制器设计奠定了基础。     

一个阅卷信息描述语言解释系统的设计

自动阅卷首先必须考虑准确性,但如何提高阅卷代码的重用性、增加阅卷的灵活性是进一步应考虑的问题。文中介绍一个以阅卷信息形式化描述为背景的语言系统的设计过程。该系统有常量、变量、表达式运算、函数运算I、F结构、循环结构等,是一个短小精悍的应用语言系统。借助该系统可以描述复杂的阅卷要求,同时实现了代码和试题的分离,提高了阅卷的开发性和灵活性,在实际应用中取得了良好的效果。该语言系统可进一步应用于开放式考试系统与练习系统平台的设计。