Hierarchical Specification, Analysis, and Testing of Real-Time Systems

实时系统的分层规范、分析和测试

• 批准号: 9415346
• 负责人: Insup Lee
• 金额: $ 18.91万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-07-01 至 1998-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9415346&HistoricalAwards=false
• 关键词: Hierarchical; Specification; Analysis; Testing; Real

As computers become ubiquitous, they are increasingly used in safety critical environments. Typical safety applications are control systems, monitoring systems and communication systems. Any failure of such computer systems may cause a great financial loss, environmental disaster or even the loss of lives. The potential high cost associated with an incorrect operation of these systems has created a demand for a rigorous framework in which various design alternatives can be formally specified and rigorously analyzed and tested before implementation. It is commonly believed that future safety critical systems uill be more complex due to increased demands on their functionalities, as well as, the size of the problem domain. Thus, it will be difficult to analyze and test the correctness without computer-aided tools. One common aspect of all safety critical systems is that they must respond under stringent realtime constraints. That is, their correctness depends not only on how concurrent components interact, but also on the time at which these interactions occur. These systems are costly to prototype, requiring careful prediction of timing properties before implementation and evaluation of design alternatives. Thus, it is important to develop a formal framework that supports automatic and computer-aided analysis and testing to effectively cope with increased complexity. The major thrust of this research is to develop analysis and testing techniques for timing properties, and to implement supporting software tools based on real-time temporal logic and state machine models. The proposed tools will provide an environment in which software engineers can generate tests from behavioral specifications and performance requirement constraints and simulate and test to validate the specification.

随着计算机变得无处不在，它们越来越多地用于安全关键环境中。典型的安全应用是控制系统、监控系统和通信系统。这些计算机系统的任何故障都可能造成巨大的经济损失、环境灾难甚至生命损失。 与这些系统的不正确操作相关的潜在高成本已经产生了对严格框架的需求，在该框架中，可以正式指定各种设计方案，并在实施之前进行严格的分析和测试。人们普遍认为，未来的安全关键系统将更加复杂，由于其功能的需求增加，以及，问题域的大小。 因此，如果没有计算机辅助工具，将很难分析和测试的正确性。所有安全关键系统的一个共同点是它们必须在严格的实时约束下做出响应。 也就是说，它们的正确性不仅取决于并发组件如何交互，还取决于这些交互发生的时间。 这些系统是昂贵的原型，需要仔细预测的时间属性之前，实施和评估的设计方案。 因此，重要的是要开发一个正式的框架，支持自动和计算机辅助分析和测试，以有效地科普日益增加的复杂性。 本研究的主要目的是发展时序特性的分析与测试技术，并以实时时序逻辑与状态机模型为基础，开发相关的软件工具。所提出的工具将提供一个环境，在该环境中，软件工程师可以生成测试的行为规范和性能要求的约束和模拟和测试，以验证规范。