Model Checking Functional Integration of Human Cognition and Machine Reasoning

被引:0
|
作者
Mercer, Eric [1 ]
Butler, Keith [2 ]
Bahrami, Ali [3 ]
机构
[1] Brigham Young Univ, Provo, UT 84602 USA
[2] Univ Washington, Seattle, WA 98195 USA
[3] Bionous LLC, Kirkland, WA USA
关键词
Cognitive Modeling; Business Process Modeling; Model Checking; Model-Based Validation; SPIN; Linear Temporal Logic; COVID-19;
D O I
10.1109/SysCon53536.2022.9773873
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Functional integration of human cognition and machine reasoning is an industry-wide problem where failure risks health or safety. Differences in human versus machine functioning obscure conventional integration. We introduce cognitive work problems (CWP) for rigorous, verifiable functional integration. CWP specify the cognitive problem that integrated designs must solve. They are technology-neutral, abstract work objects, allowing people and computing to share and transform them in coordination. The end-to-end method is illustrated on a system that employs AI for remote patient monitoring (RPM) during COVID-19 home care. The CWP specified actionable risk awareness as the medical problem RPM must solve. Graphical modeling standards enabled user participation: CWP as finite state machines and system behavior in BPMN. For model checking, the CWPs logical content was translated to linear temporal logic (LTL) and the BPMN into Promela as inputs to the SPIN model checker. SPIN verified the Promela implements the LTL correctly. We conclude this CWP-derived RPM design solves the medical problem and enhances patient safety. The method appears general to many critical systems.
引用
收藏
页数:8
相关论文
共 50 条
  • [31] Estimating functional coverage in bounded model checking
    Grosse, Daniel
    Kuehne, Ulrich
    Drechsler, Rolf
    2007 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION, VOLS 1-3, 2007, : 1176 - 1181
  • [32] Analyzing functional coverage in bounded model checking
    Grosse, Daniel
    Kuehne, Ulrich
    Drechsler, Rolf
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2008, 27 (07) : 1305 - 1314
  • [33] Comparing model checking and logical reasoning for real-time systems
    Dierks, H
    FORMAL ASPECTS OF COMPUTING, 2004, 16 (02) : 104 - 120
  • [34] Modelling human cognition of abnormal machine behaviour
    Prasanna Illankoon
    Phillip Tretten
    Uday Kumar
    Human-Intelligent Systems Integration, 2019, 1 (1) : 3 - 26
  • [35] COMPUTER WORKSTATIONS - EXPLORATIONS IN HUMAN AND MACHINE COGNITION
    LACHMAN, R
    BEHAVIOR RESEARCH METHODS INSTRUMENTS & COMPUTERS, 1990, 22 (02): : 202 - 207
  • [36] SpaceWire State Machine Verification Based on Model Checking
    Dai, Zhiquan
    Guan, Yong
    Jin, Shengzhen
    Shi, Zhiping
    Li, Xiaojuan
    Zhang, Jie
    RECENT TRENDS IN MATERIALS AND MECHANICAL ENGINEERING MATERIALS, MECHATRONICS AND AUTOMATION, PTS 1-3, 2011, 55-57 : 2192 - +
  • [37] Temporal Logic Model Checking via Probe Machine
    Zhu, Weijun
    Li, En
    Yang, Xiaoyu
    PROCEEDINGS OF 2020 IEEE 4TH INFORMATION TECHNOLOGY, NETWORKING, ELECTRONIC AND AUTOMATION CONTROL CONFERENCE (ITNEC 2020), 2020, : 623 - 626
  • [38] Model Checking Assembly Code of an Industrial Knitting Machine
    Reinbacher, Thomas
    Horauer, Martin
    Schlich, Bastian
    Brauer, Joerg
    Scheuer, Florian
    PROCEEDINGS OF THE 2009 FOURTH INTERNATIONAL CONFERENCE ON EMBEDDED AND MULTIMEDIA COMPUTING, 2009, : 97 - +
  • [39] Brain shape and human variation: from integration to cognition
    Bruner, Emiliano
    Martin-Loeches, Manuel
    Colom, Roberto
    AMERICAN JOURNAL OF PHYSICAL ANTHROPOLOGY, 2010, : 73 - 74
  • [40] A lightweight integration of theorem proving and model checking for system verification
    Kong, WQ
    Ogata, K
    Seino, T
    Futatsugi, K
    12th Asia-Pacific Software Engineering Conference, Proceedings, 2005, : 59 - 66