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

Pre and postconditions

Articles 1 - 11 of 11

Full-Text Articles in Computer Engineering

Access Control Contracts For Java Program Modules, Carlos E. Rubio-Medrano, Yoonsik Cheon Apr 2010

Access Control Contracts For Java Program Modules, Carlos E. Rubio-Medrano, Yoonsik Cheon

Departmental Technical Reports (CS)

Application-level security has become an issue in recent years; for example, errors, discrepancies and omissions in the specification of access control constraints of security-sensitive software components are recognized as an important source for security vulnerabilities. We propose to formally specify access control assumptions or constraints of a program module and enforce them at run-time. We call such specifications access control contracts. To realize access control contracts, we extended the JML language, a formal interface specification language for Java, and developed a prototype support tool that translates access control contracts to runtime checks. The access control contract reduces the vulnerability that …


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 …


Checking Design Constraints At Run-Time Using Ocl And Aspectj, Yoonsik Cheon, Carmen Avila, Steve Roach, Cuauhtemoc Munoz Dec 2009

Checking Design Constraints At Run-Time Using Ocl And Aspectj, Yoonsik Cheon, Carmen Avila, Steve Roach, Cuauhtemoc Munoz

Departmental Technical Reports (CS)

Design decisions and constraints of a software system can be specified precisely using a formal notation such as the Object Constraint Language (OCL). However, they are not executable, and assuring the conformance of an implementation to its design is hard. The inability of expressing design constraints in an implementation and checking them at runtime invites, among others, the problem of design drift and corrosion. We propose runtime checks as a solution to mitigate this problem. The key idea of our approach is to translate design constraints written in a formal notation such as OCL into aspects that, when applied to …


Automating Java Program Testing Using Ocl And Aspectj, Yoonsik Cheon, Carmen Avila Oct 2009

Automating Java Program Testing Using Ocl And Aspectj, Yoonsik Cheon, Carmen Avila

Departmental Technical Reports (CS)

Random testing can eliminate subjectiveness in constructing test data and increase the diversity of test data. However, one difficult problem is to construct test oracles that decide test results---test failures or successes. Assertions can be used as test oracles and are most effective when derived from formal specifications such as OCL constraints. If fully automated, random testing can reduce the cost of testing dramatically. In this paper we propose an approach for automating Java program testing by combining random testing and OCL. The key idea of our approach is to use OCL constraints as test oracles by translating them to …


An Aspect-Based Approach To Checking Design Constraints At Run-Time, Yoonsik Cheon, Carmen Avila, Steve Roach, Cuauhtemoc Munoz, Neith Estrada, Valeria Fierro, Jessica Romo Nov 2008

An Aspect-Based Approach To Checking Design Constraints At Run-Time, Yoonsik Cheon, Carmen Avila, Steve Roach, Cuauhtemoc Munoz, Neith Estrada, Valeria Fierro, Jessica Romo

Departmental Technical Reports (CS)

Design decisions and constraints of a software system can be specified precisely using a formal notation such as the Object Constraint Language (OCL). However, they are not executable, and assuring the conformance of an implementation to its design is hard. The inability of expressing design constraints in an implementation and checking them at runtime invites, among others, the problem of design drift and corrosion. We propose runtime checks as a solution to mitigate this problem. The key idea of our approach is to translate design constraints written in a formal notation such as OCL into aspects that, when applied to …


A Library-Based Approach To Translating Ocl Constraints To Jml Assertions For Runtime Checking, Carmen Avila, Guillermo Flores, Jr., Yoonsik Cheon Feb 2008

A Library-Based Approach To Translating Ocl Constraints To Jml Assertions For Runtime Checking, Carmen Avila, Guillermo Flores, Jr., Yoonsik Cheon

Departmental Technical Reports (CS)

OCL is a formal notation to specify constraints on UML models that cannot otherwise be expressed by diagrammatic notations such as class diagrams. Using OCL one can document detailed design decisions and choices along with the behavior, e.g., class invariants and method pre and postconditions. However, OCL constraints cannot be directly executed and checked at runtime by an implementation, thus constraint violations may not be detected or noticed, causing many potential development and maintenance problems. In this paper we propose an approach to checking OCL constraints at runtime by translating them to executable JML assertions. The key components of our …


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 …


Specifying And Checking Method Call Sequences Of Java Programs, Yoonsik Cheon, Ashaveena Perumandla Nov 2005

Specifying And Checking Method Call Sequences Of Java Programs, Yoonsik Cheon, Ashaveena Perumandla

Departmental Technical Reports (CS)

In a pre and postconditions-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 …