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 条
  • [21] Formal Specification and Verification of Autonomous Robotic Systems: A Survey
    Luckcuck, Matt
    Farrell, Marie
    Dennis, Louise A.
    Dixon, Clare
    Fisher, Michael
    ACM COMPUTING SURVEYS, 2019, 52 (05)
  • [22] Formal Specification and Verification of Multi-Agent Systems
    Bourahla, Mustapha
    Benmohamed, Mohamed
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 123 : 5 - 17
  • [23] On the formal specification and verification of multi-agent systems
    Fisher, M
    Wooldridge, M
    INTERNATIONAL JOURNAL OF COOPERATIVE INFORMATION SYSTEMS, 1997, 6 (01) : 37 - 65
  • [24] FORMAL SPECIFICATION FOR DESIGN AUTOMATION
    LENART, M
    PADAWITZ, P
    PASZTOR, A
    FORMAL DESIGN METHODS FOR CAD, 1994, 18 : 201 - 220
  • [25] Specification and verification of reactive systems with temporal logic
    Fawzi, MG
    CARI'96 - PROCEEDINGS OF THE 3RD AFRICAN CONFERENCE ON RESEARCH IN COMPUTER SCIENCE, 1996, : 884 - 894
  • [26] Interactive formal specification for efficient preparation of intelligent automation systems
    Dahl, Martin
    Larsen, Christian
    Eros, Endre
    Bengtsson, Kristofer
    Fabian, Martin
    Falkman, Petter
    CIRP JOURNAL OF MANUFACTURING SCIENCE AND TECHNOLOGY, 2022, 38 : 129 - 138
  • [27] Specification of Temporal Properties of Functions for Runtime Verification
    Dawes, Joshua Heneage
    Reger, Giles
    SAC '19: PROCEEDINGS OF THE 34TH ACM/SIGAPP SYMPOSIUM ON APPLIED COMPUTING, 2019, : 2206 - 2214
  • [28] Specification of coordinated objects and verification of their temporal properties
    Danes, M
    Lucanu, D
    Ciobanu, G
    Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Proceedings, 2005, : 259 - 266
  • [29] Inference of Properties from Requirements and Automation of their Formal Verification
    Reich, Marina
    34TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2019), 2019, : 1222 - 1225
  • [30] Formal specification and verification of VHDL
    Bickford, M
    Jamsek, D
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 310 - 326
12345