USA flag logo/image

An Official Website of the United States Government

AN INTERMEDIATE LANGUAGE FOR FORMAL VERIFICATION TOOLS

Award Information

Agency:
National Aeronautics and Space Administration 		Branch:
N/A 		Award ID:
16962 		Program Year/Program:
1991 / SBIR
Agency Tracking Number:
16962 		Solicitation Year:
N/A 		Solicitation Topic Code:
N/A 		Solicitation Number:
N/A
Small Business Information
ATC - NY
33 Thornwood Drive Suite 500 Ithaca, NY -
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 1
Fiscal Year: 1991
Title: AN INTERMEDIATE LANGUAGE FOR FORMAL VERIFICATION TOOLS
Agency: NASA
Contract: N/A
Award Amount: $47,983.00
 

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.

Principal Investigator:


0

Business Contact:

Small Business Information at Submission:

Odyssey Research Assoc Inc
301a Harris B Dates Dr Ithaca, NY 14850

EIN/Tax ID: 161549760
DUNS: N/A
Number of Employees: N/A
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No