Specification and Analysis of Data for Safety-Critical Systems

摘要

Data-driven systems are those that make use of large quantities of data to perform their function. For a data-drivensystem that must also be dependable, ensuring the validity of data is just as crucial as ensuring that of code. Data forsuch systems are often developed separately from the systems themselves and, if not subjected to careful scrutiny,might not adhere to all of the assumptions made by the systems’ developers. This paper describes a specification andverification technique for data that employs both formal and informal specification methods. This technique is illustratedusing part of a real-world system: the Minimum Safe Altitude Warning (MSAW) system, a data-driven systemthat is used by the U.S. Federal Aviation Administration to detect and alert air traffic controllers to low-flying aircraft.