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 条
  • [31] A SOC-Based Formal Specification and Verification of Hybrid Systems
    Yu, Ning
    Wirsing, Martin
    [J]. RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES (WADT 2014), 2015, 9463 : 151 - 169
  • [32] Formal Specification and Verification of a Data Replication Approach in Distributed Systems
    Souri, Alireza
    [J]. INTERNATIONAL JOURNAL OF NEXT-GENERATION COMPUTING, 2016, 7 (01): : 18 - 37
  • [33] Formal Specification and Verification of Self-Adaptive Concurrent Systems
    Fakhir, Muhammad Ilyas
    Kazmi, Syed Asad Raza
    [J]. IEEE ACCESS, 2018, 6 : 34790 - 34803
  • [34] Automated Formal Verification of the Refined Specification of Digital Systems in HSSL
    Maron, L.
    Macko, D.
    [J]. 2016 INTERNATIONAL CONFERENCE ON EMERGING ELEARNING TECHNOLOGIES AND APPLICATIONS (ICETA), 2016,
  • [35] A formal framework for context-aware systems specification and verification
    Djoudi, Brahim
    Bouanaka, Chafia
    Zeghib, Nadia
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2016, 122 : 445 - 462
  • [36] A formal approach for the specification, verification and control of flexible manufacturing systems
    Zairi, Sajeh
    Zouari, Belhassen
    Pitrac, Laurent
    [J]. ETFA 2007: 12TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOLS 1-3, 2007, : 1031 - +
  • [37] A Formal Security Framework for Mobile Agent Systems: Specification and Verification
    Loulou, Monia
    Kacem, Ahmed Hadj
    Mosbah, Mohamed
    Jmaiel, Mohamed
    [J]. CRISIS: 2008 THIRD INTERNATIONAL CONFERENCE ON RISKS AND SECURITY OF INTERNET AND SYSTEMS, PROCEEDINGS, 2008, : 69 - 76
  • [38] THE APPLICATION OF TEMPORAL LOGIC FOR THE SPECIFICATION AND VERIFICATION OF REACTIVE SYSTEMS
    PNUELI, A
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (01) : 301 - 302
  • [39] Formal verification of embedded logic controller specification with computer deduction in temporal logic
    Grobelna, Iwona
    [J]. PRZEGLAD ELEKTROTECHNICZNY, 2011, 87 (12A): : 47 - 50
  • [40] Formal Specification and Verification of an Extended Security Policy Model for Database Systems
    Hong, Zhu
    Yi, Zhu
    Li Chenyang
    Jie, Shi
    Ge, Fu
    Wang Yuanzhen
    [J]. APTC 2008: THIRD ASIA-PACIFIC TRUSTED INFRASTRUCTURE TECHNOLOGIES CONFERENCE, PROCEEDINGS, 2008, : 132 - 141
12345