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:
At present, Oscar applies his expertise as a research with the Mexico-based International Software Institute in Guadalajara.
Publications of Oscar Mondragon related to his dissertation:
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