ФОРМАЛІЗАЦІЯ СПЕЦИФІКАЦІЇ СХЕМ СТАНУ ДЛЯ УПРАВЛІННЯ СКЛАДНИМИ СИСТЕМАМИ
DOI:
https://doi.org/10.20998/2079-0023.2023.01.16Ключові слова:
формальні методи, автоматизоване програмування, кінцеві автомати, перевірка моделі, доведення теорем, генерація коду, об’єктно–орієнтоване програмування, управління космічним кораблем, формалізація вимог, верифікація та валідаціяАнотація
У статті представлено підхід формалізації для вимог об’єктно-орієнтованих програм із кінцевими автоматами з використанням як прикладу системи керування космічним апаратом. Запропоновано реалізацію шаблону стану, де кожен стан представлено як клас із чітко визначеними обов’язками, а переходи між станами контролюються самими об’єктами стану. Крім того, обговорюється застосування методів перевірки моделі, доведення теорем і генерації коду. Продемонстровано ефективність запропонованого підходу щодо забезпечення відповідності зазначеним вимогам, а також виявлено потенційні недоліки та обмеження підходу. Реалізація перевіряється за допомогою низки формальних методів перевірки, включаючи перевірку моделі та доведення теорем. У статті також обговорюється, як цей підхід можна розширити та застосувати до інших складних систем. Загалом, надано детальну інформацію щодо формалізації вимог до об’єктно–орієнтованих програм із кінцевими автоматами, що пропонує практичний та ефективний підхід для перевірки правильності та повноти таких реалізацій. Результати цієї роботи мають важливе значення для розробки критично важливих для безпеки систем і потенційно можуть підвищити якість і надійність програмних систем у різних областях. За допомогою математичних моделей і строгих формальних методів можна виявити й усунути помилки на ранніх стадіях процесу розробки, що веде до більшої впевненості в правильності кінцевого продукту. Майбутні дослідження в цій галузі можуть вивчити використання більш передових методів, таких як розробка на основі моделі та автоматичний синтез коду, для подальшої оптимізації процесу розробки програмного забезпечення. Крім того, розробка більш ефективних і зручних інструментів може зробити ці методи більш доступними для широкого кола розробників і організацій. Загалом, поєднання формальних методів і розробки програмного забезпечення має потенціал революціонізувати спосіб проектування, розробки та перевірки систем програмного забезпечення, створюючи безпечніше та надійніше програмне забезпечення для критичних програм.
Посилання
Lodi S., Mesiti M., Orsi G. A state machine for relational databases. In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering. 2019. P. 114–125.
Liggesmeyer P., Seib E., Prehofer C. A state machine approach for modeling and testing autonomous driving functions. In Proceedings of the 2021 IEEE Intelligent Vehicles Symposium. 2021. P. 2854–2859.
Giannakopoulou D., Pasareanu C., Rungta N. An integrated approach to analyzing and testing stateful systems. In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering. 2017. P. 943–948.
Saenz J. C., Perez–Palacin D., d'Amorim M. Behavior–driven development of stateful systems: a case study of a medical information system. In Proceedings of the 2019 IEEE/ACM International Conference on Automated Software Engineering. 2019. P. 1011–1016.
Azevedo G., Ribeiro M., Medeiros F. Model–based test generation for stateful systems using an FSM language. In Proceedings of the 2018 IEEE International Conference on Software Testing, Verification and Validation. 2018. P. 237–247.
Daumke P., Laroche L., Graubner S. A state machine–based approach for the dynamic adaptation of software systems. In Proceedings of the 14th International Conference on Software Technologies. 2019. P. 466–475.
Lo D., Liu Y., Xie X., Wong S. Symbolic execution of stateful programs with abstract state machines. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 2019. P. 285–296.
Li Y., Li Y., Dong J. S. Formally verifying the state machine–based software through the UPPAAL model checker. Journal of Intelligent & Fuzzy Systems 36(4). 2019. P. 3657–3668.
Chen Q., Liu S., Wang S., Sun J. Efficient generation of state machine models from Java source code for vulnerability detection. Journal of Systems and Software, 177. 2021. 237 p.
Jovanovic J., Rackovic M., Milicic M. Analysis of the role of state machine diagrams in software development: An exploratory study. Information and Software Technology, 103. 2019. 132–146 p.
Chen X., Chen J., Wang J. Research on Formalization Method of State Transition Rules for Automated Vehicle Systems. IEEE Access, 8. 2020. P. 134116–134127.
Eltoweissy M., Alnemr R., Seliem M., Ali M. Formal specification and verification of state–based software systems: A systematic literature review. Journal of Systems and Software, 163. 2021. P. 1105–1128.
Gaber A., Elragal A. Formalizing requirements for automated driving systems: A systematic literature review. Safety Science, 142. 2021. P. 538–549.
Gu C., Li X., Liu Y. A Formal Method for Analyzing and Validating the Functionality of Statecharts. IEEE Access, 7. 2021. P. 135–154.
Taha I., Ahmed E., Al–Mamory S., Karama S. Formalizing Requirements for State Machine Models of Safety–Critical Systems: A Review. IEEE Access, 9. 2021. P. 315–333.
##submission.downloads##
Опубліковано
Як цитувати
Номер
Розділ
Ліцензія
Ця робота ліцензується відповідно до Creative Commons Attribution 4.0 International License.
Автори, які публікуються у цьому журналі, погоджуються з наступними умовами:
- Автори залишають за собою право на авторство своєї роботи та передають журналу право першої публікації цієї роботи на умовах ліцензії Creative Commons Attribution License, котра дозволяє іншим особам вільно розповсюджувати опубліковану роботу з обов'язковим посиланням на авторів оригінальної роботи та першу публікацію роботи у цьому журналі.
- Автори мають право укладати самостійні додаткові угоди щодо неексклюзивного розповсюдження роботи у тому вигляді, в якому вона була опублікована цим журналом (наприклад, розміщувати роботу в електронному сховищі установи або публікувати у складі монографії), за умови збереження посилання на першу публікацію роботи у цьому журналі.
- Політика журналу дозволяє і заохочує розміщення авторами в мережі Інтернет (наприклад, у сховищах установ або на особистих веб-сайтах) рукопису роботи, як до подання цього рукопису до редакції, так і під час його редакційного опрацювання, оскільки це сприяє виникненню продуктивної наукової дискусії та позитивно позначається на оперативності та динаміці цитування опублікованої роботи (див. The Effect of Open Access).
