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 条
  • [21] Efficient Model-Checking of Dense-Time Systems with Time-Convexity Analysis
    Wang, Farn
    RTSS: 2008 REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2008, : 195 - 205
  • [22] Profiling for Run-Time Checking of Computational Properties and Performance Debugging in Logic Programs
    Mera, Edison
    Trigo, Teresa
    Lopez-Garcia, Pedro
    Hermenegildo, Manuel
    PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, 2011, 6539 : 38 - +
  • [23] Model-checking algorithms for continuous-time Markov chains
    Baier, C
    Haverkort, B
    Hermanns, H
    Katoen, JP
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) : 524 - 541
  • [24] Branching-Time Model-Checking of Probabilistic Pushdown Automata
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 239 (0C) : 73 - 83
  • [25] Branching-time model-checking of probabilistic pushdown automata
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    Kucera, Antonin
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2014, 80 (01) : 139 - 156
  • [26] Model-Checking Linear-Time Properties of Quantum Systems
    Ying, Mingsheng
    Li, Yangjia
    Yu, Nengkun
    Feng, Yuan
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (03)
  • [27] Model checking agent-based communities against uncertain group commitments and knowledge
    Sultan, Khalid
    Bentahar, Jamal
    Yahyaoui, Hamdi
    Mizouni, Rabeb
    EXPERT SYSTEMS WITH APPLICATIONS, 2021, 177 (177)
  • [28] Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications
    Patil, Sandeep
    Drozdov, Dmitrii
    Dubinin, Victor
    Vyatkin, Valeriy
    TECHNOLOGICAL INNOVATION FOR CLOUD-BASED ENGINEERING SYSTEMS, 2015, 450 : 73 - 81
  • [29] ModelScope - Inspecting Executable Models during Run-time
    Graf, Philipp
    Mueller-Glaser, Klaus D.
    ICSE'08 PROCEEDINGS OF THE THIRTIETH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2008, : 935 - 936
  • [30] Evaluation of visual property specification languages based on practical model-checking experience
    Pakonen, Antti
    Buzhinsky, Igor
    Vyatkin, Valeriy
    JOURNAL OF SYSTEMS AND SOFTWARE, 2024, 216