Overview

Introduction

The Common Aspect Proof Environment (CAPE) is an extensible environment for different aspect verification and analysis tools and over various aspect languages. It is being developed as one of the primary tasks of the Formal Methods Laboratory of AOSD-Europe. The design and implementation is mainly being done at the Technion, with tools contributed from the Technion and from other AOSD-Europe sites, and in particular INRIA, Twente and Lancaster. The tools in the environment will be usable in various predefined proof strategies that combine those tools' abilities by sharing their resources and outputs and dividing proof responsibilities among the different tools, according to the strengths of each tool. The CAPE proof environment is intended both for those who wish to apply the tools to aspect programs written in a variety of languages, and for those developing new verification or analysis tools for aspects.

Tools in the CAPE

Use of the CAPE assumes an Eclipse environment where the usual AspectJ compiler and the AspectJ Development Toolkit (AJDT) plugins are installed.

Three well-known model-checking tools--Java Pathfinder, NuSMV, and Cadence SMV, all available as open source, are integrated into the CAPE, but need to be separately downloaded from their own websites, and installed using instructions provided on the CAPE webpages. These tools all treat either Java bytecode (for Java Pathfinder) or models in SMV's input language (for NuSMV and Cadence SMV). They were not designed for use particularly with aspect systems, but are either used as part of the analysis of one of the aspect-specific tools below, or can be used to model check woven systems or models.

Two additional general-purpose analysis tools are also integrated into the CAPE and are provided as part of the downloads available from the CAPE website (since they are less generally available than the others):

Thus, overall, there are five foundational tools integrated to the CAPE, in addition to the compilers and the AJDT development tools.

The more specific tools that analyze aspect systems, are integrated into the CAPE, and can be downloaded from the website include:

  • MAVEN, a model analyzer that can prove that individual aspects are correct relative to their specifications. This means that whenever such an aspect is woven to a system that satisfies the assumption of the aspect, the resultant woven system will satisfy the guarantee of the aspect, where both the assumption and the guarantee are given as linear temporal logic assertions
  • CNVA, a scenario-based tool to check that every execution sequence in a woven system is equivalent to one where aspect advice is done atomically immediately from states that are joinpoints
  • The AIDA tool for detecting interactions between AspectJ aspects using data flow techniques
  • The Aspect Introductions Analyzer (AIA) uses the GROOVE graph rewriting toolkit to detect syntactic name and other conflicts between AspectJ introductions.
  • SECRET, a syntactic tool to detect conflicts in parameters of aspects (that originates in the Composition Filters compiler suite)
  • the GRASS tool, also based on GROOVE, analyzes Compose* composition filters to detect whether the order of application of aspects (filters) with common joinpoints is significant.

It should be noted that the CAPE implementation of the last two tools in the list above is temporarily suspended because the Compose* compiler on which they depend has recently been reimplemented, requiring adjustments in the implementation of these tools. These tools should soon be available in the CAPE.

GAR (Generic Aspect Representation)

An important component of the CAPE is the GAR - a central repository that holds the source code of an application together with the models and verification artifacts that are used to analyze the application.

The CAPE is implemented on top of the Eclipse platform and the GAR is implemented on top of the Eclipse resource management platform. Therefore, we first provide a brief overview of the Eclipse resource management platform and then describe how the GAR is implemented.

The basic unit of organization in Eclipse is a project. Each project consists of a collection of files and directories. In addition, each project has one or more natures. A nature defines the type of the project and associates to the project a builder. For example to develop a Java application we may create a project with a Java nature. This associates a Java compiler as the builder of the project. Whenever we select the build action from the menu the Java compiler takes all the Java source files in the project and compiles them.

A single project, however, is homogeneous. You can create a Java project or say a Ruby project, but you cannot have both Ruby and Java source code in the same project. However many applications today are built using more than one language. In order to support such applications we can collect several projects into a working set.

For example a web application may have some parts written in Java, others may be in Java-script or Ruby and so on. We usually create a project for each language - a project with a Java nature for the Java code, a project with a Ruby nature for the Ruby code and so on. We may then create a working set to hold the individual projects of the entire application.

Another important property of Eclipse projects is that they can refer to the same files and directories using linked resources. A linked resource is similar to a symbolic link in UNIX. This makes it possible to create some projects as views of other projects by making the files in the view projects link to the files in the other projects.

The CAPE GAR is implemented as an Eclipse working set. A typical CAPE GAR consists of one or more projects that hold the source code of the application and one or more analysis projects that either hold abstract models of the application, or use linked resources to select the parts of the source code that are relevant for analysis. For example, to perform data flow analysis using the Aida tool we create an Aida project (that is a project whose nature is Aida) and populate it with links to the source files that we would like to analyze. When we build the project the Aida tool (the Aida tool is the builder of the project) compiles the files in the project and produces a graph that is added to the project's output directory.

Tool Types

The tools introduced into the CAPE are divided into the categories Verifiers, Translators and Editors. Verifiers analyze their input and provide the user with a viewable result of the analysis process. e.g. Model checkers, data flow analyzers etc. They are implemented over Eclipse's launching mechanism, which allows the user to "debug" his/her input files with a verifier much like any other debugger in Eclipse.

Translators translate (or compile) their input into an output that other tools may use. e.g. Graph production System generators, finite state machine builders, compilers etc. They are implemented as builders, and are used as mentioned in the section above about the GAR.

Editors, like their name suggests, modify their own input files and are implemented as either built-in or external Eclipse editors.

In addition to these methods of usage, the CAPE provides a centralized location where the user can browse and operate the available tools.

Automatic vs Manual analysis

The Build Automatically flag in the Project menu directs Eclipse to automatically rebuild your projects every time they change. Alternatively you can disable this flag if you decide to manually build your projects. Automatic build is very convenient but it requires a quick builder. Therefore if you find that your analysis tool is taking a lot of time to perform the analysis it may be better to disable the automatic build support and use the manual option.

A formal model of the CAPE

We have originaly created a set of Z models of the CAPE in order to provide a description that is more precise than the existing natural language specification, but does not require one to delve into the details of the implementation. However, during the development of the models we found that the existing specification had many details that were either not clear or entirely missing. In such cases we have added the missing parts to the Z models. As a result the role of the models changed from being a precise documentation of the existing system into that of a guide or blueprint of how the CAPE should really look.

 

 

You are visitor number: