An automated qualitative analysis of real-time systems using Timed Petri net and SPIN

References

• Adalid, D., Salmerón, A., Gallardo, M. d M., & Merino, P. (2014). Using spin for automated debugging of infinite executions of java programs. Journal of Systems and Software, 90, 61–75. https://doi.org/10.1016/j.jss.2013.10.056
   Web of Science ®Google Scholar
• Alam, D. M., & He, X. (2017). A method to analyze predicate transition nets using spin model checker. International Journal of Software Engineering and Knowledge Engineering, 27(09n10), 1455–1481. https://doi.org/10.1142/S021819401740006X
   Google Scholar
• Argote García, G., Clarke, P. J., He, X., Fu, Y., & Shi, L. (2008). A formal approach for translating a sam architecture to PROMELA. 20th International Conference on Software Engineering and Knowledge Engineering (pp. 440–447). Knowledge Systems Institute (KSI).
   Google Scholar
• Asankhaya, S. (2013). End to end verification and validation with spin. CoRR.
   Google Scholar
• Basic Spin Manual. (2017, August 3). Manual. https://spinroot.com/spin/man/html
   Google Scholar
• Bause, F., & Kritzinger, P. (2013). Stochastic petri nets -An introduction to the theory. Vieweg. ISBN 3-528-15535-3.
   Google Scholar
• Behrmann, G., David, A., & Larsen, K. G. A. (2004). A tutorial on uppaal (pp. 200–236). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-30080-97
   Google Scholar
• Ben-Ari, M. M. (2010). A primer on model checking. ACM Inroads, 1(1), 40–47. https://doi.org/10.1145/1721933.1721950
   Google Scholar
• Besnard, V., Teodorov, C., Jouault, F., Brun, M., & Dhaussy, P. (2021). Unified verification and monitoring of executable UML specifications. a transformation-free approach. Software and Systems Modeling, 20(6), 1825–1855. https://doi.org/10.1007/s10270-021-00923-9
   Web of Science ®Google Scholar
• Byg, J., Jørgensen, K. Y., & Srba, J. (2009). TAPAAL: Editor, simulator and verifier of timed-arc petri nets. In Z. Liu, A. P. Ravn (Ed.), Automated technology for verification and analysis (pp. 84–89). Springer Berlin Heidelberg.
   Google Scholar
• Chaichompoo, O., Thongtak, A., & Vatanawood, W. (2017). Transformation of time petri net into PROMELA [Paper presentation]. 11th International Conference on Telecommunication Systems Services and Applications (TSSA) (p. 1). IEEE. https://doi.org/10.1109/TSSA.2017.8272928
   Google Scholar
• Chang, L., & He, X. (2015). A methodology to analyze multi-agent systems modeled in high level petri nets. International Journal of Software Engineering and Knowledge Engineering, 25(07), 1199–1235. https://doi.org/10.1142/S0218194015500230
   Google Scholar
• Cimatti, A., Clarke, E. M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., & Tacchella, A. (2002). NuSMV 2: An opensource tool for symbolic model checking [Paper presentation]. Proceedings of the 14th International Conference on Computer Aided Verification (pp. 359–364). Springer Berlin Heidelberg.
   Google Scholar
• Clarke, E., Grumberg, O., & Peled, D. (2001). Model checking. MIT Press.
   Google Scholar
• Concise PROMELA Reference. (1997). https://www.cse.msu.edu/∼cse470/ promela manual/quick.html.
   Google Scholar
• Ding, X., Smith, S. L., Belta, C., & Rus, D. (2014). Optimal control of markov decision processes with linear temporal logic constraints. IEEE Transactions on Automatic Control, 59(5), 1244–1257. https://doi.org/10.1109/TAC.2014.2298143
   Web of Science ®Google Scholar
• Dingle, N., William, K., & Tamas, S. (2009). PIPE2 a tool for the performance evaluation of generalised stochastic Petri Nets. ACM SIGMETRICS Performance Evaluation Review, 36(4), 34–39. https://doi.org/10.1145/1530873.1530881
   Google Scholar
• dos Santos, L. B. R., de Santiago Júnior, V. A., & Vijaykumar, N. L. (2014). Transformation of UML behavioral diagrams to support software model checking [Paper presentation]. Proceedings 11th International Workshop on Formal Engineering Approaches to Software Components and Architectures (pp. 133–142). Open Publishing Association.
   Google Scholar
• Fernandes, F., & Song, M. (2014). UML-checker: An approach for verifying uml behavioral diagrams. Journal of Software, 9(5), 1229–1236. https://doi.org/10.4304/jsw.9.5.1229-1236
   Google Scholar
• Fortier, P. J., & Michel, H. (2002). Computer systems performance evaluation and prediction. Butterworth-Heinemann.
   Google Scholar
• Gardey, G., Lime, D., Magnin, M., & Olivier (H.) R. (2005). Romeo: A tool for analyzing time petri nets. In K. Etessami & S. K. Rajamani (Eds.), Computer Aided Verification (pp.418–423). Springer, Berlin, Heidelberg.
   Google Scholar
• Gerogiannis, V., Kameas, A., & Pintelas, P. (1998). Comparative study and categorization of high-level petri nets. Journal of Systems and Software, 43(2), 133–160. https://doi.org/10.1016/S0164-1212(98)10028-6
   Web of Science ®Google Scholar
• Grobelna, I., & Szcześniak, P. (2022). Model checking autonomous components within electric power systems specified by interpreted petri nets. Sensors, 22(18), 6936.
   PubMed Web of Science ®Google Scholar
• Hamman, S. T., Hopkinson, K. M., & Fadul, J. E. (2016). A model checking approach to testing the reliability of smart grid protection systems. IEEE Transactions on Power Delivery, 32(6), 1–1. https://doi.org/10.1109/TPWRD.2016.2635480
   Web of Science ®Google Scholar
• He, L., Liu, G., & Zhou, M. (2023). Petri-net-based model checking for privacy-critical multiagent systems. IEEE Transactions on Computational Social Systems, 10(2), 563–576. https://doi.org/10.1109/TCSS.2022.3164052
   Web of Science ®Google Scholar
• Holzmann, G. J. (1997). The model checker spin. IEEE Transactions on Software Engineering, 23(5), 279–295. https://doi.org/10.1109/32.588521
   Web of Science ®Google Scholar
• Huth, M., & Ryan, M. (2004). Logic in computer science: Modelling and reasoning about systems. Cambridge University Press.
   Google Scholar
• JavaTPoint. (2023). Java DOM, JavaTPoint. https://www.javatpoint.com/java-dom.
   Google Scholar
• Kawises, J., & Vatanawood, W. (2019). Formalizing time petri nets with metric temporal logic using PROMELA [Paper presentation]. 20th IEEE/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD). IEEE. https://doi.org/10.1109/SNPD.2019.8935861
   Google Scholar
• Kwiatkowska, M., Norman, G., & Parker, D. (2011). Prism 4.0: Verification of probabilistic real- time systems (pp. 585–591). Computer Aided Verification.
   Google Scholar
• Lima, V., Talhi, C., Mouheb, D., Debbabi, M., Wang, L., Makan Pourzand. (2009). Formal verification and validation of uml 2.0 sequence diagrams using source and destination of messages. Electronic Notes in Theoretical Computer Science, 254:143–160.
   Google Scholar
• Lin, C., Huang, C., & Wang, B. (2018). A spin-based model checking for the simple concurrent program on a preemptive RTOS. CoRR. abs/1808.04239. http://arxiv.org/abs/1808.04239.
   Google Scholar
• Liu Guanjun Petri Nets. (2022). Theoretical models and analysis methods for concurrent systems. Springer Nature. https://doi.org/10.1007/978-981-19-6309-4
   Google Scholar
• Marsan, M. A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G. (1995). Modelling with generalised stochastic petri nets. Wiley.
   Google Scholar
• Mordechai, B. (2013). Mathematical logic for computer science (3rd ed.). Springer.
   Google Scholar
• Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4), 541–580. https://doi.org/10.1109/5.24143
   Web of Science ®Google Scholar
• Nakahori, K., & Yamaguchi, S. (2017). A support tool to design iot services with NuSMV [Paper presentation]. 2017 IEEE International Conference on Consumer Electronics (ICCE) (pp. 80–83). IEEE. https://doi.org/10.1109/ICCE.2017.7889238
   Google Scholar
• Oubelli, M. A., Younsi, N., Amirat, A., et al. (2011, December 13–15). From UML 2.0 sequence diagrams to PROMELE to PROMELA code by graph transformation using atom3 [Paper presentation]. Proceedings of the Third International Conference on Computer Science and its Applications (CIIA'11) (Vol. 825). Saida, Algeria.
   Google Scholar
• Popova-Zeugmann, L. (2013). Louchka Time Petri nets (pp. 31–137). Springer. https://doi.org/10.1007/978-3-642-41115-1_3
   Google Scholar
• Ribeiro, O. R., & Fernandes, J. M. (2007). Translating synchronous petri nets into promela for verifying behavioral properties [Paper presentation]. 2007 International Symposium on Industrial Embedded Systems (pp. 266–273). IEEE. https://doi.org/10.1109/SIES.2007.4297344
   Google Scholar
• Szpyrka, M., Biernacka, A., & Biernacki, J. (2014). Methods of translation of petri nets to NuSMV language. CS&P
   Google Scholar
• van Leeuwen J (Ed.). (1991). Handbook of theoretical computer science (vol. a): Algorithms and complexity. MIT Press.
   Google Scholar
• Vernadat, F., Berthomieu, B., Vernadat, F., Berthomieu, B. (2006). Time petri nets analysis with tina [Paper presentation]. Third International Conference on the Quantitative Evaluation of Systems - (QEST'06) (pp. 23–124). IEEE. https://doi.org/10.1109/QEST.2006.56.
   Google Scholar
• Viswanadham, N., & Narahari, Y. (1992). Performance modeling of automated manufacturing. Prentice-Hall, Inc.
   Google Scholar
• Vizovitin, N., Nepomniaschy, V., & Stenenko, A. (2017). Application of colored petri nets for verification of scenario control structures in ucm notation. Automatic Control and Computer Sciences, 51(7), 489–497. 12. https://doi.org/10.3103/S0146411617070227
   Google Scholar
• Wang, J. (1998). Time Petri nets (pp. 63–123). Springer US. https://doi.org/10.1007/978-1-4615-5537-7_4
   Google Scholar
• Wiśniewski, R., Wojnakowski, M., & Li, Z. (2022). Design and verification of petri-net-based cyber-physical systems oriented toward implementation in field-programmable gate arrays-a case study example. Energies, 16(1), 67.
   Web of Science ®Google Scholar
• Zhang, P., Muccini, H., & Li, B. (2010). A classification and comparison of model checking software architecture techniques. Journal of Systems and Software, 83(5), 723–744. https://doi.org/10.1016/j.jss.2009.11.709
   Web of Science ®Google Scholar