Abstract
Using the Cadence SMV symbolic model checker we synthesize, under certain error assumptions, a scheduler for the smart card personalization system, a case study that has been proposed by Cybernetix Recherche in the context of the EU IST project AMETIST. The scheduler that we synthesize, and of which we prove optimality, has been previously patented. Due to the large number of states (which is beyond 1013), this synthesis problem appears to be out of the scope of existing tools for controller synthesis, which typically use some form of explicit state enumeration. Our result provides new evidence that model checkers can be useful to tackle industrial sized problems in the area of scheduling and control synthesis.
This work was supported by the European Community Project IST-2001-35304 AMETIST, http://ametist.cs.utwente.nl.
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.
References
Åkesson, K., Fabian, M.: Implementing supervisory control for chemical batch processes. In: International Conf. on Control Applications, pp. 1272–1277. IEEE Computer Society Press, Los Alamitos (1999)
Albert, S.: Cybernetix case study – informal description. Technical report, Cybernétix - LIF (2002), Available through http://ametist.cs.utwente.nl
Brandin, B.A.: The real-time supervisory control of an experimental manufacturing cell. IEEE Transactions on Robotics and Automation 12, 1–13 (1996)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers, Dordrecht (1999)
Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Communications ACM 17, 643–644 (1974)
Fehnker, A.: Scheduling a steel plant with timed automata. In: Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA 1999), Hong Kong, China, pp. 280–287. IEEE Computer Society Press, Los Alamitos (1999)
Gebremichael, B., Vaandrager, F.: Control synthesis for a smart card personalization system using symbolic model checking. Technical Report NIIIR0312, Nijmegen Institute for Computing and Information Sciences, University of Nijmegen (2003)
Gunnarsson, J.: Symbolic Methods and Tools for Discrete Event Dynamic Systems. PhD thesis, Linköping Studies in Science and Technology (1997)
Hune, T., Larsen, K.G., Pettersson, P.: Guided Synthesis of Control Programs using Uppaal. Nordic Journal of Computing 8(1), 43–64 (2001)
Krilavicius, T., Usenko, Y.: Smart card personalisation machine in UPPAAL and μCRL (2003) (in preparation)
Li, Y., Wonham, W.M.: Control of vector discrete-event systems I - the base model. In: IEEE Trans. on Automatic Control, vol. 38, pp. 1214–1227. IEEE Computer Society Press, Los Alamitos (1993)
Mader, A.: Deriving schedules for the cybernetix case study (2003), Available through http://ametist.cs.utwente.nl
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)
Niebert, P., Yovine, S.: Computing optimal operation schemes fo multi batch operation of chemical plants. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 338–351. Springer, Heidelberg (2000)
Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE 77, 81–98 (1989)
Ruys, T.: Optimal Scheduling Using Branch and Bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 1–17. Springer, Heidelberg (2003)
Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete event systems. IEEE Transactions on Automatic Control 40(9), 1555–1575 (1995)
Sreenivas, R.S., Krogh, B.H.: On condition/event systems with discrete state realizations. In: Discrete Event Dynamic Systems. Theory and Applications 1, pp. 209–236. Flumer Academic (1991)
Tel, G.: Introduction to Distributed Algorithms. Cambridge University Press, Cambridge (1994)
Weiss, G.: Modeling smart-card personalization machine with LSCs. Research report, Weizmann (2003)
Wonham, W.M., Li, Y.: Control of vector discrete-event systems II – controller synthesis. IEEE Transactions on Autom. Control 39, 512–531 (1994)
Zhang, Z., Wonham, W.M.: STCT: An efficient algorithm for supervisory control design. In: Symposium on Supervisory Control of Discrete Event Systems (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gebremichael, B., Vaandrager, F. (2004). Control Synthesis for a Smart Card Personalization System Using Symbolic Model Checking. In: Larsen, K.G., Niebert, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2003. Lecture Notes in Computer Science, vol 2791. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40903-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-40903-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21671-1
Online ISBN: 978-3-540-40903-8
eBook Packages: Springer Book Archive