动作推导引擎及其在语音通信软件设计中的应用

动作逻辑作为描述程序行为的语言,常应用于智能机器人的开发上。该文把动作逻辑作为程序设计中的一种形式化语言,把动作解释为造成系统状态改变的原因,将引擎的思想引入到软件的开发过程中。所谓引擎的思想,就是将状态集合、动作集合输入到引擎中,根据这些输入,引擎自动查找相应的算法并执行,从而形成一个完成特定功能的软件系统。将引擎的思想引入到软件开发过程中,可以实现程序自动生成程序,大大提高了代码的重用,减少软件出错的几率,并且程序可读性、可扩充性和易维护性都大大地被提高。把这种根据用户输入自动生成软件系统的引擎称为动作推导引擎。     

自适应重配置软件系统的运行时监控方法研究

运行时监控技术作为实现自适应软件的一个重要研究内容,现已成为当前很多软件工程方法中用来提高软件产品可信性的一个重要设计原则。针对现有的很多软件监控方法常常将系统的监控逻辑与业务功能逻辑混杂在一起的问题,提出了一个需求模型驱动的、自适应重配置软件的运行时监控方法。以软件系统的目标模型及属性规约为基础,介绍了如何构建系统的监控模型、生成和编织监控代码,以及进行运行时诊断分析和自适应重配置调整。该方法通过采用独立于应用程序的外部单元来实现对运行时系统的监控、诊断和自适应重配置处理。这更利于系统的维护和管理,也更符合软件复用的思想。     

基于观测器的液压系统健康状态评估方法研究

为了实时评估液压系统的健康状态,提出了基于观测器的健康状态评估原理,利用解析模型、仿真模型和数据模型及其配合等方法进行液压系统标准模型的建立,联合实际液压系统的监测数据,构建液压系统的状态观测器。将实际系统的相关参数作为输入,实际监测点的输出与标准模型的输出进行特征分析与对比,在数据处理的基础上形成残差及其向量,运用数据分析方法计算系统健康度,并解析各元素及其耦合所映射的故障类型与故障程度,实现液压系统的故障定位与评估。最后,利用某型装备的起竖液压系统进行了应用举例,介绍了模型构建、故障模式与参数选择、残差构成及健康度计算的方法。所研究的状态评估方法对实时评估液压系统,及开展液压系统视情维修具有参考价值。     

基于虚拟现实技术的智能制造监控系统设计

智能制造单元设备之间数据传输方式多样,导致难以实现整个车间的远程集中监控,因此提出了一个基于虚拟现实技术设计智能制造监控系统。通过现实车间与镜像虚拟车间的动态映射实现可视化监控,构建监控系统总体架构。硬件设计讲述了控制器选择和服务器选择。软件部分利用移动目标检测算法监控车间内移动目标,实现实时监控任务。通过实验表明,设计系统的故障预警精度较高,监控效果较好。     

微机控制医用物料传送台的设计和实现

文章介绍了一种基于微型计算机用于临床检验实验室标本传送的物料传送台的实现和设计；该系统通过上位机完成指令输入、代码编译、输出控制命令和设备监控等功能，通过下位机进行实时运行监控。文中给出了系统的硬件原理图，并介绍了软件的实现过程。实际应用结果表明，该系统运行可靠，使用方便，可扩展性强，具有很强的推广价值。     

基于有理平方根逼近的非高斯随机分布系统的故障诊断和容错控制

随机分布系统指的是输入为常规向量而输出为系统输出的概率密度函数所描述的一类随机系统．该类系统控制算法的目标是选择一个控制输入使得系统的实际输出概率密度函数尽可能跟踪一个事先给定的概率密度函数．本文对采用有理平方根B样条逼近其输出概率密度函数的非高斯动态随机分布系统,提出了一种基于非线性自适应观测器的故障诊断方法．该方法可快速有效地诊断出非高斯随机分布系统故障．通过对故障系统的重组,使故障后系统的输出概率密度函数仍能跟踪给定的分布,实现了该随机系统的容错控制,提高了随机系统的可靠性．     

航天器大功率直流电源数字均流方法

针对航天器大功率直流电源系统电源模块的均流问题,提出了直流电源系统数字均流方法。该方法以供配电主控软件为均流核心,将各直流电源模块进行并联输出,通过以太网与各直流电源模块进行数据交互,采集各直流电源输出电流,通过均流算法调节直流电源输出电压,以达到电源均流的目的,此方法在现有直流电源的基础上,设计了大功率直流电源并联硬件电路,包含输入控制单元、远端补偿电路和输出控制单元,软件上设计供配电主控软件,包含均流控制功能、供配电流程功能和电源模块监控功能。通过实际硬件环境试验表明,该方法均流精度高、响应速度快、故障控制能力强,在航天电源领域具备较高的实用价值。     

基于分层排队网络模型的MCU性能预测及优化研究

针对视频会议系统中的多点控制单元(MCU)提出了一个基于分层排队网络模型的性能预测方法．通过对分层排队网络模型进行扩展，建立了多点控制单元的分层排队模型．设计了一个仿真程序对模型进行评价，仿真程序的输入即模型配置文件．该方法可以较快地从多种设计方案或硬件平台中选择满足系统性能设计目标的软件或硬件配置．仿真结果显示，选择双处理器配置和采用多线程技术，多点控制单元的接入容量提高了50％．最后，多点控制单元终端接入实验证明了该方法的有效性。     

一种基于失效费用划分的穿戴计算机软件可靠性模型

根据故障的严重程度对软件系统中潜伏的故障进行了类型划分，并利用传统的G-O模型建立了一个基于失效费用划分的软件可靠性增长模型．无线网络使穿戴计算机的性能得到了很大的提升，根据是否会严重影响穿戴计算机的网络通信能力，将其软件系统的故障分为两类：①一般故障，不影响或较小影响系统的网络通信；②通信故障，严重影响甚至阻断系统的网络通信．利用前面建立的软件可靠性增长模型，建立了一个穿戴计算机软件系统可靠性增长模型，并对一组数据进行了评估．     

基于移动支付的自动售货机实时监控系统设计

智能自动售货机缺少实时监控功能,导致带来不必要的损失,从而影响消费行为,降低运营商的经济效益。设计基于移动支付的自动售货机实时监控系统。设计系统硬件包括移动支付物联网平台搭建单元、监控芯片选取单元及其监控通信单元;软件包括移动支付物联网监控模块、售货机终端监控模块及其数据库构建模块。通过上述硬件单元与软件模块的设计,实现了自动售货机实时监控系统的运行。测试实验对象,创建实验网络环境,进行自动售货机实时监控实验。实验数据显示：相较于现有系统,设计系统响应时间缩短,监控有效率提升,充分证实了设计系统监控效果更好。     

Toward automatic detection of software failures

To date, no method has explicitly and cost effectively dealt with failure detection in software systems whose specifications are nondeterministic. In such systems, the specification permits multiple outputs for the same input sequence and system state. Nondeterminism in specifications is advantageous because the specification writer can avoid stating irrelevant behavior as mandatory, freeing the software designer to choose a behavioral alternative that would yield a more desirable implementation. Unfortunately, this flexibility comes at a cost to the failure detection mechanism. It must accommodate all the target system's legal behavioral alternatives and avoid favoring one of them. The article describes a hierarchical supervisor whose failure detection mechanism explicitly addresses systems with nondeterministic specifications. The supervisor, a unit separate from the target system, observes the system's external inputs and outputs and reports any failures. Its hierarchical structure results from splitting the task of identifying the behavioral alternative the target system chooses from the task of checking the details of system behavior. This structure makes it possible to efficiently trade off detection accuracy and computational cost. To evaluate their approach, the authors created a prototype supervisor and used it to supervise the execution of the control program of a small telephone exchange. Results indicate that the hierarchical supervisor can significantly reduce the computational cost of considering the target system's behavioral alternatives. However, although the supervisor's computational cost is significantly reduced, it is still higher than that for the target system     

Supervisor direct synthesis method for a structured discrete dynamical system

We present an implementation method for a supervisor of a discrete event system (DES) structured in a special way. Such a DES has the following characteristic features: the language generator is represented by a set of finite automata, the language model is extended with a new type of events called “expected,” and the specification is defined as a sequence of control commands. The primary advantage of our method is that it uses structural knowledge of the event stream in order to construct a supervisor. Thus, we achieve linear dependence of the supervisor’s size in the input data.     

Action Language verifier: an infinite-state model checker for reactive software specifications

Action Language is a specification language for reactive software systems. In this paper, we present the syntax and the semantics of the Action Language and we also present an infinite-state symbolic model checker called Action Language Verifier (ALV) that verifies (or falsifies) CTL properties of Action Language specifications. ALV is built on top of the Composite Symbolic Library, which is a symbolic manipulator that combines multiple symbolic representations. ALV is a polymorphic model checker that can use different combinations of the symbolic representations implemented in the Composite Symbolic Library. We describe the heuristics implemented in ALV for computing fixpoints using the composite symbolic representation. Since Action Language specifications allow declaration of unbounded integer variables and parameterized integer constants, verification of Action Language specifications is undecidable. ALV uses several heuristics to conservatively approximate the fixpoint computations. ALV also implements an automated abstraction technique that enables parameterized verification of a concurrent system with an arbitrary number of identical processes.     

Program Synthesis from Formal Requirements Specifications Using APTS

Formal specifications of software systems are extremely useful because they can be rigorously analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior. To transfer this confidence to the actual source code implementation, a formal link is needed between the specification and the implementation. Generating the implementation directly from the specification provides one such link. A program transformation system such as Paige's APTS can be useful in developing a source code generator. This paper describes a case study in which APTS was used to produce code generators that construct C source code from a requirements specification in the SCR (Software Cost Reduction) tabular notation. In the study, two different code generation strategies were explored. The first strategy uses rewrite rules to transform the parse tree of an SCR specification into a parse tree for the corresponding C code. The second strategy associates a relation with each node of the specification parse tree. Each member of this relation acts as an attribute, holding the C code corresponding to the tree at the associated node; the root of the tree has the entire C program as its member of the relation. This paper describes the two code generators supported by APTS, how each was used to synthesize code for two example SCR requirements specifications, and what was learned about APTS from these implementations.     

多数据源空间数据库引擎的研究与实现

介绍一个中间件系统：面向分布式地理信息系统的多数据源空间数据库引擎。该系统采用三层C／S结构，符合OpenGIS互操作规范，支持数据共享和功能共享，能够用于空间数据库系统集成，支持面向互联网的GIS软件的开发。     

Teaching formal methods lite via testing

A new style of formal methods course is described, based on a pragmatic approach that emphasizes testing. The course introduces students to formal specification using Z, and shows how formal specification and testing can benefit each other, in both the validation and verification phases. It uses a tools‐based approach, with practical work that reinforces formal specification techniques as well as traditional software engineering skills, such as unit and system testing, inspection and defensive programming with assertions. The two main results are to identify several practical uses of formal specifications that are not widely practised or taught, and to demonstrate that teaching them results in a more interesting and relevant formal methods course. Copyright © 2001 John Wiley & Sons, Ltd.     

Software monitoring through formal specification animation

This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs.     

Control of nondeterministic discrete-event systems for bisimulation equivalence

Most prior work on supervisory control of discrete event systems is for achieving deterministic specifications, expressed as formal languages. In this paper we study supervisory control for achieving nondeterministic specifications. Such specifications are useful when designing a system at a higher level of abstraction so that lower level details of system and its specification are omitted to obtain higher level models that may be nondeterministic. Nondeterministic specifications are also meaningful when the system to be controlled has a nondeterministic model due to the lack of information (caused for example by partial observation or unmodeled dynamics). Language equivalence is not an adequate notion of behavioral equivalence for nondeterministic systems, and instead we use the finest known notion of equivalence, namely the bisimulation equivalence. Choice of bisimulation equivalence is also supported by the fact that bisimulation equivalence specification is equivalent to a specification in the temporal logic of /spl mu/-calculus that subsumes the complete branching-time logic CTL*. Given nondeterministic models of system and its specification, we study the design of a supervisor (possibly nondeterministic) such that the controlled system is bisimilar to the specification. We obtain a small model theorem showing that a supervisor exists if and only if it exists over a certain finite state space, namely the power set of Cartesian product of system and specification state spaces. Also, the notion of state-controllability is introduced as part of a necessary and sufficient condition for the existence of a supervisor. In the special case of deterministic systems, we provide an existence condition that can be verified polynomially in both system and specification states, when the existence condition holds.