摘要：结合形式化软件开发方法和面向对象的方法学,使用SPEC#开发物流信息管理系统,利用该语言中的前置条件、后置条件、对象不变式等形式化机制显著地提高了软件的可读性、可靠性和可维护性。系统地总结了分析、设计和编码阶段的经验和问题,提出了应用SPEC#进行契约式程序设计的一组原则和建议,并分析了该语言存在的不足和改进策略。

摘要：针对测试中遇到的脉冲丢失问题,采用脉冲边沿、脉冲到达时间和脉冲间隔等特征量,设计了快速进行脉冲丢失位置定位和补偿的算法。仿真结果表明,该算法能有效地解决脉冲丢失的问题,对脉冲敏感型的数据分析和故障诊断具有重要意义。

摘要：针对任务关键性的武器装备控制领域,选用B方法来设计通用弹道计算机程序,显著地提高了软件的质量和可靠性。在开发过程中,利用抽象机机制对基本弹道计算机进行建模,并通过逐步精化的方法扩展弹道计算机功能,从而有效地控制了弹道计算参数之间的复杂关系,依赖不变式技术形式化地保证了软件运行时的安全性,并使得生成的程序具有良好的重用性和可扩展性。

摘要：提出了一个装备保障领域驱动的约束程序设计框架,定义了问题规约、问题求解、保障资源、保障任务和保障对象五个相互正交的剖面.其中问题规约剖面是对问题目标和约束的抽象描述;将之与保障资源、保障任务和保障对象剖面依次进行正交组合后,能够得到精确的具体问题规约;最后利用启发式规则在问题求解剖面中选择合适的算法,可实现联勤保障规划类问题的高效求解.

摘要：软件的功能性冗余能够有效提高计算机系统可靠性和安全性。研究了SPEC#语言中的前后置断言和对象不变式等契约机制,分析了如何通过这些机制来实现输入输出域控制、主动冗余和故障恢复等软件功能性冗余的方法和手段,并总结了软件开发过程中应用契约设计和冗余技术的若干准则和建议。这种基于契约的冗余技术能够显著地提高软件的可靠性、可维护性和可测试性,进而提高软硬件系统的整体可信性水平。

摘要：针对普通摆动气缸不能在行程中间实现任意点精确、快速定位的问题,研究开发一种摆动伺服气缸。提出集成叶片式气压驱动装置、圆盘式磁流变液旋转阻尼器、角度检测装置的摆动伺服气缸结构方案。设计了高速响应的驱动电源,线圈电流的阶跃响应时间约为1ms。对摆动伺服气缸基本性能试验结果表明:摆动伺服气缸具有良好的驱动性能,摩擦力矩较小,对气压驱动基本无影响,可调阻尼力矩在控制电压4.5V时达到饱和阻尼力矩24.7N·m,动态力矩平稳,波动在5%以内,输出力矩响应时间约为35ms。

摘要：论文介绍了一种工程装备液压系统状态检测诊断系统。该检测仪由硬件和软件两部分组成,硬件部分包括ECM-945GSE工控机、基于ARM芯片的嵌入式数据采集系统、液晶屏、触摸屏、电源模块和传感器等。软件系统主要包括数据采集程序、故障诊断和检测主程序、输出打印程序等。现场的试用试验表明,该设备能够快速方便地检测诊断液压系统的故障,提高工程机械检测与维修保障的效率。

摘要：为提高装备保障决策支持系统的整体质量,将形式化方法应用于系统设计和组件开发,特别是关键算法的设计和实现,从而大幅提高了软件的可靠性、可复用性,以及问题求解的效率,有助于装备保障整体效能的提升.