Specification and formal verification of temporal properties of production automation systems

被引：0
|
作者：
Flake, S
Müller, W
Pape, U
Ruf, J
机构：
[1] Univ Paderborn, D-33102 Paderborn, Germany
[2] Heinz Nixdorf Inst, D-33102 Paderborn, Germany
[3] IBM Deutschland Entwicklung GmbH, D-71032 Boblingen, Germany
来源：
INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING | 2004年 / 3147卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This article describes our approach for the specification and verification of production automation systems with real-time properties. We focus on the graphical MFERT notation and RT-OCL (Real-Time Object Constraint Language) for the specification of state-oriented real-time properties. RT-OCL is an extension of the Object Constraint Language (OCL) that is part of the Unified Modeling Language (UML). We introduce the formal semantics of RT-OCL based on a formal model of UML Class and State Diagrams and provide a mapping to temporal logics. The applicability of our approach is demonstrated by the case study of a manufacturing system with automated guided vehicles.
引用
收藏
页码：206 / 226
页数：21
相关论文
共 50 条
  • [1] Specification and formal verification of temporal properties of production automation systems
    Flake, Stephan
    Müller, Wolfgang
    Pape, Ulrich
    Ruf, Jürgen
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2004, 3147 : 206 - 226
  • [2] Specification and formal verification of safety properties in a point automation system
    Sener, Ibrahim
    Kaymakci, Ozgur Turay
    Ustoglu, Ilker
    Cansever, Galip
    TURKISH JOURNAL OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCES, 2016, 24 (03) : 1384 - 1396
  • [3] Modeling and formal verification of production automation systems
    Ruf, Jürgen
    Weiss, Roland J.
    Kropf, Thomas
    Rosenstiel, Wolfgang
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2004, 3147 : 541 - 566
  • [4] Modeling and formal verification of production automation systems
    Ruf, J
    Weiss, RJ
    Kropf, T
    Rosenstiel, W
    INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 541 - 566
  • [5] Formal Technical Process Specification and Verification for Automated Production Systems
    Hackenberg, Georg
    Campetelli, Alarico
    Legat, Christoph
    Mund, Jakob
    Teufl, Sabine
    Vogel-Heuser, Birgit
    SYSTEM ANALYSIS AND MODELING: MODELS AND REUSABILITY, 2014, 8769 : 287 - +
  • [6] A formal technique for the specification and verification of distributed systems and its application in manufacturing automation
    Fialho, SV
    Leao, JLS
    Pedroza, ACP
    38TH MIDWEST SYMPOSIUM ON CIRCUITS AND SYSTEMS, PROCEEDINGS, VOLS 1 AND 2, 1996, : 27 - 30
  • [7] Formal specification method for systems automation
    Petin, Jean-Francois
    Morel, Gerard
    Panetto, Herve
    EUROPEAN JOURNAL OF CONTROL, 2006, 12 (02) : 115 - 130
  • [8] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    MICROPROCESSING AND MICROPROGRAMMING, 1988, 24 (1-5): : 371 - 378
  • [9] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    INTEGRATION-THE VLSI JOURNAL, 1989, 7 (03) : 247 - 266
  • [10] FORMAL TECHNIQUES FOR SYSTEMS SPECIFICATION AND VERIFICATION
    CARMO, J
    SERNADAS, A
    INFORMATION SYSTEMS, 1991, 16 (03) : 245 - 272
12345