Modular Verification of Logic Controllers

提案编号：CMS 0528287 PI：蒂尔伯里，黎明摘要本项目的目标是发展必要的理论和技术，逻辑控制系统的模块化验证。 逻辑控制器用于许多应用，如制造系统，卫星，自主机器人和主动数据库。 在低层次上，逻辑控制器只是一组规则。 然而，当成百上千条规则在一个复杂的系统中共同起作用时，可能会发生意外或不期望的行为。 该项目将开发模块化核查技术，使核查比现有集中技术复杂得多的系统成为可能。 它也将调查是否一个系统的某些属性不能被验证在一个模块化的方式，从而给予洞察到逻辑控制系统的全局和局部属性之间的区别。或具有呼叫等待、呼叫转移和呼叫者ID的电话-各种新功能可能相互干扰。 这种特性干扰会导致系统中出现意外行为，称为“自动化意外”。由于复杂性，设计师不可能想象环境因素和用户命令的所有可能组合，并检查系统是否按预期运行。该项目将开发自动验证复杂系统以正确和安全的方式运行的方法和技术。该项目的成果将通过纳入控制系统本科课程的单元加以传播。

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.