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.