AN INTERMEDIATE LANGUAGE FOR FORMAL VERIFICATION TOOLS

Award Information
Agency:
National Aeronautics and Space Administration
Amount:
$47,983.00
Program:
SBIR
Contract:
N/A
Solitcitation Year:
N/A
Solicitation Number:
N/A
Branch:
N/A
Award Year:
1991
Phase:
Phase I
Agency Tracking Number:
16962
Solicitation Topic Code:
N/A
Small Business Information
Odyssey Research Assoc Inc
301a Harris B Dates Dr, Ithaca, NY, 14850
Hubzone Owned:
N
Woman Owned:
N
Socially and Economically Disadvantaged:
N
Duns:
N/A
Principal Investigator
 () -
Business Contact
Phone: () -
Research Institution
N/A
Abstract
THIS PROJECT WILL INVESTIGATE AN INTERMEDIATE FORMAL LANGUAGE FOR INTEGRATING FORMAL VERIFICATION TOOLS. SUCH A LANGUAGE WOULD ALLOW DIFFERENT TOOLS SUCH AS THEOREM PROVERS, DECISION PROCEDURES, AND FORMULA GENERATORS TO BE USED IN THE SAME ENVIRONMENT, EITHER BY TRANSLATING THE VARIOUS TOOLS' FORMAL LANGUAGES INTO THE INTERMEDIATE LANGUAGE AND BACK OR BY USING THE INTERMEDIATE LANGUAGE AS AN INTERNAL FORM SHARED BETWEEN TOOLS. THE ABILITY TO INTEGRATE DIFFERENT VERIFICATION TOOLS WILL SIGNIFICANTLY ENHANCE THE UTILITY OF FORMAL VERIFICATION IN DEVELOPING RELIABLE SOFTWARE. THE PROJECT OBJECTIVES ARE TO FORMULATE A CANDIDATE INTERMEDIATE FORMAL LANGUAGE AND TO DEFINE TRANSLATION ALGORITHMS AMONG THE INTERMEDIATE LANGUAGE AND THE TWO EXISTING FORMAL LANGUAGES FROM DIFFERENT FORMAL VERIFICATION ENVIRONMENTS. THE APPROACH WILL BE TO EXAMINE A COLLECTION OF FORMAL LANGUAGES FROM EXISTING FORMAL VERIFICATION ENVIRONMENTS AND TO FORMULATE A CANDIDATE INTERMEDIATE LANGUAGE EXPRESSIVE ENOUGH TO TRANSLATE THE EXISTING LANGUAGES INTO. IT WILL THEN CHOOSE TWO EXISTING LANGUAGES FROM DIFFERENT ENVIRONMENTS AND DEFINE ALGORITHMS TO TRANSLATE THE INTO THE INTERMEDIATE LANGUAGE, AND BACK. THIS WILL DEMONSTRATE THE FEASIBILITY OF THE INTERMEDIATE LANGUAGE FOR CONNECTING DIFFERENT ENVIRONMENTS AND DEFINE ALGORITHMS TO TRANSLATE THEM INTO THE INTERMEDIATE LANGUAGE, AND BACK. THIS WILL DEMONSTRATE THE FEASIBILITY OF THE INTERMEDIATE LANGUAGE FOR CONNECTING DIFFERENT TOOLS. THE RESULTS WILL BE A CANDIDATE INTERMEDIATE LANGUAGE AND THE TRANSLATION ALGORITHMS. THIS PROJECT WILL INVESTIGATE AN INTERMEDIATE FORMAL LANGUAGE FOR INTEGRATING FORMAL VERIFICATION TOOLS. SUCH A LANGUAGE WOULD ALLOW DIFFERENT TOOLS SUCH AS THEOREM PROVERS, DECISION PROCEDURES, AND FORMULA GENERATORS TO BE USED IN THE SAME ENVIRONMENT, EITHER BY TRANSLATING THE VARIOUS TOOLS' FORMAL LANGUAGES INTO THE INTERMEDIATE LANGUAGE AND BACK OR BY USING THE INTERMEDIATE LANGUAGE AS AN INTERNAL FORM SHARED BETWEEN TOOLS. THE ABILITY TO INTEGRATE DIFFERENT VERIFICATION TOOLS WILL SIGNIFICANTLY ENHANCE THE UTILITY OF FORMAL VERIFICATION IN DEVELOPING RELIABLE SOFTWARE. THE PROJECT OBJECTIVES ARE TO FORMULATE A CANDIDATE INTERMEDIATE FORMAL LANGUAGE AND TO DEFINE TRANSLATION ALGORITHMS AMONG THE INTERMEDIATE LANGUAGE AND THE TWO EXISTING FORMAL LANGUAGES FROM DIFFERENT FORMAL VERIFICATION ENVIRONMENTS. THE APPROACH WILL BE TO EXAMINE A COLLECTION OF FORMAL LANGUAGES FROM EXISTING FORMAL VERIFICATION ENVIRONMENTS AND TO FORMULATE A CANDIDATE INTERMEDIATE LANGUAGE EXPRESSIVE ENOUGH TO TRANSLATE THE EXISTING LANGUAGES INTO. IT WILL THEN CHOOSE TWO EXISTING LANGUAGES FROM DIFFERENT ENVIRONMENTS AND DEFINE ALGORITHMS TO TRANSLATE THE INTO THE INTERMEDIATE LANGUAGE, AND BACK. THIS WILL DEMONSTRATE THE FEASIBILITY OF THE INTERMEDIATE LANGUAGE FOR CONNECTING DIFFERENT ENVIRONMENTS AND DEFINE ALGORITHMS TO TRANSLATE THEM INTO THE INTERMEDIATE LANGUAGE, AND BACK. THIS WILL DEMONSTRATE THE FEASIBILITY OF THE INTERMEDIATE LANGUAGE FOR CONNECTING DIFFERENT TOOLS. THE RESULTS WILL BE A CANDIDATE INTERMEDIATE LANGUAGE AND THE TRANSLATION ALGORITHMS.

* information listed above is at the time of submission.

Agency Micro-sites

US Flag An Official Website of the United States Government