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 条
  • [1] Compositional reasoning in model checking
    Berezin, S
    Campos, S
    Clarke, EM
    COMPOSITIONALITY: THE SIGNIFICANT DIFFERENCE, 1998, 1536 : 81 - 102
  • [2] An integration of model checking with automated proof checking
    Rajan, S
    Shankar, N
    Srivas, MK
    COMPUTER AIDED VERIFICATION, 1995, 939 : 84 - 97
  • [3] Conditional Commitments: Reasoning and Model Checking
    El Kholy, Warda
    Bentahar, Jamal
    El Menshawy, Mohamed
    Qu, Hongyang
    Dssouli, Rachida
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2014, 24 (02)
  • [4] Bounded model checking with description logic reasoning
    Ben-David, Shoham
    Trefler, Richard
    Weddell, Grant
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, PROCEEDINGS, 2007, 4548 : 60 - +
  • [5] Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning
    Bersani, Marcello M.
    Camilli, Matteo
    Lestingi, Livia
    Mirandola, Raffaela
    Rossi, Matteo
    2023 IEEE/ACM 11TH INTERNATIONAL CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING, FORMALISE, 2023, : 18 - 28
  • [6] Robust Boolean reasoning for equivalence checking and functional property verification
    Kuehlmann, A
    Paruthi, V
    Krohm, F
    Ganai, MK
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2002, 21 (12) : 1377 - 1394
  • [7] Quantum Structure in Cognition and the Foundations of Human Reasoning
    Aerts, Diederik
    Sozzo, Sandro
    Veloz, Tomas
    INTERNATIONAL JOURNAL OF THEORETICAL PHYSICS, 2015, 54 (12) : 4557 - 4569
  • [8] Quantum Structure in Cognition and the Foundations of Human Reasoning
    Diederik Aerts
    Sandro Sozzo
    Tomas Veloz
    International Journal of Theoretical Physics, 2015, 54 : 4557 - 4569
  • [9] Logic and cognition human - Performance in default reasoning
    Pelletier, FJ
    Elio, R
    IN THE SCOPE OF LOGIC: METHODOLOGY & PHILOSOPHY OF SCIENCE, 2002, 315 : 137 - 154
  • [10] Machine Knowledge and Human Cognition
    Li, Fashen
    Li, Lian
    Yin, Jianping
    Huang, Liang
    Zhou, Qingguo
    An, Ning
    Zhang, Yong
    Liu, Li
    Zhang, Jialin
    Kuang, Kun
    Yang, Lei
    Wu, Zhixi
    Yu, Lianchun
    BIG DATA MINING AND ANALYTICS, 2020, 3 (04): : 292 - 299