Temporal Verification and Development of Reactive Programs
{'Code': '05010400', 'Directorate': {'Abbreviation': 'CSE', 'LongName': 'Direct For Computer & Info Scie & Enginr'}, 'Division': {'Abbreviation': 'CCF', 'LongName': 'Division of Computing and Communication Foundations'}}
{'SignBlockName': 'name not available', 'PO_EMAI': None, 'PO_PHON': None}
Temporal logic is a useful, powerful formalism for the                          specification,analysis, and development of a large class of systems,            reactive systems.  This class of systems includes concurrent and real-          time programs, process control and embedded programs, hardware devices,         and other systems whose role is to maintain a continuous interaction            with their environment.                                                                                                                                         Promising applications of temporal logic have been reported in diverse          areas such as the design and verification of communication protocols,           hardware design and analysis, synthesis of concurrent programs, and             database analysis.                                                              This research is aimed at making the temporal formalism into a                  practical tool. The primary goals are to establish a uniform temporal-          logic methodology for the specification, verification, development, and         automatic synthesis of reactive systems, and to construct an                    experimental system that will provide computerized support for these            activities.                                                                                                                                                     To attain these goals the investigation includes: the expressive power          and convenience of specification by temporal logic, and its possible            improvements by extensions such as past operators and quantification            over state-variables; Combination of temporal logic with transition             systems, such as automata; Compositionality of temporal specifications          as a basis for systematic development by decomposition and refinement.
{'FirstName': 'Zohar', 'LastName': 'Manna', 'PI_MID_INIT': None, 'PI_SUFX_NAME': None, 'PI_FULL_NAME': 'Zohar Manna', 'EmailAddress': 'zm@cs.stanford.edu', 'NSF_ID': '000215203', 'StartDate': '09/01/1988', 'EndDate': None, 'RoleCode': 'Principal Investigator'}
{'Name': 'Stanford University', 'CityName': 'STANFORD', 'ZipCode': '943052004', 'PhoneNumber': '6507232300', 'StreetAddress': '450 JANE STANFORD WAY', 'StreetAddress2': None, 'CountryName': 'United States', 'StateName': 'California', 'StateCode': 'CA', 'CONGRESSDISTRICT': '16', 'CONGRESS_DISTRICT_ORG': 'CA16', 'ORG_UEI_NUM': 'HJD6G4D6TJY5', 'ORG_LGL_BUS_NAME': 'THE LELAND STANFORD JUNIOR UNIVERSITY', 'ORG_PRNT_UEI_NUM': None}
{'Name': None, 'CityName': None, 'StateCode': None, 'ZipCode': None, 'StreetAddress': None, 'CountryCode': None, 'CountryName': None, 'StateName': None, 'CountryFlag': None, 'CONGRESSDISTRICT': None, 'CONGRESS_DISTRICT_PERF': '""'}
{'Code': '2875', 'Text': 'SYSTEM SOFTWARE'}
{'url': 'https://www.nsf.gov/awardsearch/download?DownloadFileName=1988&All=true', 'xml': '8812595.xml'}