Scalable Formal Methods for Multidimensional Components

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

This research investigates scalable formal methods and their combinations as a way to reduce the gap between formal methods and software practice. These methods include domain-specific certification and runtime verification and monitoring. Important subthemes are: exploitation of domain-specific knowledge to derive efficient and scalable algorithms and decision procedures; strength through the combined use of several "lightweight" formal methods; multidimensional components to represent not only code, but also different views of the system from different perspectives; dependability metrics based on the notion of multidimensional component, so that increases in dependability along each dimension are aggregated into measurable overall dependability increases. Various prototypes are developed: safety policy certifier for units of measurement; coordinate frame safety certifier; optimality state estimation certifier; runtime verification and monitoring prototypes. These are experimentally evaluated using the NASA-HDCP testbed. This research is expected to lead to advances in software technology and to benefit advanced education. Novel combinations of software synthesis, certification and monitoring lead to new, powerful dependable software development methodologies ensuring safe execution with little or no overhead. Two graduate courses are planned. Supported graduate students are given a solid scientific foundation and acquire invaluable experience by working closely with NASA scientists.