Transformational supervisor synthesis for evolving systems. (English) Zbl 1492.93116
Discrete Event Dyn. Syst. 32, No. 2, 317-358 (2022); correction ibid. 33, No. 4, 509-513 (2023).
Summary: Supervisory controller synthesis is a means to compute correct-by-construction controllers for discrete event systems. As these systems and their requirements evolve over time, an updated supervisor needs to be computed each time an adaptation takes place. We consider the case that a supervisor has been synthesized for a given model, after which this model is (slightly) adapted. We investigate how we can make use of the previous synthesis result, in order to more efficiently compute the supervisor for the adapted model. We introduce model deltas as a means to describe the difference between pairs of models. Using the model deltas, a notion of atomic adaptations is introduced. For these atomic adaptations, algorithms are provided to compute the supervisor for the adapted model in a transformational manner from the previous synthesis result, rather than performing a completely new synthesis. These atomic adaptations can be iterated over, to transformationally compute a supervisor for model deltas that contain a number of atomic adaptations. To improve efficiency, it is shown how atomic adaptations can be grouped together based on their required computations and be processed at the same time. A running example is used to support the explanations on the functioning of the algorithms. The efficiency of the method is evaluated by means of both an academic and an industrial use case.
Keywords:
discrete event systems; supervisory control theory; supervisor synthesis; software product line engineering; delta modeling; software evolutionReferences:
| [1] | Broadfoot GH, Hopcroft PJ (2003) Analytical software design. Technical report, Verum Consultants B.V. |
| [2] | Cassandras, CG; Lafortune, S., Introduction to Discrete Event Systems (2008), Boston: Springer, Boston · Zbl 1165.93001 · doi:10.1007/978-0-387-68612-7 |
| [3] | Classen A, Heymans P, Schobbens PY, Legay A, Raskin JF (2010) Model checking lots of systems: Efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, p 335-344 |
| [4] | Fei, Z.; Miremadi, S.; Ȧkesson, K.; Lennartson, B., Efficient symbolic supervisor synthesis for extended finite automata, IEEE Trans Control Syst Technol, 22, 6, 2368-2375 (2014) · doi:10.1109/TCST.2014.2303134 |
| [5] | Flordal, H.; Malik, R.; Fabian, M.; Åkesson, K., Compositional synthesis of maximally permissive supervisors using supervision equivalence, Discret Event Dyn Syst, 17, 4, 475-504 (2007) · Zbl 1125.93018 · doi:10.1007/s10626-007-0018-z |
| [6] | Khan YI (2013) Optimizing verification of structurally evolving algebraic Petri nets. In: Proceedings of the 5th International Workshop Software Engineering for Resilient Systems, Lecture Notes in Computer Science, vol 8166, pp 64-78 |
| [7] | Kleinberg, J.; Tardos, E., Algorithm Design Addison-Wesley Longman Publishing Co. (2005), Boston: Inc., Boston |
| [8] | Krook J, Kianfar R, Fabian M (2020) Formal synthesis of safe stop tactical planners for an automated vehicle. In: Proceedings of the 15th IFAC Workshop on Discrete Event Systems, IFAC-PapersOnLine, vol 53, pp 445-452 |
| [9] | Larman, C.; Basili, VR, Iterative and incremental development: a brief history, Computer, 36, 6, 47-56 (2003) · doi:10.1109/MC.2003.1204375 |
| [10] | Lehman, MM, Laws of software evolution revisited, Softw Process Technol Lect Notes Comput Sci, 1149, 108-124 (1996) · doi:10.1007/BFb0017737 |
| [11] | Markovski J, van Beek D, Theunissen R, Jacobs K, Rooda J (2010) A state-based framework for supervisory control synthesis and verification. In: Proceedings of the 49th IEEE Conference on Decision and Control, pp 3481-3486 |
| [12] | Ouedraogo, L.; Kumar, R.; Malik, R.; Ȧkesson, K., Nonblocking and safe control of discrete-event systems modeled as extended finite automata, IEEE Trans Autom Sci Eng, 8, 3, 560-569 (2011) · doi:10.1109/TASE.2011.2124457 |
| [13] | Pohl, K.; Böckle, G.; van der Linden, FJ, Software Product Line Engineering: Foundations Principles and Techniques (2005), Berlin: Springer-Verlag, Berlin · Zbl 1075.68575 · doi:10.1007/3-540-28901-1 |
| [14] | Ramadge, PJ; Wonham, WM, Supervisory control of a class of discrete event processes, SIAM J Control Optim, 25, 1, 206-230 (1987) · Zbl 0618.93033 · doi:10.1137/0325013 |
| [15] | Ramadge, PJ; Wonham, WM, The control of discrete event systems, Proc IEEE, 77, 1, 81-98 (1989) · doi:10.1109/5.21072 |
| [16] | Rawlings BC, Christenson B, Wassick JM, Ydstie BE (2014) Supervisor synthesis to satisfy safety and reachability requirements in chemical process control. In: Proceedings of the 12th IFAC Workshop on Discrete Event Systems, IFAC Proceedings Volumes, vol 47, pp 195-200 |
| [17] | Reijnen FFH, Goorden MA, van de Mortel-Fronczak JM, Rooda JE (2020) Modeling for supervisor synthesis – a lock-bridge combination case study. Discret Event Dyna Syst 30(3):499-532 · Zbl 1448.93088 |
| [18] | Reniers MA, Thuijsman SB (2020) Supervisory control for dynamic feature configuration in product lines. In: Proceedings of the IEEE Forum on Specification and Design Languages, pp 1-8 |
| [19] | Rosa M, Cury JER, Baldissera FL (2020) Supervisory control in construction robotics: in the quest for scalability and permissiveness. In: Proceedings of the 15th IFAC Workshop on Discrete Event Systems, IFAC-PapersOnLine, vol 53, pp 117-122 |
| [20] | Schaefer, I.; Rabiser, R.; Clarke, D.; Bettini, L.; Benavides, D.; Botterweck, G.; Pathak, A.; Trujillo, S.; Villela, K., Software diversity: state of the art and perspectives, Int J Softw Tools Technol Transfer, 14, 5, 477-495 (2012) · doi:10.1007/s10009-012-0253-y |
| [21] | Theunissen, RJM; Petreczky, M.; Schiffelers, RRH; van Beek, DA; Rooda, JE, Application of supervisory control synthesis to a patient support table of a magnetic resonance imaging scanner, IEEE Trans Autom Sci Eng, 11, 1, 20-32 (2014) · doi:10.1109/TASE.2013.2279692 |
| [22] | Thuijsman SB, Reniers MA (2020) Transformational supervisor synthesis for evolving systems. In: Proceedings of the 15th IFAC Workshop on Discrete Event Systems, IFAC-PapersOnLine, vol 53, pp 309-316 |
| [23] | Tijsse Claase RG (2020) Symbolic transformational supervisor synthesis. Master’s thesis, Eindhoven University of Technology, Department of Mechanical Engineering |
| [24] | Wonham, WM; Cai, K., Supervisory Control of Discrete-Event Systems (2019), Cham: Springer, Cham · Zbl 1405.93008 · doi:10.1007/978-3-319-77452-7 |
| [25] | Wonham, WM; Cai, K.; Rudie, K., Supervisory control of discrete-event systems: A brief history, IFAC Annu Rev Control, 45, 250-256 (2018) · doi:10.1016/j.arcontrol.2018.03.002 |
| [26] | ter Beek MH, Reniers MA, de Vink EP (2016) Supervisory controller synthesis for product lines using CIF 3. In: Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Lecture Notes in Computer Science, vol 9952, pp 856-873 |
| [27] | ter Beek MH, de Vink EP (2014) Towards modular verification of software product lines with mCRL2. In: Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, Lecture Notes in Computer Science, vol 8802, pp 368-385 |
| [28] | van Beek DA, Fokkink WJ, Hendriks D, Hofkamp A, Markovski J, van de Mortel-Fronczak JM, Reniers MA (2014) CIf 3: Model-based engineering of supervisory controllers. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol 8413, pp 575-580 |
| [29] | van der Sanden LJ, Reniers MA, Geilen MCW, Basten AA, Jacobs J, Voeten JPM, Schiffelers RRH (2015) Modular model-based supervisory controller design for wafer logistics in lithography machines. In: Proceedings of the ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, pp 416-425 |
| [30] | van der Schriek YIC (2018) Evaluation of supervisory control theory based on requirement evolution of LOPW. Master’s thesis, Eindhoven University of Technology, Deptartment of Mechanical Engineering |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
