Advertisement
Published in:
2011 | OriginalPaper | Chapter
A SAT-Based Approach for the Construction of Reusable Control System Components
Authors : Daniel Côté, Benoît Fraikin, Marc Frappier, Richard St-Denis
Published in: Formal Methods for Industrial Critical Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.