O. Mondragon Receives Best Dissertation Award for an Interval-Related Dissertation

On April 10, 2005, The University of Texas at El Paso has informed Oscar Mondragon that he has received a University Outstanding Dissertation Award for his interval-related 2004 Ph.D. dissertation "Elucidation and Specification of Software Properties through Patterns and Composite Propositions to Support Formal Verification Techniques".

One of the main problems of software engineering is to verify that the software satisfies the given specifications. Traditionally, in software industry, the new software is tested on several different situations. Usually, there are so many possible situations that it is absolutely unrealistic to test the software on all of them, so, instead of testing the software on all possible situations, practitioners test software on selected situations, selected inputs that they believe to be representative. It is well known that even after the most thorough testing on such seemingly representative situations, most software package and systems retain errors. The resulting software errors (bugs, faults, etc.) lead to large losses of time and productivity, and even sometimes - to catastrophic events with loss of life. Software problems are especially important for time critical real-time systems where the software is used to make decisions that need to be made within given time.

In view of this situation, one of the main objectives of software engineering is to develop formal verification techniques - techniques that would guarantee that the software works correctly on all possible situations, not just on the few selected situations on which this software was actually tested.

In general, program verification is a computationally difficult task; it is known that no algorithm is possible for solving the general program verification problem. It is therefore desirable to find particular cases of program verification that would be general enough but still allow algorithmic solutions. There exist many interesting directions in developing efficient formal verification techniques, among them the direction related to the use of interval logics.

The main idea behind interval logics is that, crudely speaking, if we want to guarantee that a certain property occurs for all possible values within a given interval, then, instead of testing this property for finite set of "representative" values from this interval (and risking that we miss the values on which the tested property does not hold), we perform all the operations with the entire interval, thus guaranteeing that this property is indeed true for all the values within this interval. In general, the interval approaches to program verification still leads to algorithmically unsolvable problems. However, several efficient formal methods have been developed, including Future Interval Logic (FIL), an approach championed by the Real Time Systems Group (RTSG) at the University of Pennsylvania, one of the world leading centers in formal verification techniques.

The FIL approach has several interesting applications, but it is not yet widely used in the software engineering community, for two reasons:

first, the existing FIL formalism only captures a few simplest properties of software -- although there are examples that several more complex properties of a program can also be described in FIL and thus tested;
second, while in principle, there are algorithms for testing FIL properties, these algorithms are more of academic nature in the sense that they have not been implemented in an easy-to-use way.

These two problems were the two challenges that Oscar Mondragon handled in his dissertation. As a result:

first, he drastically expanded the original FIL logic so that it now includes a large number of important software properties -- while not increasing the computationally complexity of verifying these properties;
second, he developed a user-friendly way of using FIL to verify programs: namely, he has developed a new language that enables the user to use traditional software engineering terms, and develop an efficient translation from this language into FIL; he also helped the RTSG group to enhanced the translation from the FIL specifications into Meta Event Definition Language (MEDL), the property specification language of the Monitoring and Checking system.

In the process of developing his tools, Oscar also applied his software verification skills to testing the originally proposed FIL-related tools, and uncovered (and helped correct) several bugs in these well-used tools.

At present, Oscar applies his expertise as a research with the Mexico-based International Software Institute in Guadalajara.

APPENDIX
Publications of Oscar Mondragon related to his dissertation:

JOURNAL PUBLICATIONS

1. O. Mondragon, A. Q. Gates, and S. Roach, "Prospec: Support for Elicitation and Formal Specification of Software Properties," in O. Sokolsky and M. Viswanathan (Eds. of the special issue), Electronic Notes on Theoretical Computer Science 89(2), 2004.

2. O. Mondragon and A. Q. Gates, "Supporting Elicitation and Specification of Software Properties through Patterns and Composite Propositions," Intl. Journal of Software Engineering and Knowledge Engineering, 14(1), Feb. 2004.

3. A. Q. Gates and O. Mondragon, "FasTLInC: A Constraint-based Tracing Approach," The Journal of Systems and Software, 63, 2002, 241-258.

4. A. Q. Gates, S. Roach, O. Mondragon, and N. Delgado, "DynaMICs: Comprehensive Support for Run-Time Monitoring", in Electronic Notes in Theoretical Computer Science, K. Havelund and G. Rosu (eds.), 55(2), 2001, http://www.elsevier.nl/locate/entc

PAPERS IN REFEREED CONFERENCE PROCEEDINGS

1. A. Q. Gates, O. Mondragon, and F. Kassem, "Automated Support for Property Specification Based on Patterns", Proceedings of the 15th International Conference on Software Engineering and Knowledge Engineering, July 2003, pp. 174-181.

2. A. Q. Gates, O. Mondragon, M. Payne, and S. Roach, "Instrumentation of Intermediate Code for Runtime Verification", Proceedings 28th Annual NASA Goddard/IEEE Software Engineering Workshop, December 2003.

3. O. Mondragon, A. Q. Gates, and S. Roach, "Composite Propositions: Toward Support for Formal Specification of System Properties", Proceedings 27th Annual NASA Goddard/IEEE Software Engineering Workshop, December 2002, pp. 67-74.

4. A. Q. Gates, O. Mondragon, F. Saenz, and R. Cereceres, "The Use of Integrity Constraints to Support Tracing", Proceedings of Software Engineering and Knowledge Engineering Conference, June 2000, 195-204.

5. A. Q. Gates, N. Delgado, and O. Mondragon, "A Structured Approach for Managing a Practical Software Engineering Course", Proceedings 2000 Frontiers in Education Conference, Kansas City, Mo., 2000.

[<--] Back to Honors Received by Interval Researchers

[<--] Back to the main menu of the Interval Computations website