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 条
  • [31] FORMAL DESCRIPTION AND VERIFICATION OF PRODUCTION SYSTEMS
    LIU, NK
    DILLON, T
    INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS, 1995, 10 (04) : 399 - 442
  • [32] Formal Specification and Verification of CRDTs
    Zeller, Peter
    Bieniusa, Annette
    Poetzsch-Heffter, Arnd
    FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, 2014, 8461 : 33 - 48
  • [33] FORMAL FOUNDATION FOR SPECIFICATION AND VERIFICATION
    LAMPORT, L
    SCHNEIDER, FB
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 190 : 203 - 285
  • [34] A SOC-Based Formal Specification and Verification of Hybrid Systems
    Yu, Ning
    Wirsing, Martin
    RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES (WADT 2014), 2015, 9463 : 151 - 169
  • [35] Automated Formal Verification of the Refined Specification of Digital Systems in HSSL
    Maron, L.
    Macko, D.
    2016 INTERNATIONAL CONFERENCE ON EMERGING ELEARNING TECHNOLOGIES AND APPLICATIONS (ICETA), 2016,
  • [36] Formal Specification and Verification of a Data Replication Approach in Distributed Systems
    Souri, Alireza
    INTERNATIONAL JOURNAL OF NEXT-GENERATION COMPUTING, 2016, 7 (01): : 18 - 37
  • [37] A formal framework for context-aware systems specification and verification
    Djoudi, Brahim
    Bouanaka, Chafia
    Zeghib, Nadia
    JOURNAL OF SYSTEMS AND SOFTWARE, 2016, 122 : 445 - 462
  • [38] Formal Specification and Verification of Self-Adaptive Concurrent Systems
    Fakhir, Muhammad Ilyas
    Kazmi, Syed Asad Raza
    IEEE ACCESS, 2018, 6 : 34790 - 34803
  • [39] A formal approach for the specification, verification and control of flexible manufacturing systems
    Zairi, Sajeh
    Zouari, Belhassen
    Pitrac, Laurent
    ETFA 2007: 12TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOLS 1-3, 2007, : 1031 - +
  • [40] A Formal Security Framework for Mobile Agent Systems: Specification and Verification
    Loulou, Monia
    Kacem, Ahmed Hadj
    Mosbah, Mohamed
    Jmaiel, Mohamed
    CRISIS: 2008 THIRD INTERNATIONAL CONFERENCE ON RISKS AND SECURITY OF INTERNET AND SYSTEMS, PROCEEDINGS, 2008, : 69 - 76
12345