基于三值语义的软件运行时验证方法

运行时验证技术是对传统的程序正确性保证技术如模型检验和测试的有效补充。模型检验和测试都试图验证系统的所有可能执行路径的正确性,而运行时验证关注的是系统的当前执行路径。本文提出一种基于三值语义的软件运行时验证方法,一方面该方法提供了从代码插装、系统底层信息提取到监控器生成、验证系统运行轨迹是否满足性质规约的完整的解决方案;另一方面基于三值语义的监控器有发现一条无穷运行轨迹的最小好(坏)前缀的能力,从而使得监控器能尽可能早的发现性质违背。同时,我们开发了基于三值语义的软件运行时验证原型工具并针对案例进行了分析。     

运行时验证中的减少监控开销方法研究

运行时验证中的一个重要研究内容就是减少监控开销,以达到运行时开销对系统影响最小化的目标。总结了近年来运行时验证中减少监控开销技术的研究发展,首先介绍了运行时开销控制的研究现状;然后详细介绍了运行时开销减少的具体方法;最后分析了运行时开销控制技术面临的主要挑战,并对该领域未来的研究方向进行了展望。     

基于AOP 的运行时验证中的冲突检测

现有的形式化验证方法除了在模型层面对系统进行验证以外,越来越倾向于直接针对系统的实际代码和具体运行.运行时验证技术验证的对象是具体程序,它试图把形式化验证技术部署到程序的实际运行过程中.然而在把形式化技术部署到实际运行过程中会出现一系列在模型层面验证通常不会出现的问题,对这些问题中的冲突现象进行了研究,定义了运行时验证技术中存在的两种冲突,并给出了相应的检测算法.最后,对这些算法进行了实现和实例研究,结果表明了该方法的有用性.     

基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。     

参数化运行时监控研究

随着计算机软件广泛应用于各类安全关键系统以及软件日趋复杂,软件可靠性变得越来越重要。作为一种广泛使用于各种平台的软件解决方案,运行时监控是提高软件可靠性的最灵活的解决方案之一。但随着运行时监控技术以及软件技术的发展,人们希望通过运行时监控技术来验证系统的动态属性,从而提出参数化性质的运行时监控技术。由于其在面向对象系统中的适用性,参数化性质的运行时监控已经受到了越来越多的关注。综述了参数化运行时监控的研究进展,提出了参数化运行时监控的问题定义,介绍了这一领域的主要研究内容:参数化运行时监控方法、减少参数化监控开销的技术、多属性规约的参数化运行时监控。     

一种基于MaC的运行时验证框架的研究

介绍一种基于Monitoring and Checking（MaC）的运行时验证框架。受预测语义概念及一种比较成熟的运行时验证工具MaC的启发,通过研究MaC的工作原理和框架,结合预测语言的定义,提出一种运行时验证框架。该工作的意义在于,一方面继承了MaC的逻辑表达能力,在事件、条件的定义上简洁方便;另一方面通过带预测语义的验证器的引入,扩展了MaC的逻辑表达能力,并使得该运行时验证框架带有一定的预测性,为进一步研究基于预测语义的在线主动监控打下良好的基础。     

一种嵌入式操作系统运行时验证方法

作为测试、模型检验等开发阶段所用技术的有效补充,运行时验证技术越来越受到广泛的关注。然而,当前的运行时验证技术主要用于应用软件,很少专门针对操作系统进行研究。对面向嵌入式操作系统的运行时验证框架和关键技术进行了研究,并结合一个开源嵌入式操作系统FreeRTOS进行了设计与实现。首先提出了一种面向嵌入式操作系统的运行时验证和反馈调整框架,然后针对框架中的关键技术部分,完成了规约语言的设计、三值语义监控器的生成、FreeRTOS嵌入式操作系统相关接口的实现等主要工作。     

面向多线程程序的内存安全运行时验证

Linux操作系统、嵌入式系统、航电系统、通信系统等一般都是用C/C++语言进行编写。因为C语言具有偏底层硬件、移植性强、执行效率高等优秀特性。但是随着多核并行机的出现，许多语言也开始支持多线程编程。由于C语言本身存在着对内存访问时，不对内存边界进行检查的问题，从而造成软件系统相关的可靠性和安全性问题。对多线程C语言程序来说，由于多线程程序的不确定性，使得运行时验证多线程C程序的内存安全问题变得更加困难。通过使用基于改进的指针运行时验证技术、多核多线程技术、并行计算、无锁数据结构技术、源代码插桩技术方法，并结合开源工具Clang编译器实现原型工具Movec对多线程C程序的支持。该工具实现了对多线程C程序内存安全问题的运行时验证。然后通过Mibench和SARD测试用例进行实验，验证了该工具对多线程C程序进行运行时验证的有效性。     

运行时验证及其应用

计算机软件在日常生活、工业、军事、国家安全领域已占有重要地位,软件的正确性、可靠性、安全性、可用性和可维护性已经受到广泛关注和深入研究。传统的验证技术包括定理证明、模型检测、以及测试,这些方法受到程序的运行以及程序所在环境的不可控等因素的限制。运行时验证的验证过程基于被监控系统的实际运行过程进行,从而有效地避免这些限制,是传统验证技术的有效补充。     

一种基于活性顺序图的运行时验证研究

运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重写逻辑验证算法效率较低等问题,提出一种基于活性顺序图的运行时验证的改进方法,以支持现有的运行时验证技术。实验表明,改进方法验证结果准确,且验证过程开销较小。     

基于Matlab Runtime Server的应用与开发

针对目前Matlab与其他高级语言混合编程研究成果中存在的局限性,讨论和研究了基于MatlabRuntimeSever的混合编程技术及其开发流程,并将这一研究成功应用于某型飞机试飞地面数据处理系统的设计与开发中。     

Parrot动态编译及其到Java的移植

动态编译是Perl的主要特征之一,Perl6是Perl的下一代版本,而Parrot作为Perl6解释器的实现,提供了更强大的动态编译技术.在深入分析Parrot动态编译技术的基础上,总结其到Java移植的关键点,重点讨论了PMC的移植方法,以及用于动态编译的编译器的获得和保存、注册、运行等的移植方法.阐述了利用Java的Reflection技术访问动态装载的类的方法,从而实现动态链接编译器的移植.     

Runtime analysis of a binary particle swarm optimizer

We investigate the runtime of a binary Particle Swarm Optimizer (PSO) for optimizing pseudo-Boolean functions f:{0,1}ⁿ→R. The binary PSO maintains a swarm of particles searching for good solutions. Each particle consists of a current position from {0,1}ⁿ, its own best position and a velocity vector used in a probabilistic process to update its current position. The velocities for a particle are then updated in the direction of its own best position and the position of the best particle in the swarm.We present a lower bound for the time needed to optimize any pseudo-Boolean function with a unique optimum. To prove upper bounds we transfer a fitness-level argument that is well-established for evolutionary algorithms (EAs) to PSO. This method is applied to estimate the expected runtime for the class of unimodal functions. A simple variant of the binary PSO is considered in more detail for the test function OneMax, showing that there the binary PSO is competitive to EAs. An additional experimental comparison reveals further insights.     

测试任务运行时间

在实时系统中,为满足任务时限要求,测试单个任务运行时间是必不可少的.本文首先讲述两种测试任务运行时间的方法,接着比较和分析这两种方法的优缺点以及测试时应当注意的问题,然后讨论影响任务运行时间的因素,并给出一个如何有效测试任务运行时间的设计方案.     

Efficient algorithms for 2D area management and online task placement on runtime reconfigurable FPGAs

Partial Runtime Reconfigurable (PRTR) FPGAs allow HW tasks to be placed and removed dynamically at runtime. We make two contributions in this paper. First, we present an efficient algorithm for finding the complete set of Maximal Empty Rectangles on a 2D PRTR FPGA. We also present a HW implementation of the algorithm with negligible runtime overhead. Second, we present an efficient online deadline-constrained task placement algorithm for minimizing area fragmentation on the FPGA by using an area fragmentation metric that takes into account probability distribution of sizes of future task arrivals as well as the time axis. The techniques presented in this paper are useful in an operating system for runtime reconfigurable FPGAs to manage the HW resources on the FPGA when HW tasks that arrive and finish dynamically at runtime.     

Matlab/Runtime Server工具箱在工程中的应用研究

作为一种高性能的用于工程计算的编程软件，Matlab具有强大的数值计算、图形处理、算法开发等功能，但是具有这些功能的应用程序只能在Matlab环境中使用，代码执行速度慢。该文系统地分析了用Matlab／Runtime Server工具箱进行Matlab应用程序独立发布技术的特点，并重点阐述了利用该工具箱如何实现对Matlab应用程序的独立发布，最后的工程应用实例讨论了具体实现过程，从而拓宽了Matlab在科学研究和工程技术中的应用领域。     

Defining and documenting execution viewpoints for a large and complex software-intensive system

An execution view is an important asset for developing large and complex systems. An execution view helps practitioners to describe, analyze, and communicate what a software system does at runtime and how it does it. In this paper, we present an approach to define and document viewpoints that guide the construction and use of execution views for an existing large and complex software-intensive system. This approach includes the elicitation of the organization's requirements for execution views, the initial definition and validation of a set of execution viewpoints, and the documentation of the execution viewpoints. The validation and application of the approach have helped us to produce mature viewpoints that are being used to support the construction and use of execution views of the Philips Healthcare MRI scanner, a representative large software-intensive system in the healthcare domain.     

Comparison of simple diversity mechanisms on plateau functions

It is widely assumed and observed in experiments that the use of diversity mechanisms in evolutionary algorithms may have a great impact on its running time. Up to now there is no rigorous analysis pointing out how different diversity mechanisms influence the runtime behavior. We consider evolutionary algorithms that differ from each other in the way they ensure diversity and point out situations where the right mechanism is crucial for the success of the algorithm. The considered evolutionary algorithms either diversify the population with respect to the search points or with respect to function values. Investigating simple plateau functions, we show that using the “right” diversity strategy makes the difference between an exponential and a polynomial runtime. Later on, we examine how the drawback of the “wrong” diversity mechanism can be compensated by increasing the population size.     

Plateaus can be harder in multi-objective optimization

In recent years a lot of progress has been made in understanding the behavior of evolutionary computation methods for single- and multi-objective problems. Our aim is to analyze the diversity mechanisms that are implicitly used in evolutionary algorithms for multi-objective problems by rigorous runtime analyses. We show that, even if the population size is small, the runtime can be exponential where corresponding single-objective problems are optimized within polynomial time. To illustrate this behavior we analyze a simple plateau function in a first step and extend our result to a class of instances of the well-known SetCover problem.     

HPC++:一种支持多线索和远程对象调用的并行语言

本文介绍了一种新型的并行程序设计语言ＨＰＣ＋ ＋ 语言．在由多个结点（共享存储的多处理器）互连起来组成的网络环境下,ＨＰＣ＋ ＋ 不仅支持结点间的并行,还支持结点内的线索并行．另外,利用ＣＯＢＲＡ 的ＩＤＬ技术,用户可以对远程对象的成员函数进行调用．本文还对它的并行标准模版库进行了描述．