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 条
  • [41] THE APPLICATION OF TEMPORAL LOGIC FOR THE SPECIFICATION AND VERIFICATION OF REACTIVE SYSTEMS
    PNUELI, A
    JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (01) : 301 - 302
  • [42] Formal verification of embedded logic controller specification with computer deduction in temporal logic
    Grobelna, Iwona
    PRZEGLAD ELEKTROTECHNICZNY, 2011, 87 (12A): : 47 - 50
  • [43] 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
    APTC 2008: THIRD ASIA-PACIFIC TRUSTED INFRASTRUCTURE TECHNOLOGIES CONFERENCE, PROCEEDINGS, 2008, : 132 - 141
  • [44] FORMAL SPECIFICATION AND VERIFICATION OF MULTIMEDIA SYSTEMS IN OPEN DISTRIBUTED-PROCESSING
    BLAIR, L
    BLAIR, G
    BOWMAN, H
    CHETWYND, A
    COMPUTER STANDARDS & INTERFACES, 1995, 17 (5-6) : 413 - 436
  • [45] A formal approach for the specification and verification of trustworthy component-based systems
    Mohammad, Mubarak
    Alagar, Vangalur
    JOURNAL OF SYSTEMS AND SOFTWARE, 2011, 84 (01) : 77 - 104
  • [46] Formal specification and verification of reusable communication models for distributed systems architecture
    Rouland, Quentin
    Hamid, Brahim
    Jaskolka, Jason
    FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2020, 108 : 178 - 197
  • [47] ON THE FORMAL SPECIFICATION AND VERIFICATION OF DIGITAL CIRCUITS
    DEGRAAF, PJ
    MICROPROCESSING AND MICROPROGRAMMING, 1990, 30 (1-5): : 537 - 544
  • [48] Formal Specification and Verification of Security Guidelines
    Zhioua, Zeineb
    Roudier, Yves
    Ameur, Rabea Boulifa
    2017 IEEE 22ND PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC 2017), 2017, : 267 - 273
  • [49] Formal Verification of ABAP by Z Specification
    Rodruksa, Soravit
    Pradubsuwun, Denduang
    PROCEEDINGS OF 2017 14TH INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING (JCSSE), 2017,
  • [50] Formal specification and verification of a micropayment protocol
    Gouda, MG
    Liu, AX
    ICCCN 2004: 13TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS, 2004, : 489 - 494
12345