Monitoring Java Programs with Java PathExplorer

We present recent work on the development of Java PathExplorer (JPaX), a tool for monitoring the execution of Java programs. 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. The tool facilitates automated instrumentation of a program's byte code, which will then emit events to an observer during its execution. The observer checks the events against user provided high level requirement specifications, for example temporal logic formulae, and against lower level error detection procedures, usually concurrency related such as deadlock and data race algorithms. High level requirement specifications together with their underlying logics are defined in rewriting logic using Maude, and then can either be directly checked using Maude rewriting engine, or be first translated to efficient data structures and then checked in Java.     

Synchronous set relations in rewriting logic

This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure, which is written in the Maude system, enables the synchronous execution of a set relation provided by the user. By using the infrastructure, algorithm verification techniques such as reachability analysis and model checking, already available in Maude for traditional asynchronous rewriting, are automatically available to synchronous set rewriting. In this way, set-based synchronous languages and systems such as those built from agents, components, or objects can be naturally specified and simulated, and are also amenable to formal verification in the Maude system. The use of the infrastructure and some of its Maude-based verification capabilities are illustrated with an executable operational semantics of the Plan Execution Interchange Language (PLEXIL), a synchronous language developed by NASA to support autonomous spacecraft operations.     

Two Case Studies of Semantics Execution in Maude: CCS and LOTOS

We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing and executing inference systems. In order to illustrate the general ideas we consider two substantial case studies. In the first one, we represent both the semantics of Milner’s CCS and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics is already known, it cannot be directly executed in the default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved in a general, not CCS dependent way by controlling the rewriting process by means of reflection. This executable specification plus the reflective control of rewriting can be used to analyze CCS processes. The same techniques are also used to implement a symbolic semantics for LOTOS in our second case study. The good properties of Maude as a metalanguage allow us to implement a whole formal tool where LOTOS specifications without restrictions in their data types (given as ACT ONE specifications) can be executed. In summary, we present Maude as an executable semantic framework by providing easy-tool-building techniques for a language given its operational semantics.Research supported by CICYT projects Desarrollo Formal de Sistemas Distribuidos (TIC97-0669-C03-01) and Desarrollo Formal de Sistemas Basados en Agentes Móviles (TIC2000-0701-C02-01).     

Generating Java Compiler Optimizers Using Bidirectional CTL

There have been several research works that analyze and optimize programs using temporal logic. However, no evaluation of optimization time or execution time of these implementations has been done for any real programming language. In this paper, we present a system that generates a Java optimizer from specifications in temporal logic. The specification is simpler, and the generated optimizers run more efficiently than previously reported work. We implemented a new model checker for a bidirectional CTL (computational tree logic) called CTL_bd, which is equivalent to CTL-FV [Lacey, D., Jones, N.D., Van Wyk, E. and Frederiksen, C.C.: Compiler optimization correctness by temporal logic. Higher-Order and Symbolic Computation, Vol. 17, No. 3, pp. 173–206, 2004] after removing free variables. The model checker can check future and past temporal CTL operators symmetrically without any conversion. We also present a new specification language based on the bidirectional CTL that can express typical optimization rules very naturally. By adding rewriting conditions to allow for temporary variables and considering real-world language features such as exceptions, the system can perform optimization of Java programs. So far, a compiler optimizer using temporal logic was assumed to be impractical, because it consumes too much time. However, with our method, the generated Java compiler optimizer can compile seven of the SPECjvm98 benchmarks with a compile time from 4 seconds to 4 minutes.     

Using Maude to write and execute ODP information viewpoint specifications

The aim of the open distributed processing (ODP) information viewpoint is to describe the semantics of the information and of the information processing in a system, from a global point of view, without having to worry about other considerations, such as how the information will be finally distributed or implemented or the technology used to achieve such implementation. Although several notations have been proposed to model this ODP viewpoint, they are not expressive enough to faithfully represent all the information concepts, or they tend to suffer from a lack of (formal) support, or both. In this paper, we explore the use of Maude as a formal notation for writing ODP information specifications. Maude is an executable rewriting logic language especially well suited for the specification of object-oriented open and distributed systems. We show how Maude offers a simple, natural, and accurate way of modeling the ODP information viewpoint concepts, allows the execution of the specifications produced, and offers good tool support for reasoning about them.     

Interface-Based Specification and Verification of Concurrency Controllers

We present a modular approach to specification and verification of concurrency controllers by decoupling their behavior and interface specifications. The behavior specification of a concurrency controller defines how its shared variables change their values whereas the interface specification defines the order in which a client thread should call its methods. We show that the concurrency controllers can be designed modularly by composing their interfaces. We separate the verification of the concurrency controllers from the verification of the threads that use them. For the verification of the concurrency controllers we use infinite state verification techniques which enable us to verify controllers with parameterized constants and arbitrary number of user threads. We automatically generate Java monitors from the concurrency controller specifications which preserve the verified properties. For the thread verification we use finite state program verification tools which enable us to verify Java threads without any restrictions. We show that the user threads can be verified using stubs generated from the concurrency controller interfaces which improves the efficiency of the thread verification significantly.     

Executable structural operational semantics in Maude

This paper describes in detail how to bridge the gap between theory and practice when implementing in Maude structural operational semantics described in rewriting logic, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2. We validate this technique using it in several case studies: a functional language Fpl (evaluation and computation semantics), an imperative language WhileL (evaluation and computation semantics), Kahn’s functional language Mini-ML (evaluation or natural semantics), Milner’s CCS (with strong and weak transitions), and Full LOTOS (including ACT ONE data type specifications). In addition, on top of CCS we develop an implementation of the Hennessy–Milner modal logic for describing local capabilities of processes, and for LOTOS we build an entire tool where Full LOTOS specifications can be entered and executed (without user knowledge of the underlying implementation of the semantics). We also compare this method based on transitions as rewrites with another one based on transitions as judgements.     

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.     

UML行为图驱动的Java程序运行时验证工具

UML是一种标准的可视化建模工具，广泛应用于软件系统的描述、可视化、构建和建立文档。本文介绍了一种UMI。行为图驱动的Java程序运行时验证工具。该工具以一个随机的测试用例集作为输入，运行经过插装的被测Java程序，得到一组用于验证的程序运行轨迹。通过对程序运行轨迹和UML行为图中合法的事件序列的比较，该工具可以对程序的动态行为规约进行检查。本文描述了该工具的设计思想、算法和实现技术，并通过对实例研究对该工具的可用性和有效性进行了讨论。     

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

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