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.
The research described in this paper was supported in part by the Natural Sciences and Engineering Research Council of Canada (NSERC).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Åkesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica—an integrated environment for verification, synthesis and simulation of discrete event systems. In: Proceedings of 8th International Workshop on Discrete Event Systems, pp. 384–385 (2006)
Barbeau, M., Kabanza, F., St-Denis, R.: An efficient algorithm for controller synthesis under full observation. Journal of Algorithms 25, 144–161 (1997)
Balemi, S., Hoffmann, G.J., Gyugyi, P., Wong-Toi, H., Franklin, G.F.: Supervisory control of a rapid thermal multiprocessor. IEEE Transactions on Automatic Control 38, 1040–1059 (1993)
Claessen, K., Een, N., Sheeran, M., Sörensson, N., Voronov, A., Åkesson, K.: SAT-solving in practice, with a tutorial example from supervisory control. Discrete Event Dynamic Systems: Theory and Applications 19, 495–524 (2009)
Côté, D.: Conception par composantes de contrôleurs d’usines modulaires utilisant la théorie du contrôle supervisé. Ph.D. thesis, Département d’informatique, Université de Sherbrooke, submitted (2011)
Côté, D., Embe Jiague, M., St-Denis, R.: Systems-theoretic view of component-based software development. In: Pre-proceedings of 7th International Workshop on Formal Aspects of Component Software, pp. 65–82 (2010) (to appear in Lecture Notes in Computer Science)
Fernandez, J.-C.: An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming 13, 219–236 (1990)
FESTO: Sorting Station—Modular Production System. Festo Didactic GmbH & Co., Denkendorf (1998)
Gebremichael, B., Vaandrager, F.: Control synthesis for a smart card personalization system using symbolic model checking. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 189–203. Springer, Heidelberg (2004)
Gromyko, A., Pistore, M., Traverso, P.: A tool for controller synthesis via symbolic model checking. In: Proceedings of 8th International Workshop on Discrete Event Systems, pp. 475–476 (2006)
Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)
Kumar, R., Garg, V.K.: Modeling and Control of Logical Discrete Event Systems. Kluwer Academic Publishers, Boston (1995)
Leduc, R.J., Lawford, M., Wonham, W.M.: Hierarchical interface-based supervisory control—part II: parallel case. IEEE Transactions on Automatic Control 50, 1336–1348 (2005)
Ma, C., Wonham, W.M.: Nonblocking Supervisory Control of State Tree Structures. Lecture Notes in Control and Information Sciences, vol. 317. Springer, Heidelberg (2005)
Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE 77, 81–98 (1989)
Song, R., Leduc, R.J.: Symbolic synthesis and verification of hierarchical interface-based supervisory control. In: Proceedings of 8th International Workshop on Discrete Event Systems, pp. 419–426 (2006)
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)
Wong, K.C., Wonham, W.M.: Hierarchical control of discrete-event systems. Discrete Event Dynamic Systems: Theory and Applications 6, 241–273 (1996)
Wong, K.C., Wonham, W.M.: On the computation of observers in discrete-event systems. Discrete Event Dynamic Systems: Theory and Applications 14, 55–107 (1996)
Zhang, Z., Wonham, W.M.: STCT: an efficient algorithm for supervisory control design. In: Caillaud, B., Darondeau, P., Lavagno, L., Xie, X. (eds.) Synthesis and Control of Discrete Event Systems, pp. 77–102. Kluwer Academic Publishers, The Netherlands (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Côté, D., Fraikin, B., Frappier, M., St-Denis, R. (2011). A SAT-Based Approach for the Construction of Reusable Control System Components. In: Salaün, G., Schätz, B. (eds) Formal Methods for Industrial Critical Systems. FMICS 2011. Lecture Notes in Computer Science, vol 6959. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24431-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-24431-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24430-8
Online ISBN: 978-3-642-24431-5
eBook Packages: Computer ScienceComputer Science (R0)