Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Methods for Industrial Critical Systems

FMICS 2019: Formal Methods for Industrial Critical Systems pp 76–92Cite as

The Impact of Requirement Splitting on the Efficiency of Supervisory Control Synthesis

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11687))

Abstract

Supervisory control theory provides means to synthesize supervisors for a cyber-physical system based on models of the uncontrolled system components and models of the control requirements. Although several synthesis procedures have been proposed and automated, obtaining correct and useful models of industrial-size applications that are needed as their input remains a challenge. We show that the efficiency of supervisor synthesis techniques tends to increase significantly if a single large requirement is split into a set of smaller requirements. A theoretical underpinning is provided for showing the strength of this modeling guideline. Moreover, several examples from the literature as well as some real-life case studies are included for illustration.

Supported by Rijkswaterstaat, part of the Dutch Ministry of Infrastructure and Water Management.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Here we have a slight abuse of notation of the synchronous product operator, as this one is only formally defined for automata. In case of two requirements modeled with state-event invariant expressions restricting the same event \(\sigma \), denoted by \(R_i = \sigma \) needs \(C_1, i\in \{1,2\}\), we define \(R_1\parallel R_2 = \sigma \) needs \(C_1 \wedge C_2\).

  2. 2.

    https://github.com/magoorden/SplittingRequirements.

References

  1. Basile, D., ter Beek, M.H., Di Giandomenico, F., Gnesi, S.: Orchestration of dynamic service product lines with featured modal contract automata. In: 21st International Systems and Software Product Line Conference , vol. B, pp. 117–122. ACM (2017). https://doi.org/10.1145/3109729.3109741

  2. van Beek, D.A., et al.: CIF 3: model-based engineering of supervisory controllers. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 575–580. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_48

    Chapter  Google Scholar 

  3. Cai, K., Wonham, W.M.: Supervisor localization: a top-down approach to distributed control of discrete-event systems. IEEE Trans. Autom. Control. 55(3), 605–618 (2010)

    Article  MathSciNet  Google Scholar 

  4. Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Boston (2008). https://doi.org/10.1007/978-0-387-68612-7

    Book  MATH  Google Scholar 

  5. Eppinger, S.D., Browning, T.R.: Design Structure Matrix Methods and Applications. MIT Press, Cambridge (2012)

    Book  Google Scholar 

  6. Fabian, M., Fei, Z., Miremadi, S., Lennartson, B., Åkesson, K.: Supervisory control of manufacturing systems using extended finite automata. In: Campos, J., Seatzo, C., Xie, X. (eds.) Formal Methods in Manufacturing. Industrial Information Technology, pp. 295–314. Taylor & Francis Inc., Boca Raton, February 2014

    Google Scholar 

  7. Göbe, F., Ney, O., Kowalewski, S.: Reusability and modularity of safety specifications for supervisory control. In: IEEE 21st International Conference on Emerging Technologies and Factory Automation, pp. 1–8, September 2016. https://doi.org/10.1109/ETFA.2016.7733498

  8. Goorden, M.A., van de Mortel-Fronczak, J.M., Reniers, M.A., Rooda, J.E.: Structuring multilevel discrete-event systems with dependency structure matrices. In: 56th IEEE Conference on Decision and Control, pp. 558–564, December 2017. https://doi.org/10.1109/CDC.2017.8263721

  9. Greenyer, J., Brenner, C., Cordy, M., Heymans, P., Gressi, E.: Incrementally synthesizing controllers from scenario-based product line specifications. In: 9th Joint Meeting on Foundations of Software Engineering, pp. 433–443. ACM (2013). https://doi.org/10.1145/2491411.2491445

  10. Grigorov, L., Butler, B.E., Cury, J.E.R., Rudie, K.: Conceptual design of discrete-event systems using templates. Discret. Event Dyn. Syst. 21(2), 257–303 (2011). https://doi.org/10.1007/s10626-010-0089-0

    Article  MathSciNet  MATH  Google Scholar 

  11. Jiao, T., Gan, Y., Xiao, G., Wonham, W.M.: Exploiting symmetry of discrete-event systems by relabeling and reconfiguration. IEEE Trans. Syst. Man Cybern.: Syst. 99, 1–12 (2018). https://doi.org/10.1109/TSMC.2018.2795011

    Article  Google Scholar 

  12. Komenda, J., Masopust, T., van Schuppen, J.H.: Control of an engineering-structured multilevel discrete-event system. In: 13th International Workshop on Discrete Event Systems, pp. 103–108, May 2016

    Google Scholar 

  13. Korssen, T., Dolk, V., van de Mortel-Fronczak, J.M., Reniers, M.A., Heemels, M.: Systematic model-based design and implementation of supervisors for advanced driver assistance systems. IEEE Trans. Intell. Transp. Syst. 19(2), 533–544 (2017). https://doi.org/10.1109/TITS.2017.2776354

    Article  Google Scholar 

  14. Lin, F., Wonham, W.M.: Decentralized control and coordination of discrete-event systems with partial observation. IEEE Trans. Autom. Control 35(12), 1330–1337 (1990). https://doi.org/10.1109/9.61009

    Article  MathSciNet  MATH  Google Scholar 

  15. Ma, C., Wonham, W.: Nonblocking Supervisory Control of State Tree Structures. Lecture Notes in Control and Information Sciences, vol. 317. Springer, Heidelberg (2005). https://doi.org/10.1007/b105592

    Book  MATH  Google Scholar 

  16. Markovski, J., Jacobs, K.G.M., van Beek, D.A., Somers, L.J., Rooda, J.E.: Coordination of resources using generalized state-based requirements, pp. 300–305 (2010)

    Article  Google Scholar 

  17. Modarres, M.: Risk Analysis in Engineering : Techniques, Tools, and Trends. CRC Press, Boca Raton (2016). https://doi.org/10.1201/b21429

    Book  Google Scholar 

  18. Mohajerani, S., Malik, R., Fabian, M.: A framework for compositional synthesis of modular nonblocking supervisors. IEEE Trans. Autom. Control 59(1), 150–162 (2014)

    Article  MathSciNet  Google Scholar 

  19. Mohajerani, S., Malik, R., Fabian, M.: A framework for compositional nonblocking verification of extended finite-state machines. Discret. Event Dyn. Syst. 26(1), 33–84 (2016). https://doi.org/10.1007/s10626-015-0217-y

    Article  MathSciNet  MATH  Google Scholar 

  20. de Queiroz, M.H., Cury, J.E.R.: Modular supervisory control of large scale discrete event systems. In: Boel, R., Stremersch, G. (eds.) Discrete Event Systems. The Springer International Series in Engineering and Computer Science, vol. 569, pp. 103–110. Springer, Boston (2000). https://doi.org/10.1007/978-1-4615-4493-7_10

    Chapter  MATH  Google Scholar 

  21. Ramadge, P.J.G., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control. Optim. 25(1), 206–230 (1987)

    Article  MathSciNet  Google Scholar 

  22. Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989)

    Article  Google Scholar 

  23. Ramos, A.L., Ferreira, J.V., Barceló, J.: Model-based systems engineering: an emerging approach for modern systems. IEEE Trans. Syst., Man, Cybern., Part C (Appl. Rev.) 42(1), 101–111 (2012). https://doi.org/10.1109/TSMCC.2011.2106495

    Article  Google Scholar 

  24. Reijnen, F.F.H., Goorden, M.A., van de Mortel-Fronczak, J.M., Reniers, M.A., Rooda, J.E.: Application of dependency structure matrices and multilevel synthesis to a production line. In: IEEE Conference on Control Technology and Applications, pp. 458–464, August 2018. https://doi.org/10.1109/CCTA.2018.8511449

  25. Reijnen, F.F.H., Goorden, M.A., van de Mortel-Fronczak, J.M., Rooda, J.E.: Supervisory control synthesis for a waterway lock. In: 1st IEEE Conference on Control Technology and Applications, pp. 1562–1568, August 2017. https://doi.org/10.1109/CCTA.2017.8062679

  26. Reijnen, F.F.H., Verbakel, J.J., van de Mortel-Fronczak, J.M., Rooda, J.E.: Hardware-in-the-loop set-up for supervisory controllers with an application: the Prinses Marijke complex. In: IEEE Conference on Control Technology and Applications, August 2019 (accepted)

    Google Scholar 

  27. Reijnen, F.F.H., Goorden, M.A., van de Mortel-Fronczak, J.M., Rooda, J.E.: Supervisory control synthesis for a lock-bridge combination. Discret. Event Dyn. Syst. (2019, submitted)

    Google Scholar 

  28. Rudie, K., Wonham, W.M.: Think globally, act locally: decentralized supervisory control. IEEE Trans. Autom. Control 37(11), 1692–1708 (1992)

    Article  MathSciNet  Google Scholar 

  29. Su, R., van Schuppen, J.H., Rooda, J.E.: Synthesize nonblocking distributed supervisors with coordinators. In: 17th Mediterranean Conference on Control and Automation, pp. 1108–1113, June 2009

    Google Scholar 

  30. Su, R., van Schuppen, J.H., Rooda, J.E., Hofkamp, A.T.: Nonconflict check by using sequential automaton abstractions based on weak observation equivalence. Automatica 46(6), 968–978 (2010)

    Article  MathSciNet  Google Scholar 

  31. Theunissen, R.J.M.: Supervisory Control in Health Care Systems. Ph.D. thesis, Eindhoven University of Technology, Eindhoven (2015). http://repository.tue.nl/786117

  32. Wonham, W.M., Ramadge, P.J.G.: Modular supervisory control of discrete-event systems. Math. Control Sig. Syst. 1(1), 13–30 (1988)

    Article  MathSciNet  Google Scholar 

  33. Wonham, W.M., Cai, K.: Supervisory Control of Discrete-Event Systems, 1st edn. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-319-77452-7

    Book  MATH  Google Scholar 

  34. Zhong, H., Wonham, W.M.: On the consistency of hierarchical supervision in discrete-event systems. IEEE Trans. Autom. Control 35(10), 1125–1134 (1990)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgments

The authors thank Ferdie Reijnen for providing the models of Lock III and the Prinses Marijke complex. The authors thank Rijkswaterstaat, part of the Dutch Ministry of Infrastructure and Water Management, for providing funding for this research. In particular, the authors thank Maria Angenent, Bert van der Vegt, and Han Vogel for their feedback on the results.

Author information

Authors and Affiliations

  1. Eindhoven University of Technology, Eindhoven, The Netherlands

    Martijn Goorden, Joanna van de Mortel-Fronczak, Michel Reniers & Jacobus Rooda

  2. Vrije Universiteit, Amsterdam, The Netherlands

    Wan Fokkink

Authors
  1. Martijn Goorden
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joanna van de Mortel-Fronczak
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michel Reniers
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Wan Fokkink
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Jacobus Rooda
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martijn Goorden .

Editor information

Editors and Affiliations

  1. Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen

  2. Eindhoven University of Technology, Eindhoven, The Netherlands

    Tim Willemse

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Goorden, M., van de Mortel-Fronczak, J., Reniers, M., Fokkink, W., Rooda, J. (2019). The Impact of Requirement Splitting on the Efficiency of Supervisory Control Synthesis. In: Larsen, K., Willemse, T. (eds) Formal Methods for Industrial Critical Systems. FMICS 2019. Lecture Notes in Computer Science(), vol 11687. Springer, Cham. https://doi.org/10.1007/978-3-030-27008-7_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-27008-7_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-27007-0

  • Online ISBN: 978-3-030-27008-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation