Modeling, Simulation and Verification of Probabilistic Reconfigurable Discrete-Event Systems Under Energy and Memory Constraints

  • O. Khlifi
  • O. Mosbahi
  • M. KhalguiEmail author
  • G. Frey
  • Z. Li
Research Paper


Adaptive probabilistic systems have ability to modify their behaviors to cope with unpredictable significant changes at run-time such as component failures or resources depletion. Reconfiguration is often a major task for systems, i.e., it may violate the memory usage, the required energy and the concerned real-time constraints. It might also make the system’s functions unavailable for some time and make potential harm to human life or large financial investments. Thus, updating a system with any new configuration requires that the post-reconfigurable system fully satisfies the related constraints. Formal modeling and verification could avoid the resources and constraints violation. Thus, the paper proposes a new formalism to specify such systems. We also develop a new visual environment named ZIZO which helps in modeling, constructive simulation and CTL-based verification of adaptive probabilistic systems. The contributions are used to guarantee the resources and correctness of an IPv4 ZeroConf protocol.


Reconfiguration Petri net Model checking Memory and energy control 


  1. Andrade E, Maciel P, Callou G, Nogueira B (2009) A methodology for mapping SysML activity diagram to time Petri net for requirement validation of embedded real-time systems with energy constraints. In: Proceedings of the 3rd international conference on digital society, Cancun, Mexico, pp 266–271Google Scholar
  2. Axelsson R, Hague M, Kreutzer S, Lange M, Latte M (2010) Extended computation tree logic. In: Logic for programming, artificial intelligence, and reasoning. Springer, Berlin, pp 67–81Google Scholar
  3. Bai LP, Wu NQ, Li ZW, Zhou MC (2016) Optimal one-wafer cyclic scheduling and buffer space configuration for single-arm multicluster tools with linear topology. IEEE Trans Syst Man Cybern Syst 46(10):1456–1467CrossRefGoogle Scholar
  4. Bohnenkamp H, Van der Stok P, Hermanns H, Vaandrager F (2003) Cost-optimization of the IPV4 zeroconf protocol. In: Proceedings of the international conference on dependable systems and networks, pp 531–540Google Scholar
  5. Bouyer P (2007) Model-checking timed temporal logics. In: Proceedings of the 5th workshop on methods for modalities, France, pp 323–341Google Scholar
  6. Brázdil T, Forejt V, Kretínský J, Kucera A (2008) The satisfiability problem for probabilistic CTL. In: Proceedings of the 23rd Annual IEEE symposium on logic in computer science, LICS, Pittsburgh, PA, pp 391–402Google Scholar
  7. Chen YF, Li ZW, Barkaoui K, Giua A (2015) On the enforcement of a class of nonlinear constraints on Petri nets. Automatica 55:116–124MathSciNetCrossRefzbMATHGoogle Scholar
  8. Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263CrossRefzbMATHGoogle Scholar
  9. Cong X, Fanti MP, Mangini AM, Li ZW (2017) Decentralized diagnosis by Petri nets and integer linear programming. IEEE Trans Syst Man Cybern Syst. Google Scholar
  10. Dumitrache I, Caramihai SI, Stanescu AM (2000) Intelligent agent based control systems in manufacturing. In: Proceedings of the 2000 IEEE International Symposium on Intelligent Control, Rio Patras, pp 369–374Google Scholar
  11. Forejt V, Kwiatkowska M, Norman G, Parker D (2011) Automated verification techniques for probabilistic system. In: Bernardo M, Issarny V (eds) Formal methods for eternal networked software systems (SFM'11), vol 6659. Springer, Heidelberg, pp 53–113Google Scholar
  12. Gasmi M, Mosbahi O, Khalgui M, Gomes L, Li ZW (2016) R-Node: new pipelined approach for an effective reconfigurable wireless sensor node. IEEE Trans Syst Man Cybern Syst 99:1–14Google Scholar
  13. Hanisch HM, Thieme J, Luder A, Wienhold O (1997) Modeling of plc behavior by means of timed net condition/event systems. In: Proceedings of emerging technologies and factory automation, ETFA, Los Angeles, CA, pp 391–396Google Scholar
  14. Heydari A, Landers RG, Balakrishnan SN (2014) Optimal control approach for turning process planning optimization. IEEE Trans Contol Syst Technol 22(4):1337–1349CrossRefGoogle Scholar
  15. Kalita D, Khargonekar PP (2002) Formal verification for analysis and design of logic controllers for reconfigurable machining systems. IEEE Trans Robot Autom 18(4):463–474CrossRefGoogle Scholar
  16. Khlifi O, Mosbahi O, Khalgui M, Frey G (2015) GR-TNCES: new extensions of R-TNCES for modelling and verification of flexible systems under energy and memory constraints. In: Proceedings of the international conference on software engineering and App, ICSOFT-EA, Colmar, France, pp 373–380Google Scholar
  17. Kopetz H (2003) Time-triggered real-time computing. Ann Rev Control 27(1):3–13CrossRefGoogle Scholar
  18. Li ZW, Liu GY, Hanisch M-H, Zhou MC (2012) Deadlock prevention based on structure reuse of Petri net supervisors for flexible manufacturing systems. IEEE Trans Syst Man Cybern Part A Syst Hum 42(1):178–191CrossRefGoogle Scholar
  19. Ma F, Wang J (2008) Modeling and simulation method of enterprise energy consumption process based on fuzzy timed Petri nets. In: Proceedings of the 7th world congress on intelligent control and automation Chongqing, China, pp 4148–4153Google Scholar
  20. Ma Z, Li ZW, Giua A (2017a) Characterization of admissible marking sets in Petri nets with conflicts and synchronizations. IEEE Trans Autom Control 62(3):1329–1341MathSciNetCrossRefzbMATHGoogle Scholar
  21. Ma Z, Tong Y, Li L, Giua A (2017b) Basis marking representation of Petri net reachability spaces and its application to the reachability problem. IEEE Trans Autom Control 62(3):1078–1093MathSciNetCrossRefzbMATHGoogle Scholar
  22. Model-Checkers for Net Condition/Event Systems (2007) Accessed Feb 2016
  23. Norman G, Parker D, Sproston J (2013) Model checking for probabilistic timed automata. Formal Methods Syst Design 43(2):164–190CrossRefzbMATHGoogle Scholar
  24. Preuße S, Lapp HC, Hanisch HM (2012) Closed-loop system modeling, validation, and verification. In: Proceedings of emerging technologies & factory automation, ETFA, Poland, pp 1–8Google Scholar
  25. PRISM 4.3 (2015) PRISM model checker. Accessed Sept 2016
  26. Ratzer AV et al (2003) CPN tools for editing, simulating, and analyzing coloured Petri nets. In: Applications and theory of Petri Nets 2003, Springer, Berlin, pp 450–462Google Scholar
  27. Salem MOB et al (2015a) ZiZo: Modeling, simulation and verification of reconfigurable real-time control tasks sharing adaptive resources-application to the medical project BROS. In: Proceedings of 8th international conference on health informatics, Portugal, pp 20–31Google Scholar
  28. Salem MOB, Mosbahi O, Khalgui M (2015b) PCP-based solution for resource sharing in reconfigurable timed net condition/event systems. In: Proceedings of adaptive discrete event control systems, ADECS, Tunisia, pp 52–67Google Scholar
  29. Salem MOB, Mosbahi O, Khalgui M, Jlalia Z, Frey G, Smida M (2016) BROMETH: methodology to design safe reconfigurable medical robotic systems. Int J Med Robot Comput Assist Surg. Google Scholar
  30. Shareef A, Zhu Y (2010) Energy modeling of wireless sensor nodes based on Petri nets. In: Proceedings of the 39th international conference on parallel processing, ICPP, San Diego, CA, pp 101–110Google Scholar
  31. Sharifloo AM, Spoletini P (2013) LOVER: light-weight formal verification of adaptive systems at run time. Springer, Berlin, pp 170–177Google Scholar
  32. Tong Y, Li Z, Giua A (2016) On the equivalence of observation structures for Petri net generators. IEEE Trans Autom Control 61(9):2448–2462MathSciNetCrossRefzbMATHGoogle Scholar
  33. Tong Y, Li ZW, Seatzu C, Giua A (2017) Verification of state-based opacity using Petri nets. IEEE Trans Autom Control 62(6):2823–2837MathSciNetCrossRefzbMATHGoogle Scholar
  34. Uzam M, Li ZW, Gelen G, Zakariyya RS (2016) A divideand-conquer-method for the synthesis of liveness enforcing supervisors for flexible manufacturing systems. J Intell Manuf 27(5):1111–1129CrossRefGoogle Scholar
  35. Wang X, Khemaissia I, Khalgui M, Li ZW, Mosbahi O, Zhou MC (2015) Dynamic low-power reconfiguration of real-time systems with periodic and probabilistic tasks. IEEE Trans Autom Sci Eng 12(1):258–271CrossRefGoogle Scholar
  36. Wang X, Li ZW, Wonham WM (2016) Dynamic multiple-period reconfiguration of real-time scheduling based on timed DES supervisory control. IEEE Trans Ind Inform 12(1):101–111Google Scholar
  37. Wu NQ, Zhou MC (2012a) Modeling, analysis and control of dual-arm cluster tools with residency time constraint and activity time variation based on Petri nets. IEEE Trans Autom Sci Eng 9(2):446–454CrossRefGoogle Scholar
  38. Wu NQ, Zhou MC (2012b) Schedulability analysis and optimal scheduling of dual-arm cluster tools with residency time constraint and activity time variation. IEEE Trans Autom Sci Eng 9(1):203–209MathSciNetCrossRefGoogle Scholar
  39. Wu NQ, Zhou MC, Li ZW (2015) Short-term scheduling of crude-oil operations: Petri net-based control-theoretic approach. IEEE Robot Autom Mag 22(2):64–76CrossRefGoogle Scholar
  40. Wu NQ, Zhou MC, Bai LP, Li ZW (2016) Short-term scheduling of crude oil operations in refinery with high-fusion-point oil and two transportation pipelines. Enterp Inf Syst 10(6):581–610CrossRefGoogle Scholar
  41. Ye JH, Li ZW, Giua A (2015) Decentralized supervision of Petri nets with a coordinator. IEEE Trans Syst Man Cybern Syst 45(6):955–966CrossRefGoogle Scholar
  42. Zhang J, Khalgui M, Li ZW, Mosbahi O, Abdulrahman MA (2013) R-TNCES: a novel formalism for reconfigurable discrete event control systems. IEEE Trans Syst Man Cybern Syst 43(4):757–772CrossRefGoogle Scholar
  43. Zhang S, Wu N, Li Z, Qu T, Li C (2017) Petri net-based approach to short-term scheduling of crude oil operations with less tank requirement. Inf Sci 417:247–261CrossRefGoogle Scholar
  44. Zhang H, Feng L, Wu N, Li Z (2018) Integration of learning-based testing and supervisory control for requirements conformance of black-box reactive systems. IEEE Trans Autom Sci Eng 15(1):2–15CrossRefGoogle Scholar

Copyright information

© Shiraz University 2018

Authors and Affiliations

  1. 1.School of Electrical and Information EngineeringJinan University (Zhuhai Campus)ZhuhaiChina
  2. 2.Institute of Automation and Energy SystemsSaarland UniversitySaarbrückenGermany
  3. 3.National Institute of Applied Sciences and Technology, University of CarthageTunisTunisia
  4. 4.Institute of Systems Engineering, Macau University of Science and TechnologyTaipaChina
  5. 5.School of Electro-Mechanical EngineeringXidian UniversityXi’anChina

Personalised recommendations