MFS:一个基于重写技术的程序开发系统

MFS是一个基于重写技术的程序开发系统．它提供的程序设计语言MFSL是扩展的函数式语言与代数规约语言相结合的混合语言．在这种混合语言中引入了能够提高效率和满足用户特殊需求的优化规则定义机制．语言的类型系统以及在语言和系统中引入的证明和测试机制能够使人们在开发过程中较早地发现问题,提高所开发系统的正确性．在系统的实现中采用的必要平行最外归约策略、图归约、证据测试集等技术能够使所开发的系统具有很高的实现效率．应用这一程序开发系统,能够较快地开发出正确且效率较高的程序．     

多旋翼飞控推进子系统的Coq形式化验证

飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.     

区间逻辑的一个辅助证明工具

DC/P(duration calculus prover)是一族实时区间逻辑的辅助定理证明工具.它采用Gentzen风格相继式演算作为基本证明系统,并结合项重写、自动判定算法等技术以提高证明的自动化程序.该文介绍了DC/P的语义编码方法、采用的相继式证明系统及实现技术,并给出了应用实例.     

基于项重写系统的联锁系统模型检测方法研究

模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。     

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

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

基于树语言逼近的安全协议形式化分析

利用形式化方法或工具自动化分析实用安全协议十分必要,定理证明技术因其可解决无限状态系统的验证备受关注,但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础,以项重写形式化定义协议模型,以树自动机模拟协议攻击者知识集,给出攻击者知识集可达项逼近求解的算法,并根据上述模型讨论秘密性和认证性的验证方法,最后以Needham-Schroeder公钥认证协议为例验证模型的有效性,并指出下一步研究方向。     

一种通用自动测试系统自检子系统的设计与实现

针对某型PXI总线通用自动测试系统的测试资源较多、传统人工检测效率低、时间长、强度大且易出错的难题,提出了一种基于仪器自检、重要关键仪器测试、灵活运用开关及多路复用器的自检方案.利用RCV与ITA接口设计研制了自检适配器;采用虚拟仪器技术设计开发了自检子系统测试程序.测试验证结果表明,该自检子系统实现了对通用自动测试系统的快速、准确的自检测试功能,为快速定位故障模块提供了检测手段.     

重写对策在基于HOL的形式化证明中的应用

讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用.通过REWRITE_ TAC对策、ASM_ REWRITE_ TAC对策和RW_ TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较.进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题.     

悬臂式灯具配光自动化测试设备研究与实现

为了实现摩托车前照灯光照度和信号灯发光强度的自动化测试,自主研发了一种悬臂式灯具配光性能测试设备.阐述了测试设备的工作原理和系统组成,设计开发了测试设备的机械结构、控制子系统、测试子系统、软件系统等主要模块,并以摩托车制动灯为例进行配光测试实例验证.研究表明,悬臂式配光测试设备可以实现摩托车前照灯和信号灯配光性能的高效自动化测试,具有较好的测量精度和稳定性;测试设备已投入生产使用,满足生产单位的测试需要.     

实时图像识别系统PCI驱动程序设计与开发

为提高实时图像识别系统的数据传输速率和识别搜索效率,分析驱动程序设计的关键问题,提出类FACADE设计模式,并将其作为驱动程序接口设计的框架.在阐述WDM驱动模型基本结构和核心概念的基础上,采用类FACADE设计模式和MDL内存描述方法,开发实时图像识别系统PCI设备驱动程序.通过向量识别程序测试,验证了该驱动程序的有效性和稳定性;通过车牌识别程序测试,验证了类FACADE设计模式可使图像识别系统识别搜索效率提高20倍.     

基于Telnet的节目分送系统的设计原理与实现

ＶＯＤ技术是当前多媒体应用技术中的一项热点技术,节目分送子系统的目标是根据节目排程自动把省中心视频服务器节目及相应的资料下载到地市州视频服务器中,在简介ＶＯＤ系统的基础上,主要讨论了节目分送系统的原理与实现。     

ADI: Automatic Derivation of Invariants

Most current systems for mechanical program verification are not fully automatic, since the user himself must provide the intermediate inductive assertions. This paper describes an interactive computer program, called ADI, which automatically generates the needed inductive assertions. ADI is also able to extend partial loop assertions supplied by the user to form complete assertions. The implementation (written in QLISP and INTERLISP) is based on both the algorithmic and the heuristic approaches introduced by Katz and Manna in "Logical Analysis of Programs" [25]. For the algorithmic subsystem ADI includes: Difference Equations Constructor, Difference Equations Solver, and Invariants from Conditional Statements Generator. The heuristic subsystem includes: Exit Rules Package, Bounding Variables Component, Strengthening Executer, Weakening Executer, and a Heuristic Invariant Matcher-which is the actual implementation of two new heuristics, MATCHPQ and MATCHPT. ADI is a small step toward interactive, practical program verification.     

Cathedral-II: A Silicon Compiler for Digital Signal Processing

The article describes the status of work at IMEC on the Cathedral-II silicon compiler. The compiler was developed to synthesize synchronous multiprocessor system chips for digital signal processing. It is a continuation of work on the Cathedral-I operational silicon compiler for bit-serial digital filters. Cathedral-II is based on a ?meet in the middle? design method that encourages a total separation between system design and reusable silicon design. The CAD system includes a rule-based synthesis program, a procedural program, and a controller synthesis environment. Processors are synthesized in terms of modules called from automated reusable module generators. Chip layout is done on a floor planner. An expert subsystem verifies correctness during silicon design and generates functional and timing models for verification at the module and chip levels.     

基于SSX10的支付密码核验系统的设计与实现

目前银行票据核验主要是人工的,存在着不安全、效率低、易出错等问题。针对这些问题,该文提出一种基于SSX10的支付密码核验系统。系统主要由三大部分组成:人行核验子系统、商业银行核验子系统、商业银行核验前台系统,通过Intranet和业务系统集成在一起,可以快速、可靠、安全地处理支付凭证。目前系统已无故障运行5000小时以上,提高工作效率百倍以上,为银行电子化业务实时核算奠定了坚实的基础。     

片上多核处理器存储一致性验证

存储一致性验证是片上多核处理器功能验证的重要部分.由于验证并行程序的执行结果是否符合存储一致性模型理论上是NP难问题,现有的验证方法中只能采用一些时间复杂度大于O(n3)的不完全方法.发现在支持写原子性的多处理器系统中,两条执行时间不重叠的操作之间存在确定的时间序.通过引入时间序的概念,设计并实现了一种线性时间复杂度的存储一致性验证工具LCHECK.LCHECK利用时间序将验证局部化,使得在表示程序执行结果的有向图中,序关系边的推导和正确性检测都被限定在有限范围内.与现有其他方法相比,LCHECK时间复杂度低,对程序长度和访存地址数没有限制,因此验证效率更高.作为国产片上多核处理器龙芯3号的重要验证工具, LCHECK发现了一些存储系统的设计错误.     

基于PKI的联行支票核验系统的设计与实现

目前票据联行核验主要是人工的,存在着不安全、效率低、易出错等问题。针对这些问题,提出一种基于PKI技术框架的支票联行核验系统。系统主要由4大部分组成:CA、人行核验子系统、商业银行核验子系统、商业银行核验前台系统,通过Intranet和业务系统集成在一起,可以快速、可靠、安全地处理支付凭证。目前系统已无故障运行5 000小时以上,提高工作效率百倍以上,为银行电子化业务实时核算奠定了坚实的基础。     

Verification of linear algebra programs in the spektr system

A subsystem for verification of linear algebra programs is described. The subsystem is implemented as part of the problem-oriented verification system SPEKTR.Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 136–144, September–October, 1992.     

基于基数K链表的动态软件水印版权保护机制研究

目前对于软件的版权保护主要有两方面，一是版权的归属证明，二是软件非法复制的消除与鉴别。按现有技术手段后者的实现难度较大，而软件知识产权的证明则在技术上具有可行性。文章利用大数分解难题，实现了一个基于基数K链表的动态软件水印系统。通过该系统，用户版权证明信息可在软件运行时经过特定触发条件动态构建于程序内存空间中。实验结果表明，已嵌入的动态水印能够被正确提取，且相比传统的静态水印技术，该水印系统具有隐蔽性高、抗攻击性强、实现简单等特点，且嵌入的水印对宿主程序的运行性能基本没有影响。     

基于“软硬结合”平台的导航战体系对抗与评估系统研究

为了实现全规模、等要素的真实或近真实条件的导航战体系对抗及评估,基于"软硬结合"平台的导航战体系对抗与评估系统提出"软硬结合"的系统架构,即用计算机网络把试验推演评估仿真分系统和对抗硬件平台系统试验连接起来,设计的试验推演评估仿真分系统基于软件虚拟方式满足系统灵活性及一定规模的要求,和工程体系对照的物理仿真分系统具备装备实体物理特性,"软硬结合"模式通过硬件设备可与软件模型无差别的等效集成,共同构建试验环境;在导航战体系对抗过程中实现了对体系的信息流、时间流、预期试验结论等验证内容,实现了进行全规模、全要素验证要求,并具备灵活性与真实性有效统一;现有初步规模设备的典型应用场景对抗的试验结果表明,"软硬结合"平台这一体系能够满足相应的体系化、网络化系统对抗和多层次、全方位的体系对抗需求。     

Formal verification and simulation for platform screen doors and collision avoidance in subway control systems

For hybrid systems, hybrid automata-based tools are capable of verification, while Matlab Simulink/Stateflow is proficient in simulation. We propose a co-verification procedure, in which the verification tool SpaceEx/PHAVer and simulation tool Matlab are integrated to analyze and verify hybrid systems. For the application of this procedure, a platform screen door system (PSDS, a subsystem of the subway control system), is modeled with hybrid automata and Simulink/Stateflow charts, respectively. The models of PSDS are simulated by Matlab and verified by SpaceEx/PHAVer. The simulation and verification results indicate that the sandwiched situation can be avoided under time interval conditions. We improve the model with four trains and four stations on a subway line and analyze the urgent control scenario for the safety distance requirement. In this paper, the Simulink/Stateflow model is a refinement of the SpaceEx/PHAVer model, which is closer to a final implementation. Moreover, the two models are complementary for some features (e.g.,visualization of simulation, correctness proving by verification), stressing different aspects of the overall system and permitting complementary analysis techniques, i.e., verification versus simulation. We conclude that this integration procedure is competent in verifying subway control systems.