SPECIFICATION FORMALIZATION OF STATE CHARTS FOR COMPLEX SYSTEM MANAGEMENT
DOI:
https://doi.org/10.20998/2079-0023.2023.01.16Keywords:
formal methods, automated programming, state machines, model checking, theorem proving, code generation, object-oriented programming, spacecraft control, requirements formalization, verification and validationAbstract
This article presents a formalization approach for the requirements of object-oriented programs with state machines, using a spacecraft control system as a case study. It proposes a state pattern implementation, where each state is represented as a class with clearly defined responsibilities, and the transitions between states are controlled by the state objects themselves. Additionally, the application of model checking, theorem proving, and code generation techniques are discussed. The effectiveness of the proposed approach in ensuring compliance with the specified requirements is demonstrated, while also identifying potential drawbacks and limitations of the approach. The implementation is validated using a range of formal verification techniques, including model checking and theorem proving. The article also discusses how the approach can be extended and applied to other complex systems. Overall, the valuable insights into the formalization of requirements for object-oriented programs with state machines are provided, offering a practical and effective approach for verifying the correctness and completeness of such implementations. The results of this work have important implications for the development of safety-critical systems and can potentially improve the quality and reliability of software systems in various domains. By using mathematical models and rigorous formal methods, it is possible to detect and eliminate errors early in the development process, leading to higher confidence in the correctness of the final product. Future research in this area could explore the use of more advanced techniques, such as model-driven development and automatic code synthesis, to further streamline the software development process. Additionally, the development of more efficient and user-friendly tools could make these techniques more accessible to a wider range of developers and organizations. Altogether, the combination of formal methods and software engineering has the potential to revolutionize the way software systems are designed, developed, and verified, leading to safer and more reliable software for critical applications.
References
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.
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution 4.0 International License.
Authors who publish with this journal agree to the following terms:
- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
