Modular Verification of Logic Controllers

摘要本课题的目标是为逻辑控制系统的模块化验证提供必要的理论和技术。逻辑控制器用于许多应用，如制造系统，卫星，自主机器人和活动数据库。在较低的层次上，逻辑控制器只是一组规则。然而，当数百或数千个这样的规则在一个复杂的系统中一起作用时，可能会发生意外或不希望发生的行为。该项目将开发模块化验证技术，与现有的集中式技术相比，可以验证更复杂的系统。它还将研究系统的某些属性是否不能以模块化方式验证，从而深入了解逻辑控制系统的全局和局部属性之间的区别。随着系统变得越来越复杂——例如，带有防抱死刹车、电子稳定控制和四轮转向系统的汽车；或者具有呼叫等待、呼叫转移和来电显示功能的电话——各种新功能可能会相互干扰。这种特性干扰会导致系统中出现意想不到的行为，称为“自动化意外”。由于复杂性，设计师不可能想象出环境因素和用户命令的所有可能组合，并检查系统是否按预期运行。该项目将开发方法和技术来自动验证复杂系统以正确和安全的方式运行。该项目的成果将通过集成在控制系统本科课程中的模块进行传播。

Proposal #: CMS 0528287PI: Tilbury, Dawn AbstractThe goal of this project is to develop the necessary theories and technologies for modular verification of logic control systems. Logic controllers are used for many applications such as manufacturing systems, satellites, autonomous robots, and active databases. At a low level, a logic controller is simply a set of rules. However, when hundreds or thousands of these rules are acting together in a complex system, unexpected or undesirable behavior can occur. This project will develop modular verification technologies that will allow much more complex systems to be verified than are possible with existing centralized techniques. It will also investigate whether some properties of a system cannot be verified in a modular fashion, thus giving insight into the distinction between global and local properties of logic control systems.As systems become more complex -- for example, cars with antilock brakes, electronic stability control, and four-wheel steering; or telephones with call waiting, call forwarding, and caller ID - the various new features can interfere with each other. This feature interference can cause unexpected behaviors to occur in the system, called "automation surprises." Because of the complexity, it is impossible for the designer to imagine all possible combinations of environmental factors and user commands and check that the system behaves as desired. This project will develop methods and techniques to automatically verify that complex systems operate in a correct and safe manner. The results of the project will be disseminated through modules integrated into undergraduate courses in control systems.