Increasing Dependability by Agent-Based Model-Checking During Run-Time

被引:0
|
作者
Rehberger, Sebastian [1 ]
Aicher, Thomas [1 ]
Vogel-Heuser, Birgit [1 ]
机构
[1] Tech Univ Munich, Inst Automat & Informat Syst, Munich, Germany
来源
SERVICE ORIENTATION IN HOLONIC AND MULTI-AGENT MANUFACTURING | 2016年 / 640卷
关键词
Automation production systems (aPS); Agents; Model-checking; Modelling; Verification; SYSTEMS;
D O I
10.1007/978-3-319-30337-6_15
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Agent-oriented software engineering (AOSE) is a paradigm for distributing intelligent control mechanisms (ICM) within an automated production system (aPS). Benefits resulting from AOSE have been surveyed in many applications as route-finding, plug-and-produce techniques and also in the control of Smart Grids. To ensure safe functionalities, i.e. dependability or uptime, of distributed technical systems for instance by conducting simulation, virtual commissioning, the execution of test cases and model-checking are commonly investigated in aPS during the design phase. In this paper we analyze an automatic diagnostic method to increase dependability by using model-checking during run-time, based on discretized models of the mechanical plant as well as models of the PLC software. Consequently the algorithm is incorporated into a software agent and logically coupled to a particular aPS module. Thus, the dependability for introducing novel product types, which have not been involved in the design process, could be increased. The evaluation of our approach is shown at a small lab-scale production system by searching for counter-examples of combinations with control actions and work piece (WP) types with modified mass, that may lead to a production halt.
引用
收藏
页码:159 / 167
页数:9
相关论文
共 50 条
  • [31] Combining real-time model-checking and fault tree analysis
    Schäfer, A
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 522 - 541
  • [32] MODEL-CHECKING OF LINEAR-TIME PROPERTIES IN POSSIBILISTIC KRIPKE STRUCTURE
    Li, Lijun
    Li, Yongming
    QUANTITATIVE LOGIC AND SOFT COMPUTING, 2012, 5 : 287 - 294
  • [33] A Model-Checking Approach for Fault Analysis Based on Configurable Model Extraction
    Ogawa, Hideto
    Ichii, Makoto
    Myojin, Tomoyuki
    Chikahisa, Masaki
    Nakagawa, Yuichiro
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2015, E98D (06): : 1150 - 1160
  • [34] Time Constrained Verification of Analog Circuits using Model-Checking Algorithms
    Grabowski, Darius
    Platte, Daniel
    Hedrich, Lars
    Barke, Erich
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 153 (03) : 37 - 52
  • [35] Model-checking trace-based information flow properties
    D'Souza, Deepak
    Holla, Raveendra
    Raghavendra, K. R.
    Sprick, Barbara
    JOURNAL OF COMPUTER SECURITY, 2011, 19 (01) : 101 - 138
  • [36] Model-checking distributed real-time systems with states, events, and multiple fairness assumptions
    Wang, F
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 553 - 567
  • [37] Architecture-Based Run-Time Fault Diagnosis
    Casanova, Paulo
    Schmerl, Bradley
    Garlan, David
    Abreu, Rui
    SOFTWARE ARCHITECTURE, 2011, 6903 : 261 - +
  • [38] Towards Model-Checking Security of Real-Time Java']Java Software
    Spalazzi, Luca
    Spegni, Francesco
    Liva, Giovanni
    Pinzger, Martin
    PROCEEDINGS 2018 INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING & SIMULATION (HPCS), 2018, : 642 - 649
  • [39] SMT-Based Symbolic Model-Checking for Operator Precedence Languages
    Chiari, Michele
    Geatti, Luca
    Gigante, Nicola
    Pradella, Matteo
    COMPUTER AIDED VERIFICATION, PT I, CAV 2024, 2024, 14681 : 387 - 408
  • [40] Model-checking of real-time systems: A telecommunications application - Experience report
    Alur, R
    Jagadeesan, LJ
    Kott, JJ
    VonOlnhausen, JE
    PROCEEDINGS OF THE 1997 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 1997, : 514 - 524