DOI: https://doi.org/10.32515/2664-262X.2025.11(42).2.38-44
Specification and Verification of a Formal Model for a Real-Time System Using TLA+
About the Authors
Olena Shyshatska, PhD in Physics and Mathematics, Associate Professor at the Department of Theory and Technology of Programming, Faculty of Computer Science and Cybernetics, Taras Shevchenko National University of Kyiv, Kyiv, Ukraine, ORCID: https://orcid.org/0000-0001-8791-8989, е-mail: shyshatska@knu.ua
Liubomyr Matiichuk, Associate Professor, Doctor of Economics, Professor of the Department of Computer Science, Ternopil Ivan Puluj National Technical University, ORCID: https://orcid.org/0000-0001-6701-4683, e-mail: mlpstat@gmail.com
Andrii Shyshatskyy, Assistant at the Department of Theory and Technology of Programming, Faculty of Computer Science and Cybernetics, Taras Shevchenko National University of Kyiv, Kyiv, Ukraine, ORCID: https://orcid.org/0009-0000-5038-1110, e-mail: ashyshatskyy@knu.ua
Abstract
The paper describes theoretical and applied aspects of modeling real-time information systems using the example of a continuous glucose monitoring (CGM) system. The primary focus is on the application of formal methods, in particular the TLA+ specification language and modal logics, which ensure mathematical precision in describing system behavior. A formal model of the CGM system is constructed, safety invariants are defined, and automated model verification is performed using the TLC mechanism. The obtained results can be used to improve the reliability and justify the correctness of software-hardware solutions in the field of medical IT systems, particularly Closed-Loop Systems (CLS), which currently lack appropriate regulatory certification. The proposed approach contributes to the formalization of the validation process for such systems in accordance with standards for safety-critical software.
Keywords
real-time systems, CGM, model, formal design methods, specification, verification, TLA+
Full Text:
PDF
References
1. Rafeh, R., & Rabiee, A. (2013). Towards the design of safety-critical software. Journal of Applied Research and Technology, 11, 683–694.
2. Capozucca, A., & Guelfi, N. (2006). The fault-tolerant insulin pump. In Rigorous Development of Complex Fault-Tolerant Systems (pp. 59–75). Berlin: Springer-Verlag.
3. Lamport, L. (2002). Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston: Addison-Wesley Professional.
4. Wayne, H. (2018). Practical TLA+: Planning driven development. New York: Apress.
5. Fainekos, G., Kress-Gazit, H., & Pappas, G. (2005). Temporal logic motion planning for mobile robots. In Proceedings of the 2005 IEEE International Conference on Robotics and Automation (pp. 2020–2025). Barcelona: IEEE.
6. Humberstone, L. (2016). Philosophical applications of modal logic. London: College Publications.
7. Kripke, S. (1962). Semantical considerations for modal logics. Acta Philosophica Fennica, Helsinki, 389.
8. Guéron, J. (2008). Time and modality (Studies in Natural Language and Linguistic Theory; Vol. 75). Dordrecht: Springer.
9. Newcombe, C., Rath, T., Zhang, F., et al. (2015). How Amazon Web Services uses formal methods. Communications of the ACM, 58(4), 66–73.
10. Henzinger, T.A., & Sifakis, J. (2006). The discipline of embedded systems design. IEEE Computer, 39(10), 36–44.
11. Woodcock, J., Larsen, P.G., Bicarregui, J., & Fitzgerald, J. (2009). Formal methods: Practice and experience. ACM Computing Surveys (CSUR), 41(4), Article 19, 1–3.
12. AndrewShysh. (2025, February 15). Blood glucose monitoring model: Specification and verification [GitHub repository]. GitHub. https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main.
Citations
1. Rafeh, R., Rabiee, A. Towards the design of safety-critical software. Journal of Applied Research and Technology. 2013. Vol. 11. P. 683–694.
2. Capozucca, A., Guelfi, N. The fault-tolerant insulin pump. Rigorous Development of Complex Fault-Tolerant Systems. Berlin : Springer-Verlag, 2006. P. 59–75.
3. Lamport, L. Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston : Addison-Wesley Professional, 2002. 384 p.
4. Wayne, H. Practical TLA+: Planning driven development. New York : Apress, 2018. 221 p.
5. Fainekos, G., Kress-Gazit, H., Pappas, G. Temporal logic motion planning for mobile robots. Proceedings of the 2005 IEEE International Conference on Robotics and Automation. Barcelona, 2005. P. 2020–2025.
6. Humberstone, L. Philosophical applications of modal logic. London : College Publications, 2016. 588 p.
7. Kripke, S. Semantical considerations for modal logics. Acta Philosophica Fennica. 1962. Helsinki. 389 p.
8. Guéron, J. Time and modality. (Studies in Natural Language and Linguistic Theory ; Vol. 75). Dordrecht : Springer, 2008. 316 p.
9. Newcombe, C., Rath, T., Zhang, F. et al. How Amazon Web Services uses formal methods. Communications of the ACM. 2015. Vol. 58, No. 4. P. 66–73.
10. Henzinger, T. A., Sifakis, J. The discipline of embedded systems design. IEEE Computer. 2006. Vol. 39, No. 10. P. 36–44.
11. Woodcock, J., Larsen, P. G., Bicarregui, J., Fitzgerald, J. Formal methods: Practice and experience. ACM Computing Surveys (CSUR). 2009. Vol. 41, No. 4. Article No. 19. P. 1–3.
12. Blood glucose monitoring model: specification and verification. Github: веб-сайт. URL: https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main (дата звернення: 15.02.2025).
Copyright (c) 2025 Olena Shyshatska, Liubomyr Matiichuk, Andrii Shyshatskyy
Specification and Verification of a Formal Model for a Real-Time System Using TLA+
About the Authors
Olena Shyshatska, PhD in Physics and Mathematics, Associate Professor at the Department of Theory and Technology of Programming, Faculty of Computer Science and Cybernetics, Taras Shevchenko National University of Kyiv, Kyiv, Ukraine, ORCID: https://orcid.org/0000-0001-8791-8989, е-mail: shyshatska@knu.ua
Liubomyr Matiichuk, Associate Professor, Doctor of Economics, Professor of the Department of Computer Science, Ternopil Ivan Puluj National Technical University, ORCID: https://orcid.org/0000-0001-6701-4683, e-mail: mlpstat@gmail.com
Andrii Shyshatskyy, Assistant at the Department of Theory and Technology of Programming, Faculty of Computer Science and Cybernetics, Taras Shevchenko National University of Kyiv, Kyiv, Ukraine, ORCID: https://orcid.org/0009-0000-5038-1110, e-mail: ashyshatskyy@knu.ua
Abstract
Keywords
Full Text:
PDFReferences
1. Rafeh, R., & Rabiee, A. (2013). Towards the design of safety-critical software. Journal of Applied Research and Technology, 11, 683–694.
2. Capozucca, A., & Guelfi, N. (2006). The fault-tolerant insulin pump. In Rigorous Development of Complex Fault-Tolerant Systems (pp. 59–75). Berlin: Springer-Verlag.
3. Lamport, L. (2002). Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston: Addison-Wesley Professional.
4. Wayne, H. (2018). Practical TLA+: Planning driven development. New York: Apress.
5. Fainekos, G., Kress-Gazit, H., & Pappas, G. (2005). Temporal logic motion planning for mobile robots. In Proceedings of the 2005 IEEE International Conference on Robotics and Automation (pp. 2020–2025). Barcelona: IEEE.
6. Humberstone, L. (2016). Philosophical applications of modal logic. London: College Publications.
7. Kripke, S. (1962). Semantical considerations for modal logics. Acta Philosophica Fennica, Helsinki, 389.
8. Guéron, J. (2008). Time and modality (Studies in Natural Language and Linguistic Theory; Vol. 75). Dordrecht: Springer.
9. Newcombe, C., Rath, T., Zhang, F., et al. (2015). How Amazon Web Services uses formal methods. Communications of the ACM, 58(4), 66–73.
10. Henzinger, T.A., & Sifakis, J. (2006). The discipline of embedded systems design. IEEE Computer, 39(10), 36–44.
11. Woodcock, J., Larsen, P.G., Bicarregui, J., & Fitzgerald, J. (2009). Formal methods: Practice and experience. ACM Computing Surveys (CSUR), 41(4), Article 19, 1–3.
12. AndrewShysh. (2025, February 15). Blood glucose monitoring model: Specification and verification [GitHub repository]. GitHub. https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main.
Citations
1. Rafeh, R., Rabiee, A. Towards the design of safety-critical software. Journal of Applied Research and Technology. 2013. Vol. 11. P. 683–694.
2. Capozucca, A., Guelfi, N. The fault-tolerant insulin pump. Rigorous Development of Complex Fault-Tolerant Systems. Berlin : Springer-Verlag, 2006. P. 59–75.
3. Lamport, L. Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston : Addison-Wesley Professional, 2002. 384 p.
4. Wayne, H. Practical TLA+: Planning driven development. New York : Apress, 2018. 221 p.
5. Fainekos, G., Kress-Gazit, H., Pappas, G. Temporal logic motion planning for mobile robots. Proceedings of the 2005 IEEE International Conference on Robotics and Automation. Barcelona, 2005. P. 2020–2025.
6. Humberstone, L. Philosophical applications of modal logic. London : College Publications, 2016. 588 p.
7. Kripke, S. Semantical considerations for modal logics. Acta Philosophica Fennica. 1962. Helsinki. 389 p.
8. Guéron, J. Time and modality. (Studies in Natural Language and Linguistic Theory ; Vol. 75). Dordrecht : Springer, 2008. 316 p.
9. Newcombe, C., Rath, T., Zhang, F. et al. How Amazon Web Services uses formal methods. Communications of the ACM. 2015. Vol. 58, No. 4. P. 66–73.
10. Henzinger, T. A., Sifakis, J. The discipline of embedded systems design. IEEE Computer. 2006. Vol. 39, No. 10. P. 36–44.
11. Woodcock, J., Larsen, P. G., Bicarregui, J., Fitzgerald, J. Formal methods: Practice and experience. ACM Computing Surveys (CSUR). 2009. Vol. 41, No. 4. Article No. 19. P. 1–3.
12. Blood glucose monitoring model: specification and verification. Github: веб-сайт. URL: https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main (дата звернення: 15.02.2025).