@inproceedings{29f308aeae0b42b7850b92f7b6b15fdb,
title = "Using the Rodin Platform as a Programming Tool",
abstract = "Being the result of several research projects that involved at the same time academic and industrial partners, the Rodin platform is designed to implement and analyse mathematical models of transitional systems based on Event-B language. Several plugins were integrated in the platform including ProB, a model checker that can be used to verify LTL properties or animate the model. In this paper, we introduce a methodology for using the Rodin platform and ProB as a powerful, integrated, programming and analysis environment. Our approach is based on assigning an FSM to an algorithm, then implementing the corresponding Event-B model in Rodin, and finally verifying its correctness and finiteness using the facilities of the platform.",
keywords = "Algorithms, Event-B language, Formal verification, FSM, Mathematical modelling, Model checking, Rodin platform",
author = "Adrian Turcanu and Florentin Ipate",
note = "Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.; 15th International Conference on Information Technology and Applications 2021, ICITA 2021 ; Conference date: 13-11-2021 Through 14-11-2021",
year = "2022",
month = apr,
day = "21",
doi = "10.1007/978-981-16-7618-5_44",
language = "English",
isbn = "9789811676178",
series = "Lecture Notes in Networks and Systems",
publisher = "Springer",
pages = "505--513",
editor = "Abrar Ullah and Steve Gill and {\'A}lvaro Rocha and Sajid Anwar",
booktitle = "Proceedings of International Conference on Information Technology and Applications. ICITA 2021",
}