RoboChart: modelling and verification of the functional behaviour of robotic applications

被引:0
|
作者
Alvaro Miyazawa
Pedro Ribeiro
Wei Li
Ana Cavalcanti
Jon Timmis
Jim Woodcock
机构
[1] University of York,Department of Computer Science
[2] University of York,Department of Electronic Engineering
来源
Software & Systems Modeling | 2019年 / 18卷
关键词
State machines; Formal semantics; Process algebra; CSP; Model checking; Timed properties; Domain-specific language for robotics;
D O I
暂无
中图分类号
学科分类号
摘要
Robots are becoming ubiquitous: from vacuum cleaners to driverless cars, there is a wide variety of applications, many with potential safety hazards. The work presented in this paper proposes a set of constructs suitable for both modelling robotic applications and supporting verification via model checking and theorem proving. Our goal is to support roboticists in writing models and applying modern verification techniques using a language familiar to them. To that end, we present RoboChart, a domain-specific modelling language based on UML, but with a restricted set of constructs to enable a simplified semantics and automated reasoning. We present the RoboChart metamodel, its well-formedness rules, and its process-algebraic semantics. We discuss verification based on these foundations using an implementation of RoboChart and its semantics as a set of Eclipse plug-ins called RoboTool.
引用
收藏
页码:3097 / 3149
页数:52
相关论文
共 50 条
  • [11] Emotions modelling for safe behaviour generation in robotic systems
    Agate, R.
    Seward, D. W.
    Pace, C.
    SAFETY AND RELIABILITY FOR MANAGING RISK, VOLS 1-3, 2006, : 93 - 99
  • [12] Modelling, verification and investigation of behaviour of circular CFST columns
    Gupta, Pramod K.
    Khaudhair, Ziyad A.
    Ahuja, Ashok K.
    STRUCTURAL CONCRETE, 2014, 15 (03) : 340 - 349
  • [13] Modelling and verification of parameterized architectures: A functional approach
    Merniz, Salah
    Harous, Saad
    IET COMPUTERS AND DIGITAL TECHNIQUES, 2021, 15 (05): : 335 - 348
  • [14] Pharmacophore modelling: Methods, experimental verification and applications
    Ghose, AK
    Wendoloski, JJ
    PERSPECTIVES IN DRUG DISCOVERY AND DESIGN, 1998, 9-11 : 253 - 271
  • [15] Modelling the behaviour of Web applications with ArgoUWE
    Knapp, A
    Koch, N
    Zhang, GF
    WEB ENGINEERING, PROCEEDINGS, 2005, 3579 : 624 - 626
  • [16] Modelling Behaviour of Configurable VR Applications
    Walczak, Krzysztof
    INTERNATIONAL JOURNAL OF ARCHITECTURAL COMPUTING, 2009, 7 (01) : 77 - 103
  • [17] TRIP steel: Plastic behaviour modelling and influence on functional behaviour
    Thibaud, S.
    Boudeau, N.
    Gelin, J. C.
    JOURNAL OF MATERIALS PROCESSING TECHNOLOGY, 2006, 177 (1-3) : 433 - 438
  • [18] Verification of nanometre-scale modelling of tribofilm sliding behaviour
    Oesterle, W.
    Dmitriev, A. I.
    Orts-Gil, G.
    Schneider, T.
    Ren, H.
    Sun, X.
    TRIBOLOGY INTERNATIONAL, 2013, 62 : 155 - 162
  • [19] Teaching Functional Patterns through Robotic Applications
    Boender, J.
    Currie, E.
    Loomes, M.
    Primiero, G.
    Raimondi, F.
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (230): : 17 - 29
  • [20] Modelling and verification of IEC 61499 applications using Prolog
    Dubinin, Victor
    Vyatkin, Valeriy
    Hanisch, Hans-Michael
    2006 IEEE CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION, VOLS 1 -3, 2006, : 764 - +