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 条
  • [41] A formal approach for the specification and verification of trustworthy component-based systems
    Mohammad, Mubarak
    Alagar, Vangalur
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2011, 84 (01) : 77 - 104
  • [42] FORMAL SPECIFICATION AND VERIFICATION OF MULTIMEDIA SYSTEMS IN OPEN DISTRIBUTED-PROCESSING
    BLAIR, L
    BLAIR, G
    BOWMAN, H
    CHETWYND, A
    [J]. COMPUTER STANDARDS & INTERFACES, 1995, 17 (5-6) : 413 - 436
  • [43] Formal specification and verification of reusable communication models for distributed systems architecture
    Rouland, Quentin
    Hamid, Brahim
    Jaskolka, Jason
    [J]. FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2020, 108 : 178 - 197
  • [44] Formal specification and verification of hardware designs
    Ramesh, S
    Rao, SSSP
    Sivakumar, G
    Bhaduri, P
    [J]. PHOTOMASK AND X-RAY MASK TECHNOLOGY V, 1998, 3412 : 261 - 268
  • [45] A formal specification and verification of normative multi-agent systems by DisCSP
    Boudhaouia, Aida
    Mazigh, Belhassen
    Missaoui, Ezzine
    [J]. 2017 IEEE/ACS 14TH INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS (AICCSA), 2017, : 399 - 406
  • [46] Formal Verification of ABAP by Z Specification
    Rodruksa, Soravit
    Pradubsuwun, Denduang
    [J]. PROCEEDINGS OF 2017 14TH INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING (JCSSE), 2017,
  • [47] Formal specification and verification of a micropayment protocol
    Gouda, MG
    Liu, AX
    [J]. ICCCN 2004: 13TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS, 2004, : 489 - 494
  • [48] ON THE FORMAL SPECIFICATION AND VERIFICATION OF DIGITAL CIRCUITS
    DEGRAAF, PJ
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1990, 30 (1-5): : 537 - 544
  • [49] Formal Specification and Verification of Security Guidelines
    Zhioua, Zeineb
    Roudier, Yves
    Ameur, Rabea Boulifa
    [J]. 2017 IEEE 22ND PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC 2017), 2017, : 267 - 273
  • [50] Specification and Verification of Invariant Properties of Transition Systems
    Gaina, Daniel
    Tutu, Ionut
    Riesco, Adrian
    [J]. 2018 25TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2018), 2018, : 99 - 108
12345