A SAT-based approach for the construction of reusable control system components

Abstract

This paper shows how to take advantage of a SAT-solving approach in the development of safety control software systems for manufacturing plants. In particular, it demonstrates how to construct reusable components which are assembled after instantiation to derive controllers of modular production systems. An experiment has been conducted with Alloy not only to verify properties required by a control theory for complex systems organized hierarchically, but also to synthesize two major parts of a component: observer and supervisor. The former defines its interface while guaranteeing nonblocking hierarchical control. The latter ensures the satisfaction of constraints imposed on its behavior and on the interactions among its subcomponents during system operation. As long as the size of component interfaces is small, SAT-solvers appear useful to build correct reusable components because the formal models that engineers manipulate and analyze are very close to the abstract models of the mathematical theory. © 2011 Springer-Verlag.