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

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–271 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–81 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–1467 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–540 Bouyer P (2007) Model-checking timed temporal logics. In: Proceedings of the 5th workshop on methods for modalities, France, pp 323–341 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–402 Chen YF, Li ZW, Barkaoui K, Giua A (2015) On the enforcement of a class of nonlinear constraints on Petri nets. Automatica 55:116–124 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–263 Cong X, Fanti MP, Mangini AM, Li ZW (2017) Decentralized diagnosis by Petri nets and integer linear programming. IEEE Trans Syst Man Cybern Syst. https://doi.org/10.1109/tsmc.2017.2726108 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–374 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–113 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–14 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–396 Heydari A, Landers RG, Balakrishnan SN (2014) Optimal control approach for turning process planning optimization. IEEE Trans Contol Syst Technol 22(4):1337–1349 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–474 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–380 Kopetz H (2003) Time-triggered real-time computing. Ann Rev Control 27(1):3–13 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–191 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–4153 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–1341 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–1093 Model-Checkers for Net Condition/Event Systems (2007) http://www.vyatkin.org/tools/modelchekers.html. Accessed Feb 2016 Norman G, Parker D, Sproston J (2013) Model checking for probabilistic timed automata. Formal Methods Syst Design 43(2):164–190 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–8 PRISM 4.3 (2015) PRISM model checker. http://www.prismmodelchecker.org/. Accessed Sept 2016 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–462 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–31 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–67 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. https://doi.org/10.1002/rcs.1786 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–110 Sharifloo AM, Spoletini P (2013) LOVER: light-weight formal verification of adaptive systems at run time. Springer, Berlin, pp 170–177 Tong Y, Li Z, Giua A (2016) On the equivalence of observation structures for Petri net generators. IEEE Trans Autom Control 61(9):2448–2462 Tong Y, Li ZW, Seatzu C, Giua A (2017) Verification of state-based opacity using Petri nets. IEEE Trans Autom Control 62(6):2823–2837 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–1129 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–271 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–111 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–454 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–209 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–76 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–610 Ye JH, Li ZW, Giua A (2015) Decentralized supervision of Petri nets with a coordinator. IEEE Trans Syst Man Cybern Syst 45(6):955–966 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–772 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–261 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–15