Catálogo de publicaciones - libros

PSL is a property specification language recently standardized as IEEE 1850-2005 PSL. It includes as its a linear temporal logic that enhances LTL with regular expressions and other useful features. PSL and its precursor, Sugar, have been used by the IBM Haifa Research Laboratory for formal verification of hardware since 1993, and for informal (dynamic, simulation runtime) verification of hardware since 1997. More recently both Sugar and PSL have been used for formal, dynamic, and runtime verification of software. In this paper I will introduce PSL and briefly touch on theoretical and practical issues in the use of PSL for dynamic and runtime verification.

Trace monitor specifications consist of a pattern that is matched against the trace of events of a subject system. We investigate the design choices in defining the semantics of matching patterns against traces.

Some systems use an semantics (where every relevant event must be matched by the pattern), while others employ a semantics (which allows any event to be skipped during matching). The semantics of exact-match is well established; here we give a semantics to skipping by providing a translation to exact-match. It turns out the translation is surjective: a pattern language with skipping semantics is strictly less expressive than one with exact-match semantics. That proof suggests the addition of a novel operator to a skipping language that makes it equivalent to exact-match.

Another design decision concerns the atoms in patterns: are these unique runtime events, or can multiple atoms match the same runtime event? Many implementations have chosen predicates for atoms, and then overlap is natural. There are some exceptions, however, and we examine the consequences of that design choice in some depth.

Perfect pre-deployment test coverage is notoriously difficult to achieve for large applications. With enough end users, many more test cases will be encountered during an application’s deployment than during testing. The use of runtime verification after deployment would enable developers to detect and report on unexpected situations. Unfortunately, the prohibitive performance cost of runtime monitors prevents their use in deployed code.

In this work we study the feasibility of collaborative runtime verification, a verification approach which distributes the burden of runtime verification onto multiple users. Each user executes a partially instrumented program and therefore suffers only a fraction of the instrumentation overhead.

We focus on runtime verification using tracematches. Tracematches are a specification formalism that allows users to specify runtime verification properties via regular expressions with free variables over the dynamic execution trace. We propose two techniques for soundly partitioning the instrumentation required for tracematches: spatial partitioning, where different copies of a program monitor different program points for violations, and temporal partitioning, where monitoring is switched on and off over time. We evaluate the relative impact of partitioning on a user’s runtime overhead by applying each partitioning technique to a collection of benchmarks that would otherwise incur significant instrumentation overhead.

Our results show that spatial partitioning almost completely eliminates runtime overhead (for any particular benchmark copy) on many of our test cases, and that temporal partitioning scales well and provides runtime verification on a “pay as you go” basis.

Aspects have been successfully promoted as a means to improve the modularization of software in the presence of crosscutting concerns. The so-called is considered to be one of the remaining challenges of aspect-oriented software development: aspects may interfere with the behavior of the base code or other aspects. Especially interference between aspects is difficult to prevent, as this may be caused solely by the composition of aspects that behave correctly in isolation. A typical situation where this may occur is when multiple advices are applied at a , join point.

In [1] we explained the problem of behavioral conflicts between aspects at shared join points. We presented an approach for the detection of behavioral conflicts. This approach is based on a novel abstraction model for representing the behavior of advice. This model allows the expression of both primitive and complex behavior in a simple manner. This supports automatic conflict detection. The presented approach employs a set of conflict detection rules, which can be used to detect generic, domain specific and application specific conflicts. The approach is implemented in Compose*, which is an implementation of Composition Filters. This application shows that a declarative advice language can be exploited for aiding automated conflict detection.

This paper discusses the need for a runtime extension to the described static approach. It also presents a possible implementation approach of such an extension in Compose*. This allows us to reason efficiently about the behavior of aspects. It also enables us to detect these conflicts with minimal overhead at runtime.

HALO is a novel aspect language introducing a logic-based pointcut language which combines history-based pointcuts and “escape” conditions for interacting with the base language. This combination is difficult to support when escape conditions access context exposed by “future” join points. This paper introduces a weaving mechanism based on copying objects for resolving such pointcuts. Though this seems a memory consuming solution, it can be easily combined with HALO’s analysis for reducing the join point history. Furthermore, pointcuts with escape conditions accessing future join point context, sometimes require memory than pointcuts that don’t, but otherwise implement the same functionality. In this paper, we illustrate this by measuring memory usage for simulations of an e-commerce application, switching between an implementation where the pointcut definitions contain escape conditions referring to future join point context, and an equivalent implementation that doesn’t.

Runtime verification is one systematic strategy for analytical quality assurance of complex distributed systems. Model-based development approaches are promising in this context because they provide models of manageable size and complexity describing the systems under development, enabling systematic engineering processes for all development phases on various levels of detail. For runtime verification, executing implementations are monitored continuously for correctness against the specification. This requires the insertion of monitors into the software under test to gather information on system states and their evolution. In this paper we describe how we use aspect-oriented development techniques to enhance existing code with runtime monitors checking the interaction behavior of applications against their specifications. We use Message Sequence Charts (MSCs) to specify the interaction behavior of distributed systems and as basis for automatic runtime monitor generation. This uniquely ties interaction interface specifications with the monitoring infrastructure for their realization. We explain the monitor generation procedure and tool set using a case study from the embedded automotive systems domain, the Central Locking System (CLS).

This paper describes an approach to generate AspectJ aspects from formal specifications written for the Monitoring and Checking (MaC) runtime verification tool. The aspects can serve as the foundation for instrumentation of programs that can be verified at runtime. To demonstrate the practicability of the proposed approach, the authors used a benchmark from the MaC research. The benchmark is based on a safety-critical railroad crossing system comprised of a train, a gate, and a controller. Finally, the paper describes the results from generating Java-MaCs specification scripts to AspectJ aspects, and it compares the proposed approach to related approaches and ones that use aspects.

Software quality assurance activities consume a large amount of effort in industrial software developments. Actually, industrial software development sometimes requires a larger amount of testing/verification assets than the product code itself. Appropriate management of the testing/verification assets will effectively reduce the software quality assurance effort. We propose a verification asset reuse environment based on the aspect-oriented programming paradigm. Our tool, ARVE (Aspect-oriented Runtime Verification Environment), enables efficient verification asset reuse thanks to the aspect-oriented scripting language. ARVE also promotes the efficiency of the verification process by automating the verification script weaving.

We consider evolvable computational systems built as hierarchies of evolvable components, where an evolvable component is an encapsulation of a supervisory component and its supervisee. Here, we extend our prior work on a revision-based logical modelling framework for such systems to incorporate programs within each component. We describe mechanisms for combining programs, possibly in different languages, from separate components and outline an operational semantics for programmed evolvable systems. We show how supervisory components extend run-time verifiers/monitors with capabilities for diagnosis and change. We illustrate the logical modelling using an example of an automated bank teller machine.

In [3], was introduced as a general purpose rule-based temporal logic for specifying run-time monitors. A novel and relatively efficient interpretative trace-checking scheme via stepwise transformation of an monitoring formula was defined and implemented. However, application in real-world examples has shown efficiency weaknesses, especially those associated with large-scale symbolic formula manipulation. In this paper, after briefly reviewing , we introduce , a primitive conditional rule-based system, which we claim can be more efficiently implemented for run-time checking, and into which one can compile various temporal logics used for run-time verification.