Scalable Formal Methods for Multidimensional Components

本研究研究可扩展的形式化方法及其组合，以此来缩小形式化方法与软件实践之间的差距。这些方法包括特定于域的认证和运行时验证和监控。重要的子主题是：开发特定领域的知识，以得出高效和可扩展的算法和决策程序；通过组合使用几个“轻量级”正式方法来增强能力；多维组件不仅表示代码，而且还表示从不同角度对系统的不同看法；基于多维组件概念的可靠性度量，以便沿每个维度的可靠性增加聚合为可测量的总体可靠性增加。开发了各种原型：计量单位安全策略证明器；坐标框架安全证明器；最优状态估计证明器；运行时验证和监控原型。使用NASA-HDCP测试台对这些测试进行了实验评估。这项研究有望促进软件技术的进步，并有利于高等教育。软件合成、认证和监控的新颖组合导致了新的、强大的、可靠的软件开发方法，以确保以很少的开销或没有开销的安全执行。计划开设两门研究生课程。被资助的研究生通过与NASA科学家的密切合作，获得了坚实的科学基础，并获得了宝贵的经验。

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 alsodifferent 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, powerfuldependable software development methodologies ensuring safe execution with little or no overhead. Two graduate courses are planned. Supported graduate students are given a solid scientific foundationand acquire invaluable experience by working closely with NASA scientists.