Synchronous-Reactive Semantic Modeling and Verification for Function Block Networks

被引：1
|
作者：
Li, Di [1 ]
Zhai, Zhenkun [1 ]
Pang, Zhibo [2 ]
Vyatkin, Valeriy [3 ,4 ]
Liu, Chengliang [5 ]
机构：
[1] South China Univ Technol, Sch Mech & Automot Engn, Guangzhou 510641, Guangdong, Peoples R China
[2] ABB Corp Res, S-72178 Vasteras, Sweden
[3] Aalto Univ, Dept Elect Engn & Automat, Espoo 02150, Finland
[4] Lulea Univ Technol, Dept Comp Sci Elect & Space Engn, S-97187 Lulea, Sweden
[5] Shanghai Jiao Tong Univ, Inst Mechatron, Shanghai 200240, Peoples R China
来源：
IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS | 2017年 / 13卷 / 06期
基金：
中国国家自然科学基金;
关键词：
IEC; 61499; modeling; scheduling; semantics; synchronous language; DISTRIBUTED AUTOMATION; EXECUTION;
D O I：
10.1109/TII.2017.2698606
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Owing to the semantic ambiguities, it has hindered the promotion of IEC 61499 in the field of industrial automation. In order to solve the thorny problem, this paper proposes an implementation scheme for performing formal modeling and simulation verification of semantics of functional block networks. Based on the synchrony hypothesis, the formal execution model is defined according to the fixed point semantics assuming that the behavior of a component functional block is monotonic. Subsequently, through specifying the evaluation of function blocks (FBs) as a process of solving the least- fixed point problem and transforming the network topology into a directed graph, a connectivity attenuation- based algorithm is put forward to ascertain the optimal scheduling policy of FBs with the minimum overhead. Finally, by conducting the experiment for an industrial application, the feasibility and validity of the presented implementation scheme is proved.
引用
收藏
页码：3389 / 3398
页数：10
相关论文
共 50 条
  • [1] Verification of Safety for Synchronous-Reactive System Using Bounded Model Checking
    Zhang, Xiaozhen
    Yang, Zhaoming
    Kong, Hui
    Kong, Weiqiang
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2023, 33 (06) : 885 - 932
  • [2] Formal Verification of Hierarchical Ptolemy II Synchronous-Reactive Models with Bounded Model Checking
    Zhang, Xiaozhen
    Yang, Zhaoming
    Kong, Hui
    Kong, Weiqiang
    2022 IEEE 22ND INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY, QRS, 2022, : 410 - 421
  • [3] Neutralizing Semantic Ambiguities of Function Block Architecture by Modeling with ASM
    Patil, Sandeep
    Dubinin, Victor
    Pang, Cheng
    Vyatkin, Valeriy
    PERSPECTIVES OF SYSTEM INFORMATICS, PSI 2014, 2015, 8974 : 76 - 91
  • [4] Compositional verification of synchronous networks
    Holenderski, L
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2000, 1926 : 214 - 227
  • [5] Quantitative reactive modeling and verification
    Henzinger, Thomas A.
    COMPUTER SCIENCE-RESEARCH AND DEVELOPMENT, 2013, 28 (04): : 331 - 344
  • [6] Modeling the Block Verification Time of Zcash
    Stiehle, Fabian
    Daniel, Erik
    Tschorsch, Florian
    2021 IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (EUROS&PW 2021), 2021, : 412 - 416
  • [7] Modeling and verification of reactive systems using Rebeca
    Sirjani, M
    Movaghar, A
    Shali, A
    de Boer, FS
    FUNDAMENTA INFORMATICAE, 2004, 63 (04) : 385 - 410
  • [8] Visual modeling and verification of distributed reactive systems
    Iqbal, A
    Bhattacharjee, AK
    Dhodapkar, SD
    Ramesh, S
    COMPUTER SAFETY, RELIABILITY, AND SECURITY, PROCEEDINGS, 2003, 2788 : 22 - 34
  • [9] Verification of Temporal Properties of Neuronal Archetypes Modeled as Synchronous Reactive Systems
    De Maria, Elisabetta
    Muzy, Alexandre
    Gaffe, Daniel
    Ressouche, Annie
    Grammont, Franck
    HYBRID SYSTEMS BIOLOGY, (HSB 2016), 2016, 9957 : 97 - 112
  • [10] MODELING SEMANTIC NETWORKS ON THE CONNECTION MACHINE
    CHUNG, SH
    MOLDOVAN, DI
    JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 1993, 17 (1-2) : 152 - 163
12345