Open Access. Powered by Scholars. Published by Universities.®

Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

University of Texas at El Paso

PDF

JML language

Publication Year

Articles 1 - 8 of 8

Full-Text Articles in Computer Engineering

Runtime Constraint Checking Approaches For Ocl, A Critical Comparison, Carmen Avila, Amritam Sarcar, Yoonsik Cheon, Cesar Yeep Feb 2010

Runtime Constraint Checking Approaches For Ocl, A Critical Comparison, Carmen Avila, Amritam Sarcar, Yoonsik Cheon, Cesar Yeep

Departmental Technical Reports (CS)

There are many benefits of checking design constraints at runtime---for example, automatic detection of design drift or corrosion. However, there is no comparative analysis of different approaches although such an analysis could provide a sound basis for determining the appropriateness of one approach over the others. In this paper we conduct a comparative analysis and evaluation of different constraint checking approaches possible for the Object Constraint Language (OCL). We compare several approaches including (1) direct translation to implementation languages, (2) use of executable assertion languages, and (3) use of aspect-oriented programming languages. Our comparison includes both quantitative metrics such as …


Integrating Random Testing With Constraints For Improved Efficiency And Diversity, Yoonsik Cheon, Antonio Cortes, Martine Ceberio, Gary T. Leavens Feb 2008

Integrating Random Testing With Constraints For Improved Efficiency And Diversity, Yoonsik Cheon, Antonio Cortes, Martine Ceberio, Gary T. Leavens

Departmental Technical Reports (CS)

Random testing can be fully automated, eliminates subjectiveness in constructing test cases, and increases the diversity of test data. However, randomly generated tests may not satisfy program's assumptions (e.g., method preconditions). While constraint solving can satisfy such assumptions, it does not necessarily generate diverse tests and is hard to apply to large programs. We blend these techniques by extending random testing with constraint solving, improving the efficiency of generating valid test data while preserving diversity. For domains such as objects, we generate input values randomly; however, for values of finite domains such as integers, we represent test data generation as …


A Fitness Function To Find Feasible Sequences Of Method Calls For Evolutionary Testing Of Object-Oriented Programs, Myoung Yee Kim, Yoonsik Cheon Nov 2007

A Fitness Function To Find Feasible Sequences Of Method Calls For Evolutionary Testing Of Object-Oriented Programs, Myoung Yee Kim, Yoonsik Cheon

Departmental Technical Reports (CS)

In evolutionary testing of an object-oriented program, the search objective is to find a sequence of method calls that can successfully produce a test object of an interesting state. This is challenging because not all call sequences are feasible; each call of a sequence has to meet the assumption of the called method. The effectiveness of an evolutionary testing thus depends in part on the quality of the so-called fitness function that determines the degree of the fitness of a candidate solution. In this paper, we propose a new fitness function based on assertions such as method preconditions to find …


A Quick Tutorial On Jet, Yoonsik Cheon Jun 2007

A Quick Tutorial On Jet, Yoonsik Cheon

Departmental Technical Reports (CS)

JET is an automated unit testing tool for Java classes annotated with JML specifications; JML is a formal interface specification language for Java to document the behavior of Java classes and interfaces. JET tests each method of the class under test separately. For each method, it generates a collection of test data, executes them, and decides test results (i.e., pass/fail) by using JML specifications as test oracles, thereby fully automating unit testing of Java classes. This document gives a quick tutorial introduction to JET.


Abstraction In Assertion-Based Test Oracles, Yoonsik Cheon Jun 2007

Abstraction In Assertion-Based Test Oracles, Yoonsik Cheon

Departmental Technical Reports (CS)

Assertions can be used as test oracles. However, writing effective assertions of right abstraction levels is difficult because on the one hand, detailed assertions are preferred for through testing (i.e., to detect as many errors as possible), but on the other hand abstract assertions are preferred for readability, maintainability, and reusability. As assertions become a practical tool for testing and debugging programs, this is an important and practical problem to solve for the effective use of assertions. We advocate the use of model variables---specification-only variables of which abstract values are given as mappings from concrete program states---to write abstract assertions …


Random Test Data Generation For Java Classes Annotated With Jml Specifications, Yoonsik Cheon, Carlos E. Rubio-Medrano Mar 2007

Random Test Data Generation For Java Classes Annotated With Jml Specifications, Yoonsik Cheon, Carlos E. Rubio-Medrano

Departmental Technical Reports (CS)

The hidden states of objects create a barrier to designing and generating test data automatically. For example, the state of an object has to be established indirectly through a sequence of method invocations. For a non-trivial class, however, it is extremely unlikely that a randomly-chosen sequence of method invocations can construct an object successfully, as each invocation has to satisfy the state invariants. Nonetheless, automated random testing can reduce the cost of testing dramatically and has potential for finding errors that are difficult to find in other ways because it eliminates the subjectiveness in constructing test data. We propose a …


Automated Random Testing To Detect Specification-Code Inconsistencies, Yoonsik Cheon Jan 2007

Automated Random Testing To Detect Specification-Code Inconsistencies, Yoonsik Cheon

Departmental Technical Reports (CS)

An interface specification language such as JML provides a means to document precisely the behavior of program modules such as Java classes, and it is being adopted by industry. However, few practical tools exist for programmers to assure the correctness of their interface specifications. Nonetheless, the correctness of an interface specification is a prerequisite for the use of the specification, both as a precise API documentation and as a foundation for formal verification of and reasoning about the implementation. We propose automated random testing as a practical tool to assure the correctness of interface specifications. The key idea of our …


A Formal Specification In Jml Of The Java Security Package, Poonam Agarwal, Carlos E. Rubio-Medrano, Yoonsik Cheon, Patricia J. Teller Apr 2006

A Formal Specification In Jml Of The Java Security Package, Poonam Agarwal, Carlos E. Rubio-Medrano, Yoonsik Cheon, Patricia J. Teller

Departmental Technical Reports (CS)

The Java security package allows a programmer to add security features to Java applications. Although the package provides a complex application programming interface (API), its informal description, e.g., Javadoc comments, is often ambiguous or imprecise. Nonetheless, the security of an application can be compromised if the package is used without a concrete understanding of the precise behavior of the API classes and interfaces, which can be attained via formal specification. In this paper, we present our experiences in formally specifying the Java security package in JML, a formal behavior interface specification language for Java. We illustrate portions of our JML …