Control Synthesis for a Smart Card Personalization System Using Symbolic Model Checking

  • Biniam Gebremichael
  • Frits Vaandrager
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


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.


Model Check Conveyor Belt Control Synthesis Supervisory Control Discrete Event System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Å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)Google Scholar
  2. 2.
    Albert, S.: Cybernetix case study – informal description. Technical report, Cybernétix - LIF (2002), Available through
  3. 3.
    Brandin, B.A.: The real-time supervisory control of an experimental manufacturing cell. IEEE Transactions on Robotics and Automation 12, 1–13 (1996)CrossRefGoogle Scholar
  4. 4.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers, Dordrecht (1999)zbMATHGoogle Scholar
  6. 6.
    Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Communications ACM 17, 643–644 (1974)zbMATHCrossRefGoogle Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Gunnarsson, J.: Symbolic Methods and Tools for Discrete Event Dynamic Systems. PhD thesis, Linköping Studies in Science and Technology (1997)Google Scholar
  10. 10.
    Hune, T., Larsen, K.G., Pettersson, P.: Guided Synthesis of Control Programs using Uppaal. Nordic Journal of Computing 8(1), 43–64 (2001)zbMATHGoogle Scholar
  11. 11.
    Krilavicius, T., Usenko, Y.: Smart card personalisation machine in UPPAAL and μCRL (2003) (in preparation)Google Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    Mader, A.: Deriving schedules for the cybernetix case study (2003), Available through
  14. 14.
    McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE 77, 81–98 (1989)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    Tel, G.: Introduction to Distributed Algorithms. Cambridge University Press, Cambridge (1994)zbMATHCrossRefGoogle Scholar
  21. 21.
    Weiss, G.: Modeling smart-card personalization machine with LSCs. Research report, Weizmann (2003)Google Scholar
  22. 22.
    Wonham, W.M., Li, Y.: Control of vector discrete-event systems II – controller synthesis. IEEE Transactions on Autom. Control 39, 512–531 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Zhang, Z., Wonham, W.M.: STCT: An efficient algorithm for supervisory control design. In: Symposium on Supervisory Control of Discrete Event Systems (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Biniam Gebremichael
    • 1
  • Frits Vaandrager
    • 1
  1. 1.Nijmegen Institute for Computing and Information SciencesUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations