A journal of IEEE and CAA , publishes high-quality papers in English on original theoretical/experimental research and development in all areas of automation
Advanced Search
Volume 8 Issue 4
Apr.  2021

IEEE/CAA Journal of Automatica Sinica

  • JCR Impact Factor: 15.3, Top 1 (SCI Q1)
    CiteScore: 23.5, Top 2% (Q1)
    Google Scholar h5-index: 77， TOP 5
Turn off MathJax
Article Contents
Article Navigation >  IEEE/CAA Journal of Automatica Sinica  > 2021  >  8(4): 905-915
Chuanliang Xia, Chengdong Li, "Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems," IEEE/CAA J. Autom. Sinica, vol. 8, no. 4, pp. 905-915, Apr. 2021. doi: 10.1109/JAS.2020.1003003
Citation: Chuanliang Xia, Chengdong Li, "Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems," IEEE/CAA J. Autom. Sinica, vol. 8, no. 4, pp. 905-915, Apr. 2021. doi: 10.1109/JAS.2020.1003003
shu

Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems

doi: 10.1109/JAS.2020.1003003
  • 1.

    School of Computer Science and Technology, Shandong Jianzhu University, Jinan 250101, China

  • 2.

    School of Information and Electrical Engineering, Shandong Jianzhu University, Jinan 250101, China

Funds:  This work was financially supported by the National Natural Science Foundation of China (61503220), the Natural Science Foundation of Shandong Province (ZR2016FM19), the Taishan Scholar Project of Shandong Province (TSQN201812092), the Key Research and Development Program of Shandong Province (2019GGX101072, 2019JZZY010115, 2018GGX106006), and the Youth Innovation Technology Project of Higher School in Shandong Province (2019KJN005)
More Information
    Abstract
  • Embedded systems have numerous applications in everyday life. Petri-net-based representation for embedded systems (PRES+) is an important methodology for the modeling and analysis of these embedded systems. For a large complex embedded system, the state space explosion is a difficult problem for PRES+ to model and analyze. The Petri net synthesis method allows one to bypass the state space explosion issue. To solve this problem, as well as model and analyze large complex systems, two synthesis methods for PRES+ are presented in this paper. First, the property preservation of the synthesis shared transition set method is investigated. The property preservation of the synthesis shared transition subnet set method is then studied. An abstraction-synthesis-refinement representation method is proposed. Through this representation method, the synthesis shared transition set approach is used to investigate the property preservation of the synthesis shared transition subnet set operation. Under certain conditions, several important properties of these synthetic nets are preserved, namely reachability, timing, functionality, and liveness. An embedded control system model is used as an example to illustrate the effectiveness of these synthesis methods for PRES+.

     

    • FullText(HTML)
  • loading
    • References(36)
  • [1]
    M. Ashjaei, N. Khalilzad, and S. Mubeen, “Modeling, designing and analyzing resource reservations in distributed embedded systems,” RealTime Modelling and Processing for Communication Systems. Springer, 2018, pp. 203–256.
    [2]
    L. A. Cortés, P. Eles, and Z. Peng, “Modeling and formal verification of embedded systems based on a Petri net representation,” J. Systems Architecture, vol. 49, no. 12, pp. 571–598, 2003.
    [3]
    S. Bandyopadhyay, K. Banerjee, D. Sarkar, and C. R. Mandal, “Translation validation for PRES+ models of parallel behaviours via an FSMD equivalence checker,” Progress in VLSI Design and Test. Springer, 2012, pp. 69–78.
    [4]
    D. Karlsson, P. Eles, and Z. Peng, “Model validation for embedded systems using formal method-aided simulation,” IET Computers &Digital Techniques, vol. 2, no. 6, pp. 413–433, 2008.
    [5]
    D. Karlsson, P. Eles, and Z. Peng, “Formal verification of componentbased designs,” Design Automation for Embedded Systems, vol. 11, no. 1, pp. 49–90, 2007. doi: 10.1007/s10617-006-9723-3
    [6]
    C. Xia, “Reduction rules for Petri net based representation for embedded systems,” J. Front. Comput. Sci. Technol, vol. 2, no. 6, pp. 614–626, 2008.
    [7]
    C. Xia, “Property preservation of refinement for Petri net based representation for embedded systems,” Cluster Computing, vol. 19, no. 3, pp. 1373–1384, 2016. doi: 10.1007/s10586-016-0597-2
    [8]
    C. Xia, B. Shen, H. Zhang, and Y. Wang, “Liveness and boundedness preservations of sharing synthesis of Petri net based representation for embedded systems,” Computer Systems Science and Engineering, vol. 33, no. 5, pp. 345–350, 2018.
    [9]
    J. Wang, Y. Deng, and M. Zhou, “Compositional time Petri nets and reduction rules,” IEEE Trans. Systems,Man,and Cybernetics,Part B, vol. 30, no. 4, pp. 562–572, 2000. doi: 10.1109/3477.865173
    [10]
    S. A. Shah, E. L. Bohez, K. Shah, I. ul Haq, K. Azam, and S. Anwar, “Colored Petri net model for significant reduction of invariants in flexible manufacturing systems,” Int. J. Advanced Manufacturing Technology, vol. 88, no. 5–8, pp. 1775–1787, 2017. doi: 10.1007/s00170-016-8864-1
    [11]
    P.-A. Bourdil, B. Berthomieu, S. Dal Zilio, and F. Vernadat, “Symmetry reduction for time Petri net state classes,” Science of Computer Programming, vol. 132, pp. 209–225, 2016. doi: 10.1016/j.scico.2016.08.008
    [12]
    J. Esparza, P. Hoffmann, and R. Saha, “Polynomial analysis algorithms for free choice probabilistic workflow nets,” Performance Evaluation, vol. 117, pp. 104–129, 2017. doi: 10.1016/j.peva.2017.09.006
    [13]
    B. Berthomieu, D. L. Botlan, and S. D. Zilio, “Petri net reductions for counting markings,” in Int. Symp. Model Checking Software, 2018.
    [14]
    S. M. Shatz, S. Tu, T. Murata, and S. Duri, “An application of Petri net reduction for ADA tasking deadlock analysis,” IEEE Trans. Parallel and Distributed Systems, vol. 7, no. 12, pp. 1307–1322, 1996. doi: 10.1109/71.553301
    [15]
    Y. Chen, Z. Li, K. Barkaoui, and M. Uzam, “New Petri net structure and its application to optimal supervisory control: interval inhibitor arcs,” IEEE Trans. Systems,Man,and Cybernetics:Systems, vol. 44, no. 10, pp. 1384–1400, 2014. doi: 10.1109/TSMC.2014.2307284
    [16]
    L. Salum, “Avoiding state explosion in a class of Petri nets,” Expert Systems with Applications, vol. 42, no. 1, pp. 519–526, 2015. doi: 10.1016/j.eswa.2014.07.037
    [17]
    Z. Ding, C. Jiang, M. Zhou, and Y. Zhang, “Preserving languages and properties in stepwise refinement-based synthesis of Petri nets,” IEEE Trans. Systems,Man,and Cybernetics-Part A:Systems and Humans, vol. 38, no. 4, pp. 791–801, 2008. doi: 10.1109/TSMCA.2008.923064
    [18]
    L. Bernardinello, E. Mangioni, and L. Pomello, “Local state refinement and composition of elementary net systems: An approach based on morphisms,” Trans. Petri Nets and Other Models of Concurrency VIII. Springer, 2013, pp. 48–70.
    [19]
    M. Khalgui, O. Mosbahi, Z. Li, and H.-M. Hanisch, “Reconfigurable multiagent embedded control systems: from modeling to implementation,” IEEE Trans. Computers, vol. 60, no. 4, pp. 538–551, 2010.
    [20]
    D.-E. Gratie and C. Gratie, “Composition colored Petri nets for the refinement of reaction-based models,” Electronic Notes in Theoretical Computer Science, vol. 326, pp. 51–72, 2016. doi: 10.1016/j.entcs.2016.09.018
    [21]
    P. Baldan, F. Bonchi, F. Gadducci, and G. V. Monreale, “Modular encoding of synchronous and asynchronous interactions using open Petri nets,” Science of Computer Programming, vol. 109, pp. 96–124, 2015. doi: 10.1016/j.scico.2014.11.019
    [22]
    J. Li, M. Zhou, and X. Dai, “Reduction and refinement by algebraic operations for Petri net transformation,” IEEE Trans. Systems,Man,and Cybernetics-Part A:Systems and Humans, vol. 42, no. 5, pp. 1244–1255, 2012. doi: 10.1109/TSMCA.2012.2186440
    [23]
    K. S. Cheung, T. Cheung, and K. Chow, “A Petri-net-based synthesis methodology for use-case-driven system design,” J. Systems and Software, vol. 79, no. 6, pp. 772–790, 2006. doi: 10.1016/j.jss.2005.06.018
    [24]
    M. Zhou, F. DiCesare, and A. A. Desrochers, “A hybrid methodology for synthesis of Petri net models for manufacturing systems,” IEEE Trans. Robotics and Automation, vol. 8, no. 3, pp. 350–361, 1992. doi: 10.1109/70.143353
    [25]
    H. Hu, R. Su, M. Zhou, and Y. Liu, “Polynomially complex synthesis of distributed supervisors for large-scale amss using Petri nets,” IEEE Trans. Control Systems Technology, vol. 24, no. 5, pp. 1610–1622, 2015.
    [26]
    E. Best and R. Devillers, “Characterisation of the state spaces of marked graph Petri nets,” Information and Computation, vol. 253, pp. 399–410, 2017. doi: 10.1016/j.ic.2016.06.006
    [27]
    A. A. Pouyan, H. T. Shandiz, and S. Arastehfar, “Synthesis a Petri net based control model for a FMS cell,” Computers in Industry, vol. 62, no. 5, pp. 501–508, 2011. doi: 10.1016/j.compind.2011.01.001
    [28]
    G. Liu, Z. Li, K. Barkaoui, and A. M. Al-Ahmari, “Robustness of deadlock control for a class of Petri nets with unreliable resources,” Information Sciences, vol. 235, pp. 259–279, 2013. doi: 10.1016/j.ins.2013.01.003
    [29]
    C. Xia, “Analysis of properties of petri synthesis net,” in Proc. Int. Conf. Theory and Applications of Models of Computation. Springer, 2006, pp. 576–587.
    [30]
    C. Xia, “Liveness and boundedness analysis of Petri net synthesis,” Mathematical Structures in Computer Science, vol. 24, no. 5, Article No. 2014.
    [31]
    D. Liu, Z. Li, and M. Zhou, “A parameterized liveness and ratioenforcing supervisor for a class of generalized Petri nets,” Automatica, vol. 49, no. 11, pp. 3167–3179, 2013. doi: 10.1016/j.automatica.2013.07.023
    [32]
    L. Jiao, T.-Y. Cheung, and W. Lu, “On liveness and boundedness of asymmetric choice nets,” Theoretical Computer Science, vol. 311, no. 1–3, pp. 165–197, 2004. doi: 10.1016/S0304-3975(03)00359-1
    [33]
    F. Basile, F. Caccavale, P. Chiacchio, J. Coppola, A. Marino, and D. Gerbasio, “Automated synthesis of hybrid Petri net models for robotic cells in the aircraft industry,” Control Engineering Practice, vol. 31, pp. 35–49, 2014. doi: 10.1016/j.conengprac.2014.05.008
    [34]
    F. Basile, R. Cordone, and L. Piroddi, “A branch and bound approach for the design of decentralized supervisors in Petri net models,” Automatica, vol. 52, pp. 322–333, 2015. doi: 10.1016/j.automatica.2014.12.004
    [35]
    Q. Hu, Y. Du, and S. Yu, “Service net algebra based on logic Petri nets,” Information Sciences, vol. 268, pp. 271–289, 2014. doi: 10.1016/j.ins.2013.10.014
    [36]
    S. Bandyopadhyay, D. Sarkar, and C. Mandal, “Equivalence checking of Petri net models of programs using static and dynamic cut-points,” Acta Informatica, vol. 56, no. 4, pp. 321–383, 2019. doi: 10.1007/s00236-018-0320-2
    • Related Articles
    • Supplements(0)

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(6)

    Get Citation
    PDF
    XML

    Article Metrics

    Article views (1218) PDF downloads(89) Cited by()

    Highlights

    • The property preservation of Petri net synthesis is investigated.
    • The synthesis shared transition subnet set approach is presented.
    • The abstraction-synthesis-refinement representation method is proposed.
    • The synthesis method is applied to the embedded control system.
    • The proposed two synthesis methods for PRES+ can bypass the state space explosion issue.

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return