Introduction

Why have we defined our own specification language? Within the context of the Bandera project, another option would be to have developers express requirements in the specification language of one of the underlying model-checkers (e.g., in Spin's Linear Temporal Logic (LTL) specification language, or Computational Tree Logic (CTL) of NuSMV). This has several disadvantages.

1. Although temporal logics such as LTL and CTL are theoretically elegant, practitioners and even researchers sometimes find it difficult to use them to accurately express the complex state and event sequencing properties often required of software. Once written, these specifications are often hard to reason about, debug, and modify.
2. In the Bandera project, following this option forces the analyst to commit to the notation of a particular model-checker back-end. If more than one checker is to be used, the specifications may have to be recoded in a different language (e.g., switching from LTL to CTL), and then perhaps simultaneously modified if the requirement is modified.
3. This option is also problematic because it forces the specification to be stated in terms of the model's representation of program features such as control-points, local and instance variables, array access, nested object dereferences as rendered, e.g., in Promela, instead of in terms of the source code itself. Thus, the user must understand these typically highly optimized representations to accurately render the specifications. This is somewhat analogous to asking a programmer to state assertions in terms of the compiler's intermediate representation. Moreover, the representations may change depending on which optimizations were used when generating the model. Even greater challenges arise when modeling the dynamism found in typical object-oriented software: components corresponding to dynamically created objects/threads are dynamically added to the state-space during execution. These components are anonymous in the sense that they are often not bound directly to variables appearing in the source program. The lack of fixed source-level component names makes it difficult to write specifications describing dynamic component properties: such properties have to be expressed in terms of the model's representation of the heap.
4. Finally, depending on what form of abstraction is used, the specifications would have to be modified to reference abstractions of source code features instead of the source code features themselves.

In this section, we describe the design and implementation of the Bandera Specification Language (BSL) -- a source-level, model-checker independent language for expressing temporal properties of Java program actions and data. BSL addresses the problems outlined above and provides support for overcoming the hurdles one faces when specifying properties of dynamically evolving software. For example, consider a property of the bounded buffer implementation from the previous section that states that if a buffer is full, it will eventually become non-full. There are several challenges in rendering this specification in a form that can be model-checked including

• defining the meaning of full in the implementation,
• quantifying over time to insure that full buffers eventually become non-full, and
• quantifying over all dynamically created bounded buffers instances in the program.

  
Figure 16: BSL organization

BSL separates these issues and treats them with special purpose sub-languages as indicated in Figure 16.

• An assertion sublanguage allows developers to define constraints on program contexts in familiar assertion-style notation. Assertions can be selectively enabled/disabled so that one can easily identify only a subset of assertions for checking. Bandera exploits this capability by optimizing the generated models (using slicing and abstraction) specifically for the selected assertions.
• A temporal property sublanguage provides support for defining predicates on common Java control points (e.g., method invocation and return) and Java data (including dynamically created threads and objects). These predicates become the basic propositions in temporal specifications. The temporal specification language is based not on a particular temporal logic, but on a collection of field-tested temporal specification patterns developed in our earlier work [7]. This pattern language is extensible and allows for libraries of domain-specific patterns to be created.

  Interacting with both the predicate and pattern support in BSL is a powerful quantification facility that allows temporal specifications to be quantified over all objects/threads from particular classes. Quantification provides a mechanism for naming potentially anonymous data, and we have found this type of support to be crucial for expressive reasoning about dynamically created objects.

Assertions and predicates are included in the source code as Javadoc comments. This allows for HTML-based documentation to easily be extracted and browsed by developers, and for special purpose doclet-processing to provide a rich tool-based infra-structure for for writing specifications.

Even though BSL is based on Java, and, to some extent is driven by the desire to abstract away from the collection of model-checker back-ends found in Bandera, we believe that the general ideas embodied in this language will be useful in any environment for model-checking software source code.

The rest of the BSL overview is organized as follows. Section 6.2 discusses some of the salient issues that influenced our design of the language. Section 6.3 describes the design and implementation of the assertion sublanguage. Section 6.4 describes the design and implementation of the temporal specification sublanguage.