Scalable Formal Methods for Multidimensional Components

多维组件的可扩展形式方法

• 批准号: 0234524
• 负责人: Grigore Rosu
• 金额: $ 40万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-15 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0234524&HistoricalAwards=false
• 关键词: Scalable; Formal; Methods; Multidimensional; Components

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.

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