Specification and formal verification of temporal properties of production automation systems

被引：0
|
作者：
Flake, Stephan [1 ]
Müller, Wolfgang [1 ]
Pape, Ulrich [2 ]
Ruf, Jürgen [3 ]
机构：
[1] Universität Paderborn, Fürstenallee 11, 33102 Paderborn, Germany
[2] Heinz Nixdorf Institut, Fürstenallee 11, 33102 Paderborn, Germany
[3] IBM Deutschland Entwicklung GmbH, Schönaicher Str. 220, 71032 Böblingen, Germany
来源：
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2004年 / 3147卷
关键词：
Automatic guided vehicles - Formal verification - Semantics - Manufacture - Real time systems - Automation - Unified Modeling Language;
D O I：
10.1007/978-3-540-27863-4_13
中图分类号：
学科分类号：
摘要：
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. © Springer-Verlag Berlin Heidelberg 2004.
引用
收藏
页码：206 / 226
相关论文
共 50 条
  • [1] Specification and formal verification of temporal properties of production automation systems
    Flake, S
    Müller, W
    Pape, U
    Ruf, J
    INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 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