MONITOR SYNTHESIS FOR SOFTWARE HEALTH MANAGEMENT 1.0 INTRODUCTION/BACKGROUND: AVIONICS SYSTEMS, SUCH AS GUI…

Public award description

MONITOR SYNTHESIS FOR SOFTWARE HEALTH MANAGEMENT 1.0 INTRODUCTION/BACKGROUND: AVIONICS SYSTEMS, SUCH AS GUIDANCE, NAVIGATION, AND CONTROL (GNC) SYSTEMS, ARE INHERENTLY DISTRIBUTED, REAL-TIME SYSTEMS. THE CORRECTNESS OF A GNC SYSTEM IS A GLOBAL PROPERTY OF THE SYSTEM DEPENDENT UPON THE LOCAL SUBSYSTEMS COORDINATING CORRECTLY (EVEN IN THE PRESENCE OF HARDWARE FAULTS). A MEANS TO PRODUCE THE STRONGEST EVIDENCE POSSIBLE FOR THE CORRECTNESS FOR A DISTRIBUTED REAL-TIME SYSTEM IS TO FORMALLY SPECIFY IN SOME SPECIFICATION LANGUAGE ITS GLOBAL REQUIREMENTS AND THEN FORMALLY REFINE THE REQUIREMENTS INTO A CORRECTNESS-PRESERVING IMPLEMENTATION. UNFORTUNATELY, SUCH AN APPROACH IS INFEASIBLE FOR ALL BUT THE SIMPLEST PROTOTYPE SYSTEMS. SINCE FORMALIZING THE ENTIRE SYSTEMS DEVELOPMENT PROCESS IS INFEASIBLE, ROUGHLY TWO APPROACHES ARE TAKEN. ONE APPROACH IS TO FORMALIZE A HIGH-LEVEL MODEL OF THE SYSTEM AND THEN VERIFY THAT IT SATISFIES REQUIREMENTS OF THE SYSTEM. BECAUSE A HIGH-LEVEL MODEL IS USED, MATHEMATICALLY PROVING THAT THE MODEL SATISFIES THE SYSTEM REQUIREMENTS BECOMES FEASIBLE. ANOTHER APPROACH IS TO WORK WITH THE ACTUAL IMPLEMENTATION RATHER THAN AN ABSTRACT SYSTEM-LEVEL MODEL. CODE-LEVEL VERIFICATION AND VALIDATION RESEARCH SUCH AS RUNTIME MONITORING, STATIC ANALYSIS, AND MODEL-BASED DEVELOPMENT LARGELY TAKES THIS APPROACH. THE ADVANTAGE OF THIS APPROACH IS THAT IT VALIDATES THE ACTUAL IMPLEMENTATION. THE WEAKNESS, HOWEVER, IS THAT AT THE IMPLEMENTATION LEVEL, IT IS DIFFICULT TO CHECK GLOBAL PROPERTIES. FOR EXAMPLE, STATIC ANALYSIS TOOLS CHECK FOR COMMON BUGS (E.G., BUFFER OVERFLOW IN C CODE), AND MUCH OF THE RESEARCH ON MONITORING SYSTEMS HAS FOCUSED ON CODE-LEVEL PROPERTIES. THE PROPOSED WORK BUILDS ON THE STRENGTHS OF BOTH OF THESE APPROACHES BY SYNTHESIZING MONITORS FOR SYSTEM-LEVEL PROPERTIES OF FAULT-TOLERANT REAL-TIME AVIONICS SYSTEMS. SYNTHESIZING MONITORS FOR SYSTEM-LEVEL PROPERTIES FROM HIGH-LEVEL SPECIFICATIONS EFFECTIVELY CLOSES THE GAP BETWEEN REQUIREMENTS AND IMPLEMENTATION FOR THESE KINDS OF SYSTEMS. FURTHERMORE, MONITORS ARE DIGITAL SYSTEMS THEMSELVES. AS SUCH, THEY ARE SUBJECT TO THE SAME KIND OF ERRORS THAT AFFECT THE SYSTEMS THEY ARE MONITORING. HENCE, THERE IS A NEED TO GENERATE MONITORS THAT CAN TOLERATE THEIR OWN FAULTS. THIS STATEMENT OF WORK IS THE RESULT OF PROPOSAL 08-IVHM1-08-0019 SUBMITTED BY GALOIS, INC. FOR AWARD UNDER THE NASA HEADQUARTERS AERONAUTICS RESEARCH MISSION DIRECTORATE (ARMD) NASA RESEARCH ANNOUNCEMENT (NRA) NNH08ZEA001N-IVHM1 ENTITLED RESEARCH OPPORTUNITIES IN AERONAUTICS 2008, AMENDMENT B.4, PROJECT INTEGRATED VEHICLE HEALTH MANAGEMENT (IVHM), TOPIC SOFTWARE HEALTH MANAGEMENT. THIS WORK SUPPORTS NASA IVHM MILESTONE 2.4.5.1 BY PRODUCING A REPORT ON SOFTWARE HEALTH MANAGEMENT FOCUSING ON THE ROLE OF SOFTWARE MONITORING AND RUNTIME VERIFICATION. THE PROPOSED RESEARCH DIRECTLY CONTRIBUTES TO IVHM MILESTONE 2.4.5.2 AS THE ANALYTICAL METHODS AND TOOLS DEVELOPED SHALL PROVIDE EFFECTIVE MEANS TO MONITOR DISTRIBUTED REAL-TIME FAULT-TOLERANT SYSTEMS SUCH AS NAVIGATION, GUIDANCE, AND CONTROL SYSTEMS; AND TO VERIFY THAT THEY BEHAVE AS EXPECTED. THE FOCUS SHALL BE ON SYNTHESIZING MONITORS FROM ABSTRACT SPECIFICATIONS WITH A PARTICULAR CONCENTRATION ON PROPERTIES THAT REQUIRE GLOBAL KNOWLEDGE OF THE STATE OF DISTRIBUTED REAL-TIME FAULT-TOLERANT SYSTEMS. THE PROPOSED RESEARCH ALSO CONTRIBUTES TO IVHM MILESTONE 2.4.5.3 BY INVESTIGATING HOW TO CLASSIFY THOSE SOFTWARE MALFUNCTIONS FOR WHICH IT IS POSSIBLE TO STEER DISTRIBUTED REAL-TIME SYSTEMS INTO A SAFE STATE SO AS TO RECOVER FROM THE POSSIBILITY OF A CATASTROPHIC SYSTEM FAILURE. 2.0 SCOPE OF WORK: THE GOALS OF THE PROPOSED RESEARCH ARE TO DEVELOP CAPABILITIES FOR 1) SYNTHESIZING MONITORS FROM SYSTEM-LEVEL REQUIREMENTS SPECIFICATIONS, 2) SYNTHESIZING MONITORS FOR FAULT-TOLERANT REAL-TIME DISTRIBUTED SYSTEMS, AND 3) SYNTHESIZING MONITORS THAT ARE FAULT-TOLERANT THEMSELVES. EARLY INVESTIGATIONS SHALL FOCUS ON THE OBJEC