ITR/SY: Modular Interface Violation Checking Using Formally-Specified Contracts

ITR/SY：使用正式指定的合同进行模块化接口违规检查

• 批准号: 0113181
• 负责人: Murali Sitaraman
• 金额: --
• 依托单位: Clemson University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-08-15 至 2007-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0113181&HistoricalAwards=false
• 关键词: ITR; SY; Modular; Interface; Violation

AbstractProposal #0113181SitaramanClemson UniversityA fundamental goal of software engineering is to enable predictable and modular construction of software systems by assembling components. Any component-based approach works on the basic premise that participating components respect each other's contracts. If this premise is violated, the consequences can be both dangerous and expensive, because the problems may not surface until integration time. Even worse, a system may behave properly on test cases, though internal interface contracts are violated. Undetected failures from internal violations may be revealed ultimately only as accidents to component-based and embedded systems after deployment.This project offers a modular approach for detecting and isolating internal contractual violations. The approach allows checking at suitable levels of abstraction using formal specifications. It permits checking to be turned "on" or "off" selectively to facilitate effective regression testing, and it addresses violations of performance contracts in addition to functionality for parameterized and object-oriented components. To minimize errors in the violation checking process, the project will use and experimentally evaluate alternative combinations of automation, formal verification, model checking, and testing techniques.

软件工程的基本目标是通过组装组件来实现可预测和模块化的软件系统构建。任何基于组件的方法都以参与的组件尊重彼此的契约为基本前提。如果违反了这个前提，后果可能既危险又昂贵，因为问题可能要到集成时才会出现。更糟糕的是，系统可能在测试用例上正常运行，尽管内部接口契约被违反了。内部违规导致的未检测到的故障可能最终只会在部署后显示为基于组件的系统和嵌入式系统的事故。该项目提供了一种检测和隔离内部合同违规的模块化方法。该方法允许使用正式规范在适当的抽象级别进行检查。它允许选择性地“打开”或“关闭”检查，以促进有效的回归测试，并且除了参数化和面向对象组件的功能之外，它还解决了违反性能契约的问题。为了最小化违例检查过程中的错误，项目将使用并实验性地评估自动化、正式验证、模型检查和测试技术的可选组合。