Factorization of the State Space Construction for Cyclic Systems with Data

1. Verifcar models. https://forge.ibisc.univ-evry.fr/jarcile/VerifCar. Accessed 29 May 2023

2. Ahmad, S., Malik, S., Ullah, I., Park, D.-H., Kim, K., Kim, D.H.: Towards the design of a formal verification and evaluation tool of real-time tasks scheduling of IoT applications. Sustainability 11(1), 204 (2019)

   Article  Google Scholar 

3. André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_6

   Chapter  Google Scholar 

4. Arcile, J., André, É.: Timed automata as a formalism for expressing security: a survey on theory and practice. ACM Comput. Surv. 55(6), 127:1–127:36 (2023)

   Google Scholar 

5. Arcile, J., Devillers, R.R., Klaudel, H.: Verifcar: a framework for modeling and model checking communicating autonomous vehicles. Auton. Agents Multi Agent Syst. 33(3), 353–381 (2019)

   Article  Google Scholar 

6. Arcile, J., Devillers, R.R., Klaudel, H.: Dynamic exploration of multi-agent systems with periodic timed tasks. Fundam. Informaticae 175(1–4), 59–95 (2020)

   Article  MathSciNet  Google Scholar 

7. Barnes, J.E.: Experiences in the industrial use of formal methods. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46 (2011)

   Google Scholar 

8. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_18

   Chapter  Google Scholar 

9. Berthomieu, B., Vernadat, F.: Time petri nets analysis with TINA. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), pp. 123–124. IEEE Computer Society. 11–14 September 2006, Riverside, California, USA (2006)

   Google Scholar 

10. Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 298–302. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055357

    Chapter  Google Scholar 

11. Caspi, P., Mazuet, C., Paligot, N.R.: About the design of distributed control systems: the quasi-synchronous approach. In: Voges, U. (ed.) SAFECOMP 2001. LNCS, vol. 2187, pp. 215–226. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45416-0_21

    Chapter  Google Scholar 

12. Cheng, A.M.K.: A survey of formal verification methods and tools for embedded and real-time systems. Int. J. Embed. Syst. 2(3/4), 184–195 (2006)

    Article  Google Scholar 

13. Dabaghchian, M., Rakamaric, Z.: A timeless model for the verification of quasi-periodic distributed systems. In: Partha, S., Roop, Zhan, N., Gao, S., Nuzzo, P., (eds.) Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2019, pp. 4:1–4:11. ACM. October 9–11 2019. La Jolla, CA, USA ( 2019)

    Google Scholar 

14. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054180

    Chapter  Google Scholar 

15. Dutertre, B., Sorea, M.: Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 199–214. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_15

    Chapter  Google Scholar 

16. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company, Boston (1979)

    Google Scholar 

17. Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 2.0: a tool for probabilistic model checking. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), pp. 322–323. IEEE Computer Society. 27–30 September 2004, Enschede, The Netherlands (2004)

    Google Scholar 

18. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)

    Article  Google Scholar 

19. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

20. Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_6

    Chapter  Google Scholar 

21. Maiza, C., Rihani, H., Rivas, J.M., Goossens, J., Altmeyer, S., Davis, R.I.: A survey of timing verification techniques for multi-core real-time systems. ACM Comput. Surv. 52(3), 56:1–56:38 (2019)

    Google Scholar 

22. Saha, I., Misra, J., Roy, S.: Timeout and calendar based finite state modeling and verification of real-time systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 284–299. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75596-8_21

    Chapter  Google Scholar 

23. Snook, C.F., Harrison, R.: Practitioners’ views on the use of formal methods: an industrial survey by structured interview. Inf. Softw. Technol. 43(4), 275–283 (2001)

    Article  Google Scholar 

24. Zheng, X., Julien, C., Kim, M., Khurshid, S.: Perceptions on the state of the art in verification and validation in cyber-physical systems. IEEE Syst. J. 11(4), 2614–2627 (2017)

    Article  Google Scholar 

Download references