Skip to main content
SpringerLink
Log in

New Method to Reduce Verification Time of Reconfigurable Real-Time Systems Using R-TNCESs Formalism

  • Conference paper
  • First Online:
Evaluation of Novel Approaches to Software Engineering (ENASE 2019)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 1172))

Abstract

Nowadays, several systems like manufacturing, aerospace, medical, and telecommunication ones face new challenges such as fault-tolerance, response in time, flexibility, modularity, etc. To deal with these requirements, systems had to include new abilities. Consequently, systems become more complex, and their verification becomes expensive in terms of computation time and memory. Reconfigurable real-time systems are ones of those complex systems that encompass reconfigurability constraints and subject to real-time requirements. Their verification is often a hard task due to their complex behavior. In this paper, we formally model these systems using reconfigurable timed net condition/event systems (R-TNCESs) formalism, which is a Petri net extension for reconfigurable systems. Then, we propose a new methodology to efficiently verify real-time properties by avoiding redundant computations. An application of the paper contributions is carried out on a benchmark manufacturing system, a performance evaluation is achieved to demonstrate it and to compare it with other related works.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Aichernig, B.K., Schumi, R.: Statistical model checking meets property-based testing. In: Proceedings IEEE International Conference on Software Testing, Verification and Validation ICST, pp. 390–400. IEEE (2017)

    Google Scholar 

  2. Arcaini, P., Riccobene, E., Scandurra, P.: Formal design and verification of self-adaptive systems with decentralized control. ACM Trans. Auton. Adapt. Syst. (TAAS) 11(4), 25 (2017)

    Google Scholar 

  3. Badouel, E., Oliver, J.: Reconfigurable nets, a class of high level Petri nets supporting dynamic changes within workflow systems. Ph.D. thesis, Inria (1998)

    Google Scholar 

  4. Baier, C., Katoen, J., Larsen, K.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  5. Ben Salah, H., Benzina, A., Khalgui, M.: Verification of reconfigurable NoC under quality of service constraints. In: Proceedings IEEE 40th Annual Computer Software and Applications Conference (COMPSAC), pp. 329–334. IEEE (2016)

    Google Scholar 

  6. Ben Salem, M.O., Mosbahi, O., Khalgui, M., Jlalia, Z., Frey, G., Smida, M.: BROMETH: methodology to design safe reconfigurable medical robotic systems. Int. J. Med. Robot. Comput. Assist. Surg. 13(3), 1786 (2016). https://doi.org/10.1002/rcs.1786

    Article  Google Scholar 

  7. Biermann, E., Modica, T.: Independence analysis of firing and rule-based net transformations in reconfigurable object nets. Electron. Commun. EASST 10 (2008)

    Google Scholar 

  8. Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Heidelberg (2016)

    MATH  Google Scholar 

  9. Dubinin, V., Vyatkin, V., Hanisch, H.M.: Synthesis of safety controllers for distributed automation systems on the basis of reverse safe net condition/event systems. In: Proceedings IEEE Trustcom/BigDataSE/ISPA, vol. 3, pp. 287–292, August 2015

    Google Scholar 

  10. Guellouz, S., Benzina, A., Khalgui, M., Frey, G.: ZiZo: a complete tool chain for the modeling and verification of reconfigurable function blocks. In: UBICOMM 2016: the Tenth International Conference on Mobile Ubiquitous Computing, Systems, Services and Technologies, 10 2016 (2016)

    Google Scholar 

  11. Hafidi, Y., Kahloul, L., Khalgui, M., Li, Z., Alnowibet, K., Qu, T.: On methodology for the verification of reconfigurable timed net condition/event systems. IEEE Trans. Syst. Man Cybern. Syst. 99, 1–15 (2018)

    Google Scholar 

  12. Hafidi, Y., Kahloul, L., Khalgui, M., Ramdani, M.: On improved verification of reconfigurable real-time systems. In: Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE, pp. 394–401. INSTICC, SciTePress (2019). https://doi.org/10.5220/0007736603940401

  13. Hanisch, H.M., Thieme, J., Luder, A., Wienhold, O.: Modeling of PLC behavior by means of timed net condition/event systems. In: Proceedings 6th International Conference on Emerging Technologies and Factory Automation Proceedings, pp. 391–396. IEEE (1997)

    Google Scholar 

  14. Hasan, O., Tahar, S.: Formal verification methods. In: Encyclopedia of Information Science and Technology, 3rd (edn.), pp. 7162–7170. IGI Global (2015)

    Google Scholar 

  15. Kahloul, L., Bourekkache, S., Djouani, K.: Designing reconfigurable manufacturing systems using reconfigurable object Petri nets. Int. J. Comput. Integr. Manuf. 29(8), 889–906 (2016)

    Article  Google Scholar 

  16. Khalgui, M., Mosbahi, O., Li, Z., Hanisch, H.M.: Reconfigurable multiagent embedded control systems: from modeling to implementation. IEEE Trans. Comput. 60(4), 538–551 (2011)

    Article  MathSciNet  Google Scholar 

  17. Khalgui, M.: NCES-based modelling and CTL-based verification of reconfigurable embedded control systems. Comput. Ind. 61(3), 198–212 (2010)

    Article  Google Scholar 

  18. Khlifi, O., Mosbahi, O., Khalgui, M., Frey, G.: GR-TNCES: new extensions of R-TNCES for modelling and verification of flexible systems under energy and memory constraints. In: Proceedings 10th International Joint Conference on Software Technologies (ICSOFT), vol. 1, pp. 1–8. IEEE (2015)

    Google Scholar 

  19. Khlifi, O., Mosbahi, O., Khalgui, M., Frey, G.: New verification approach for reconfigurable distributed systems. In: Proceedings 12th International Conference on Software and Data Technologies ICSOFT, pp. 355–362, 01 2017 (2017)

    Google Scholar 

  20. Lakhdhar, W., Mzid, R., Khalgui, M., Li, Z., Frey, G., Al-Ahmari, A.: Multiobjective optimization approach for a portable development of reconfigurable real-time systems: from specification to implementation. IEEE Trans. Syst. Man Cybern. Syst. 49, 623–637 (2018)

    Article  Google Scholar 

  21. Lyke, J.C., Christodoulou, C.G., Vera, G.A., Edwards, A.H.: An introduction to reconfigurable systems. Proc. IEEE 103(3), 291–317 (2015)

    Article  Google Scholar 

  22. Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  23. Padberg, J., Kahloul, L.: Overview of reconfigurable Petri nets. In: Heckel, R., Taentzer, G. (eds.) Graph Transformation, Specifications, and Nets. LNCS, vol. 10800, pp. 201–222. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75396-6_11

    Chapter  MATH  Google Scholar 

  24. Patil, S., Vyatkin, V., Pang, C.: Counterexample-guided simulation framework for formal verification of flexible automation systems. In: Proceedings IEEE 13th International Conference on Industrial Informatics (INDIN), pp. 1192–1197, July 2015

    Google Scholar 

  25. Ramdani, M., Kahloul, L., Khalgui, M.: Automatic properties classification approach for guiding the verification of complex reconfigurable systems. In: Proceedings of the 13th International Conference on Software Technologies - Volume 1: ICSOFT, pp. 591–598. INSTICC, SciTePress (2018). https://doi.org/10.5220/0006863005910598

  26. Ramdani, M., Kahloul, L., Khalgui, M., Hafidi, Y.: R-TNCES rebuilding: a new method of CTL model update for reconfigurable systems. In: Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE, pp. 159–168. INSTICC, SciTePress (2019). https://doi.org/10.5220/0007736801590168

  27. Rausch, M., Hanisch, H.M.: Net condition/event systems with multiple condition outputs. In: Proceedings Emerging Technologies and Factory Automation, vol. 1, pp. 592–600. IEEE (1995)

    Google Scholar 

  28. Starke, P.H., Roch, S.: Analysing Signal-Net Systems. Citeseer, New York (2002)

    Google Scholar 

  29. Wang, C., Pastore, F., Briand, L.: System testing of timing requirements based on use cases and timed automata. In: Proceedings IEEE International Conference on Software Testing, Verification and Validation ICST. IEEE (2017)

    Google Scholar 

  30. Wang, X., Li, Z., Wonham, W.M.: Dynamic multiple-period reconfiguration of real-time scheduling based on timed DES supervisory control. IEEE Trans. Ind. Inf. 12(1), 101–111 (2016). https://doi.org/10.1109/TII.2015.2500161

    Article  Google Scholar 

  31. Yanase, R., Sakai, T., Sakai, M., Yamane, S.: Formal verification of dynamically reconfigurable systems. In: Proceedings IEEE 4th Global Conference on Consumer Electronics (GCCE), pp. 71–75, October 2015

    Google Scholar 

  32. Zhang, J., Frey, G., Al-Ahmari, A., Qu, T., Wu, N., Li, Z.: Analysis and control of dynamic reconfiguration processes of manufacturing systems. IEEE Access 6, 28028–28040 (2017)

    Article  Google Scholar 

  33. Zhang, J., et al.: Modeling and verification of reconfigurable and energy-efficient manufacturing systems. Discret. Dyn. Nat. Soc. 2015, 14 (2015)

    Google Scholar 

  34. Zhang, J., Khalgui, M., Li, Z., Frey, G., Mosbahi, O., Salah, H.B.: Reconfigurable coordination of distributed discrete event control systems. IEEE Trans. Control Sys. Techn. 23(1), 323–330 (2015)

    Article  Google Scholar 

  35. Zhang, J., Khalgui, M., Li, Z., Mosbahi, O., Al-Ahmari, A.: R-TNCES: a novel formalism for reconfigurable discrete event control systems. IEEE Trans. Systems Man Cybern. Syst. 43(4), 757–772 (2013)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Tunis El Manar, Tunis, Tunisia

    Yousra Hafidi & Mohamed Ramdani

  2. LINFI Laboratory, Computer Science Department, Biskra University, Biskra, Algeria

    Yousra Hafidi, Laid Kahloul & Mohamed Ramdani

  3. LISI Laboratory, National Institute of Applied Sciences and Technology, University of Carthage, 1080, Tunis, Tunisia

    Yousra Hafidi, Mohamed Khalgui & Mohamed Ramdani

  4. School of Electrical and Information Engineering, Jinan University, Guangzhou, China

    Yousra Hafidi, Mohamed Khalgui & Mohamed Ramdani

Authors
  1. Yousra Hafidi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laid Kahloul
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mohamed Khalgui
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mohamed Ramdani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yousra Hafidi .

Editor information

Editors and Affiliations

  1. Department of Electrical and Computer Engineering, Khalifa University of Science and Technology, Abu Dhabi, United Arab Emirates

    Ernesto Damiani

  2. Department of Computer Science, City University of London, London, UK

    George Spanoudakis

  3. Wroclaw University of Economics, Wroclaw, Poland

    Leszek A. Maciaszek

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hafidi, Y., Kahloul, L., Khalgui, M., Ramdani, M. (2020). New Method to Reduce Verification Time of Reconfigurable Real-Time Systems Using R-TNCESs Formalism. In: Damiani, E., Spanoudakis, G., Maciaszek, L. (eds) Evaluation of Novel Approaches to Software Engineering. ENASE 2019. Communications in Computer and Information Science, vol 1172. Springer, Cham. https://doi.org/10.1007/978-3-030-40223-5_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-40223-5_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-40222-8

  • Online ISBN: 978-3-030-40223-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation