Collecting Statistics over Runtime Executions

By collecting statistics over runtime executions of a program we can answer complex queries, such as “what is the average number of packet retransmissions” in a communication protocol, or “how often does process P₁ enter the critical section while process P₂ waits” in a mutual exclusion algorithm. We present an extension to linear-time temporal logic that combines the temporal specification with the collection of statistical data. By translating formulas of this language to alternating automata we obtain a simple and efficient query evaluation algorithm. We illustrate our approach with examples and experimental results.     

参数化运行时监控研究

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

面向动作的上下文感知应用的规约与运行时验证

面向动作的上下文感知（AOCA）应用组织环境中的资源,为用户动作的顺利进行提供支持.为应对环境和动作相关需求的开放性,这类应用采用轻量级、增量式的开发方法进行开发.相比于在开发阶段描述全局信息的开发方法,AOCA应用的开发可能由不同开发者在不同时间共同参与,这可能会导致较多的不一致等问题,且难以在开发阶段被发现.我们围绕使用运行时验证手段提高AOCA应用可靠性这一目标展开了研究.本文给出了对于AOCA应用运行状态进行形式化规约、对于系统级和应用级性质进行描述的方法.进一步地,我们设计实现了AOCA应用监控器.最后,通过案例分析以及性能评估证实该方法的有效性.     

基于插桩和布尔逻辑的运行时程序验证框架

针对软件测试和静态程序验证中存在的连续性程序执行验证和推理问题,提出一个基于程序插桩和布尔逻辑的运行时程序验证框架——RPA。定义一种用于描述运行时程序性质和规范的动态逻辑语言RPAL,实现自动化插桩以收集运行时程序状态信息,设计一个支持高效验证的句子调度算法。实验结果表明,结合合适的谓词扩展,RPA可以有效地验证和分析软件逻辑,发现潜在的软件错误。     

An Overview of the Runtime Verification Tool Java PathExplorer

We present an overview of the Java PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution of a Java program and check that it conforms with a set of user provided properties formulated in temporal logic. JPAX can in addition analyze the program for concurrency errors such as deadlocks and data races. The concurrency analysis requires no user provided specification. The tool facilitates automated instrumentation of a program's bytecode, which when executed will emit an event stream, the execution trace, to an observer. The observer dispatches the incoming event stream to a set of observer processes, each performing a specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications can be formulated by the user in the Maude rewriting logic, where Maude is a high-speed rewriting system for equational logic, but here extended with executable temporal logic. The Maude rewriting engine is then activated as an event driven monitoring process. Alternatively, temporal specifications can be translated into automata or algorithms that can efficiently check the event stream. JPAX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems.     

C程序数组越界的运行时验证技术研究与实现

缓存区溢出能引起非常严重的安全问题,对网络和分布式系统（如机群,网格,P2P系统等）构成严重威胁。数组越界在缓存区溢出中占据重要位置,如何检测数组越界错误是一个重要且极具意义的课题。针对该课题,给出一种对C语言数组越界进行运行时验证的方法。分析了数组越界的错误类型,根据这些类型分别研究了数组越界的运行时验证的思想;设计了基于程序插桩进行数组越界动态检测的算法,给出了该方法基于开源编译器Clang的具体实现;用实验证明了该方法是切实可行并且有效的。     

Rewriting-Based Techniques for Runtime Verification

Techniques for efficiently evaluating future time Linear Temporal Logic (abbreviated LTL) formulae on finite execution traces are presented. While the standard models of LTL are infinite traces, finite traces appear naturally when testing and/or monitoring real applications that only run for limited time periods. A finite trace variant of LTL is formally defined, together with an immediate executable semantics which turns out to be quite inefficient if used directly, via rewriting, as a monitoring procedure. Then three algorithms are investigated. First, a simple synthesis algorithm for monitors based on dynamic programming is presented; despite the efficiency of the generated monitors, they unfortunately need to analyze the trace backwards, thus making them unusable in most practical situations. To circumvent this problem, two rewriting-based practical algorithms are further investigated, one using rewriting directly as a means for online monitoring, and the other using rewriting to generate automata-like monitors, called binary transition tree finite state machines (and abbreviated BTT-FSMs). Both rewriting algorithms are implemented in Maude, an executable specification language based on a very efficient implementation of term rewriting. The first rewriting algorithm essentially consists of a set of equations establishing an executable semantics of LTL, using a simple formula transforming approach. This algorithm is further improved to build automata on-the-fly via caching and reuse of rewrites (called memoization), resulting in a very efficient and small Maude program that can be used to monitor program executions. The second rewriting algorithm builds on the first one and synthesizes provably minimal BTT-FSMs from LTL formulae, which can then be used to analyze execution traces online without the need for a rewriting system. The presented work is part of an ambitious runtime verification and monitoring project at NASA Ames, called PathExplorer, and demonstrates that rewriting can be a tractable and attractive means for experimenting and implementing logics for program monitoring.Supported in part by joint NSF/NASA grant CCR-0234524.     

An Experiment in Program Composition and Proof

This paper explores a compositional approach to program specification, development and proof. We apply a theory of composition to a problem in distributed computing with the goal of understanding the strengths and weaknesses of this compositional approach. First, we describe the theory briefly. Then we give a specification of a desired system. Next, we propose a design of the desired system as a composition of components and prove its correctness. Finally, we show how the proof can be reused for a slightly different compositional structure by using the concept of observation.     

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

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

Checking Finite Traces Using Alternating Automata

Alternating automata have been commonly used as a basis for static verification of reactive systems. In this paper we show how alternating automata can be used in runtime verification. We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a linear-time temporal logic formula. The three methods start from the same alternating automaton but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. We then show how an extension of these algorithms, that collects statistical data while verifying the execution trace, can be used for a more detailed analysis of the runtime behavior. All three methods have been implemented and experimental results are presented.     

Runtime Engine for Dynamic Profile Guided Stride Prefetching

Stride prefetching is recognized as an important technique to improve memory access performance. The prior work usually profiles and/or analyzes the program behavior offline, and uses the identified stride patterns to guide the compilation process by injecting the prefetch instructions at appropriate places. There are some researches trying to enable stride prefetching in runtime systems with online profiling, but they either cannot discover cross-procedural prefetch opportunity, or require special supports in hardware or garbage collection. In this paper, we present a prefetch engine for JVM （Java Virtual Machine）. It firstly identifies the candidate load operations during just-in-time （JIT） compilation, and then instruments the compiled code to profile the addresses of those loads. The runtime profile is collected in a trace buffer, which triggers a prefetch controller upon a protection fault. The prefetch controller analyzes the trace to discover any stride patterns, then modifies the compiled code to inject the prefetch instructions in place of the instrumentations. One of the major advantages of this engine is that, it can detect striding loads in any virtual code places for both regular and irregular code, not being limited with plain loop or procedure scopes. Actually we found the cross-procedural patterns take about 30% of all the prefetchings in the representative Java benchmarks. Another major advantage of the engine is that it has runtime overhead much smaller （the maximal is less than 4.0%） than the benefits it brings. Our evaluation with Apache Harmony JVM shows that the engine can achieve an average 6.2% speed-up with SPECJVM98 and DaCapo on Intel Pentium 4 platform, in spite of the runtime overhead.     

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

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

普适计算应用时空性质的运行时验证

运行时验证是提升普适计算应用可靠性的重要手段.这类应用的很多性质同时涉及时间关系和空间位置关系,这样的时空性质给运行时验证带来了特有的挑战.一方面,传统的时态逻辑难以描述空间性质;另一方面,适合描述空间性质的Ambient Logic在真值不确定等情况下不能很好支持有限轨迹中时间性质的描述.为支持普适计算应用时空性质的运行时验证,本文引入三值逻辑语义,提出了AL₃（3-valued Ambient Logic）;并在此基础上设计实现了基于AL₃的性质检验算法和运行时监控器.最后,通过案例分析和运行效率实验阐明了所提方法的有效性和可行性.     

面向参数化LTL的预测监控器构造技术

介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称P_ALTL)公式运行时预测监控器构造方法.一方面研究P_ALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using);另一方面给出参数化预测监控器的概念.它由静态和动态两部分组成,静态部分由参数化Büchi自动机表示,动态部分为当前状态处的变量赋值.在系统运行过程中,预测监控器基于静态部分的参数化Büchi自动机,以on-the-fly的方式在当前状态处动态地提取和绑定变量赋值,递进地验证当前程序运行是否满足指定的参数化性质规约.在该过程中,参数化监控器能够精确地识别被验证性质的最小好/坏前缀.     

Runtime Monitoring CompositeWeb Services Through Stateful Aspect Extension

The execution of composite Web services with WS-BPEL relies on externally autonomous Web services. This implies the need to constantly monitor the running behavior of the involved parties. Moreover, monitoring the execution of composite Web services for particular patterns is critical to enhance the reliability of the processes. In this paper, we propose an aspect-oriented framework as a solution to provide monitoring and recovery support for composite Web services. In particular, this framework includes 1) a stateful aspect based template, where history-based pointcut specifies patterns of interest cannot be violated within a range, while advice specifies the associated recovery action; 2) a tool support for runtime monitoring and recovery based on aspect-oriented execution environment. Our experiments indicate that the proposed monitoring approach incurs minimal overhead and is efficient. This work is supported by the National Natural Science Foundation of China under Grant Nos. 60673112, 90718033, the National Basic Research 973 Program of China under Grant No. 2009CB320704, and the High-Tech Research and Development 863 Program of China under Grand Nos. 2006AA01Z19B, 2007AA010301.     

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

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

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

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

多核处理器架构下面向监控的软件运行时验证方法研究

面向监控的软件运行时验证(Monitor-oriented Runtime Verification:MRV)方法可以有效的提高系统可靠性,但是在传统基于单核处理器架构的嵌入式系统中采用MRV方法会给目标系统性能造成较大的影响.本文对基于多核处理器架构的MRV方法进行了初步研究,分析并设计了在线验证、离线验证以及单监视器设计与多监视器设计等多种模式的MRV方法,给出了相应的MRV实现方案,并在几个开源项目中进行了MRV实例应用.实验数据分析表明,在不同模式下,基于多核处理器架构的MRV方法能够从不同程度上有效提高系统运行时验证的性能.本文工作为进一步设计有效的多核架构下MRV方法提供了基础.     

基于嵌入式可信平台的运行时监控方法

当前可信计算平台缺乏对自身运行时安全属性的监控,对此,提出一种针对嵌入式可信平台的运行时监控方法。通过自动化的代码插入和运行时实时监控,保证可信平台的运行时安全功能符合设计规范,并保证系统性能和运行状态符合特定条件约束,同时对相应的异常进行实时处理。实验结果表明,随着监控节点数的增长,监控的准确性和实时性提高,而监控开销和异常处理开销处于合理范围。