An overview of JML tools and applications

The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification typechecking, runtime debugging, static analysis, and verification.This paper gives an overview of the main ideas behind JML, details about JML’s wide range of tools, and a glimpse into existing applications of JML.     

Simulating the behavior of software modules by trace rewriting

The trace assertion method is a module interface specification method based on the finite state machine model. To support this method, we plan to develop a specification simulation tool, a trace simulator, that symbolically interprets trace assertions of trace specifications and simulates the externally observable behavior of the modules specified. We first present the trace assertion method. Then we formally define trace rewriting systems and show how trace rewriting, a technique similar to term rewriting, can be applied to implement trace simulation     

Checking JML specifications using an extensible software model checking framework

The use of assertions to express correctness properties of programs is growing in practice. Assertions provide a form of lightweight checkable specification that can be very effective in finding defects in programs and in guiding developers to the cause of a problem. A wide variety of assertion languages and associated validation techniques have been developed, but run-time monitoring is commonly thought to be the only practical solution. In this paper, we describe how specifications written in the Java Modeling Language (JML), a general purpose behavioral specification and assertional language for Java, can be validated using a customized model checker built on top of the Bogor model checking framework. Our experience illustrates the need for customized state-space representations and reduction strategies in model checking frameworks in order to effectively check the kind of strong behavioral specifications that can be written in JML. We discuss the advantages and tradeoffs of model checking relative to other specification validation techniques and present data that suggest that the cost of model checking strong specifications is practical for several real programs. This is an extended version of the paper Checking Strong Specifications Using An Extensible Model Checking Framework that appeared in Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004. This work was supported in part by the U.S. Army Research Office (DAAD190110564), by DARPA/IXO’s PCES program (AFRL Contract F33615-00-C-3044), by NSF (CCR-0306607) by Lockheed Martin, and by Rockwell-Collins.     

Observational purity and encapsulation

Practical specification languages for imperative and object-oriented programs, such as JML, Eiffel, and Spec#, allow the use of program expressions including method calls in specification formulas. For coherent semantics of specifications, and to avoid anomalies with runtime assertion checking, expressions in specifications and assertions are typically required to be weakly pure in the sense that their evaluation has no effect on the state of preexisting objects. For specification of large systems using standard libraries this restriction is impractical: it disallows many standard methods that mutate state for purposes such as caching or lazy initialization. Calls of such methods can sensibly be used for specifications and annotations in contexts where their effects cannot be observed. This paper formalizes a notion of observational purity, justifies the use of weakly and observationally pure methods in specifications, and shows that a method is observationally pure if it simulates a weakly pure method.     

Reusing a JML Specification Dedicated to Verification for Testing,and Vice-Versa: Case Studies

Testing and verification are two activities which have the same objective: to ensure software dependability. In the Java context, the Java Modelling Language (JML) has been proposed as specification language. It can be used both for verification and test. Usually, the JML specification is designed with a specific purpose: test or verification. This article addresses the question of reusability of a JML specification provided for one activity (resp. verification or test) in the other context (resp. test or verification). Two different case studies are considered.     

Model variables: cleanly supporting abstraction in design by contract

In design by contract (DBC), assertions are typically written using program variables and query methods. The lack of separation between program code and assertions is confusing, because readers do not know what code is intended for use in the program and what code is only intended for specification purposes. This lack of separation also creates a potential runtime performance penalty, even when runtime assertion checks are disabled, due to both the increased memory footprint of the program and the execution of code maintaining that part of the program's state intended for use in specifications. To solve these problems, we present a new way of writing and checking DBC assertions without directly referring to concrete program states, using ‘model’, i.e. specification‐only, variables and methods. The use of model variables and methods does not incur the problems mentioned above, but it also allow one to write more easily assertions that are abstract, concise, and independent of representation details, and hence more readable and maintainable. We implemented these features in the runtime assertion checker for the Java Modeling Language (JML), but the approach could also be implemented in other DBC tools. Copyright © 2005 John Wiley & Sons, Ltd.     

Method redefinition—ensuring alternative behaviors

The redefinition of a method in subclasses can completely change the semantics of the superclass method unless there are effective mechanisms that enforce the preservation of behavioral properties. Several approaches to behavioral subtyping—exact pre-post match, plug-in match, relaxed plug-in match among others—exist that enforce the preservation of behavioral properties.To maintain or weaken pre-conditions and to maintain or enforce post-conditions when redefining methods in extended classes—plug-in match—is the solution that is adopted, by construction, in the Eiffel language, among other assertion languages. This approach forbids the specification of a class of legitimate programs from which we present an example. We claim that relaxed plug-in match should be enforced instead, in order to accommodate these examples. Other approaches exist, as is the case of case analysis in JML and OCL, that allow the specification of those programs, but they do it at the cost of decreasing software extension.We propose a new way of building contracts that identify and express, in a natural and elegant way, the several contributions that method redefinition can bring, and that are expressive enough to specify extensible contracts for the above mentioned class of programs. These contracts ensure, by construction, that redefinition preserves behavioral properties.     

Integrating a formal method into a software engineering process with UML and Java

We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed reactive systems. To this end, we propose a specific UML profile for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by CSP_jassda, an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts. This research was partially supported by the DFG project ForMooS (grants OL 98/3-2 and WE 2290/5-1). C. B. Jones     

Measuring a Java Test Suite Coverage Using JML Specifications

We propose in this paper a way to measure the coverage of a Java test suite by considering the JML specification associed to the Java program under test. This approach is based on extracting a predicate-based graph from the JML method specifications. We then measure the coverage of this latter w.r.t. nodes of the graph that are visited by the test suite. In addition, we propose to check whether the test suite satisfies classical condition coverage criteria. We also introduce a tool, to be used as precompiler for Java, that is in charge of measuring and reporting the coverage according to these criteria.     

Interfaces for Refining Recursion and Procedures

This paper presents novel definitions of interfaced recursion blocks, interfaced procedures, and interfaced recursive procedures for the Refinement Calculus. These definitions allow step-wise refinement rules to be formally stated and proved for these constructs. An interface is associated with a (recursive) call by preceding the body of the implementation by an assertion statement which says that the interface refines to the implementation. An interface will typically be a specification statement, but in principle can be any command. The theory and rules presented in this paper have been mechanised in the theorem prover Isabelle/ZF. Received August 1999 / Accepted in revised form November 2000     

Modular specification of frame properties in JML

We present a modular specification technique for frame properties. The technique uses modifies clauses and abstract fields with declared dependencies. Modularity is guaranteed by a programming model that enforces data abstraction by preventing representation and argument exposure, a semantics of modifies clauses that uses a notion of ‘relevant location’, and by modularity rules for dependencies. For concreteness, we adapt this technique to the Java Modeling Language, JML. Copyright © 2003 John Wiley & Sons, Ltd.     

Monitoring Interfaces for Faults

We consider the problem of a module interacting with an external interface (environment) where the interaction is expected to satisfy some system specification Φ. While we have the full implementation details of the module, we are only given a partial external specification for the interface. The interface specification being partial (incomplete) means that the interface displays only a strict subset of the behaviors allowed by the interface specification.Based on the assumption that interface specifications are typically incomplete, we address the question of whether we can tighten the interface specification into a strategy, consistent with the given partial specification, that will guarantee that all possible interactions resulting from possible behaviors of the module will satisfy the system specification Φ. We refer to such a tighter specification as Φ-guaranteeing specification. Rather than verifying whether the interface, which is often an off-the-shelf component, satisfies the tighter specification, the paper proposes a construction of a run-time monitor which continuously checks the existence of a Φ-guaranteeing interface.We view the module and the external interface as players in a 2-player game. The interface has a winning strategy if it can guarantee that no matter what the module does, the overall specification Φ is met. The problem of incomplete specifications is resolved by allowing the interface to follow any strategy consistent with the interface specification. Our approach essentially combines traditional run-time monitoring and static analysis. This allows going beyond the focus of traditional run-time monitoring tools – error detection in the execution trace, towards the focus of the static analysis – bug detection in the programs.     

Foundations of the trace assertion method of module interfacespecification

The trace assertion method is a formal state machine based method for specifying module interfaces. A module interface specification treats the module as a black-box, identifying all the module's access programs (i.e., programs that can be invoked from outside of the module) and describing their externally visible effects. In the method, both the module states and the behaviors observed are fully described by traces built from access program invocations and their visible effects. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The stepwise refinement of trace assertion specifications is considered. The role of nondeterminism, normal and exceptional behavior, value functions, and multiobject modules are discussed. The relationship with algebraic specifications is analyzed. A tabular notation for writing trace specifications to ensure readability is adapted     

Specifying and checking method call sequences of Java programs

In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, referred to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules. We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and post-conditions and to specify them in a regular expression-like notation. The semantics of our extension is formally defined and provides a foundation for implementing runtime checks. Case studies have been performed to show the effectiveness our approach. We believe that our approach can be adopted by other BISLs.

A top-down methodology for microprocessor validation

A major challenge in today's functional verification is the lack of a formal specification with which to compare the RTL model. We propose a novel top-down verification approach that allows specification of a design above the RTL. From this specification, it is possible to automatically generate assertion models and RTL reference models. We also demonstrate that symbolic simulation and equivalence checking can be applied to verify an RTL design against its specification.     

Secure component composition with modular behavioral properties

We propose a flexible way of allowing the users of software components to specify their security policies, and endow digitally signed certificates with more expressive power at link time. Secure linking (SL) is more flexible than type-checking or other static checking mechanisms with endowing users the freedom to specify security policies at link time, and SL is more expressive than simple digital signing with restricting the scope of guarantees made by digitally signed certificates. SL would not prevent bugs in a software component, but it gives signers of software components finer-grain control of the meaning of their certificates. We implemented a logic-based framework for SL, which consists of the SL logic, a proof verifier, a tactical prover, and user interface languages. The framework of SL encompasses the existing constraint languages, such as OCL and JML, so the security policies and the property statements of software components can be written easily using those popular languages. In this paper, we explain the linking protocol of SL, the SL framework, and the extended user interface languages with OCL and JML. We also discuss the strength of the proposed linking protocol in developing practical software systems.     

一种组件化仿真模型(SCM-1)及其实现

火箭飞行仿真系统是一种复杂大系统;为降低系统开发的复杂度,相关专业仿真模型应具有较高水平的可重用性以及较低水平的建模复杂度,并且遵照统一的建模规范,提出了一种新的仿真组件模型(SCM-1),论述了该模型的输入/输出接口、控制接口和功能接口组成形式,设计了基于XML的模型描述规则和C语言标准代码框架,在此基础上研究了一系列该模型的通用支持工具,最后给出了某弹道模型的实例,实践表明该仿真模型建模规范能够有效提高火箭飞行仿真系统的效费比。     

Live sequence charts applied to hardware requirements specification and verification

Techniques and tools for formally verifying compliance with industry standards are important, especially in System-on-Chip (SoC) designs: a failure to integrate externally developed intellectual property (IP) cores is prohibitively costly. There are three essential components in the practical verification of compliance with a standard. First, an easy-to-read and yet formal specification of the standard is needed; we propose Live Sequence Charts (LSCs) as a high-level visual notation for writing specifications. Second, assertions should be generated directly from the specification; an implementation will be scrutinized, usually by model checking, to check that it satisfies each assertion. Third, a formal link must be made between proofs of assertions and compliance with the original specification. As an example, we take the Virtual Component Interface (VCI) Standard. We compare three efforts in verifying that the same register transfer level code is VCI-compliant. The first two efforts were manual, while the third used a tool, lscAssert, to automatically generate assertions in LTL. We discuss the details of the assertion generation algorithm.     

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.