电动汽车控制策略及实例化研究

阐述了电动汽车的动力系统原理,针对整车控制器的功能需求,讨论了其硬件部分的电源电路、信号采集电路、中央处理单元和输出驱动电路以及软件的模块化设计,给出了整车控制器的电路原理图;讨论了电动车系统控制策略,包括充电、上电、辅助作业系统、DC/DC和电子档位等;最后,进行了实例化研究。     

工程建造服务及其建模

“互联网+”与传统行业的融合进行得如火如荼,服务化转型成为融合的关键。然而,工程建造行业尚没有形成对工程建造服务化的统一认识,这不利于其与“互联网+”的融合。在分析工程建造本身服务特性的基础上,提出了工程建造服务的定义并阐释了其内涵。为适应互联网时代的平台交易方式,工程建造服务的虚拟化建模成为关键。为此,探讨了适应互联网共享特性的工程建造服务本体建模,并描述了标准化工程建造服务的实例化,为通过工程建造服务交易完成工程项目打下基础。     

Structured Theory Development for a Mechanized Logic

Experience has shown that large or multi-user interactive proof efforts can benefit significantly from structuring mechanisms, much like those available in many modern programming languages. Such a mechanism can allow some lemmas and definitions to be exported, and others not. In this paper we address two such structuring mechanisms for the ACL2 theorem prover: encapsulation and books. After presenting an introduction to ACL2, this paper justifies the implementation of ACL2s structuring mechanisms and, more generally, formulates and proves high-level correctness properties of ACL2. The issues in the present paper are relevant not only for ACL2 but also for other theorem-proving environments.     

面向对象测试技术的研究与应用

面向对象的测试技术是面向对象开发方法的一个重要方面，它对软件质量和软件重用至关重要。本文描述了有关面向对象测试的一些关键问题，提出了一种面向对象的测试方法，给出了利用Rational公司的测试工具TestMate对C＋＋程序进行面向对象测试的样例。     

Engineering software reuse for on‐board embedded real‐time systems

The dimensions of concern to ambitious reuse initiatives largely exceed the provision of desired functionalities. A domain‐specific blend of functional, technical and quality considerations determines the reuse potential of software reuse assets. In a recent project we realized considerable reuse dividends from coupling the definition of a reference software architecture and of an associated set of standard interfaces with the selection of a powerful computational model equipped with reuse‐geared enabling technology. In this paper we present our engineering approach to the project and show how it earned us a good balance between the preservation of predictability and scalability and the maximization of the reuse objective. Copyright © 2001 John Wiley & Sons, Ltd.     

现场总线功能块的实例化

首先介绍了基金会现场总线功能块的特点，在此基础上提出了功能块实例化的概念. 然后分析了在实现功能块实例化中使用到的动态对象字典（OD）、统一的服务和函数指针技术等几项关键技术． 最后阐述了功能块的实例化技术在实现复杂控制的并行计算和减少总线网络的通讯负担方面所起到的重要作用．     

视景仿真系统中三维建模的优化方法

为了提高虚拟现实系统的实时响应性能和真实性,讨论了基于Multigen Creator建模的关键技术,给出了建模的优化策略,在此基础上实施了一个少数民族文字“女书”碑林园的视景仿真漫游系统。系统运行结果表明,实例化技术、外部引用技术和阴影技术等优化的建模技术降低了三维模型的资源开销,提高了虚拟视景仿真系统的渲染效果和运行效率。     

基于预测的5G网络切片算法

5G网络实时应用场景对网络切片的建立提出了严格的要求,需要使用预测算法提前隔离资源,降低网络切片的建立时间。提出了基于预测的 5G 网络切片算法,以四阶矩为代价函数,在算法复杂度不高的前提下提供必要的预测精度,根据预测结果在5G网络中提前隔离虚拟节点资源和虚拟链路资源,当网络切片请求到达时,直接拉起容器,完成网络切片的动态创建。仿真结果表明,所提算法的预测精度能够达到 90%,在复用原始网络切片资源的条件下,新请求网络切片的创建时间减少50%。     

Comparing Instance Generation Methods for Automated Reasoning

The clause-linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the disconnection tableau calculus, and saturation-based methods, such as primal partial instantiation and resolution-based instance generation. We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one. This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS). See for more information.