Using task analytic models and phenotypes of erroneous human behavior to discover system failures using model checking

2010 ◽  
Author(s):  
Matthew L. Bolton ◽  
Ellen J. Bass
Keyword(s):  
Model Checking ◽  
Human Behavior ◽  
System Failures ◽  
Analytic Models

A Method for the Formal Verification of Human-interactive Systems

2009 ◽  
Vol 53 (12) ◽  
pp. 764-768 ◽  
Author(s):  
Matthew L Bolton ◽  
Ellen J. Bass
Keyword(s):  
Model Checking ◽  
Human Behavior ◽  
Interactive Systems ◽  
Formal Models ◽  
Operational Environment ◽  
Patient Controlled Analgesia ◽  
Operational Conditions ◽  
Analytic Models ◽  
Human Device

Predicting failures in complex, human-interactive systems is difficult as they may occur under rare operational conditions and may be influenced by many factors including the system mission, the human operator's behavior, device automation, human-device interfaces, and the operational environment. This paper presents a method that integrates task analytic models of human behavior with formal models and model checking in order to formally verify properties of human-interactive systems. This method is illustrated with a case study: the programming of a patient controlled analgesia pump. Two specifications, one of which produces a counterexample, illustrate the analysis and visualization capabilities of the method.

A model checking approach for user relationship management in the social network

Kybernetes ◽  
2019 ◽  
Vol 48 (3) ◽  
pp. 407-423 ◽  
Author(s):  
Alireza Souri ◽  
Monire Nourozi ◽  
Amir Masoud Rahmani ◽  
Nima Jafari Navimipour
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Human Behavior ◽  
Social Systems ◽  
Relationship Management ◽  
Model Analysis ◽  
Statistical Testing ◽  
Behavior Model ◽  
Content Type ◽  
The Social

Purpose The purpose of this paper is to describe how formal verification strategies have been utilized to assess the correctness of Knowledge Creation Process (KCP) in the social systems. This paper analyzes a User Relationship Management (URM) approach in term of human behavior connection in the social systems. A formal framework is displayed for the URM which consolidates behavioral demonstrating strategy. Design/methodology/approach Evaluating the human behavior interactions is an important matter in the social systems. For this analysis, formal verification is an essential section in the complex information systems development. Model checking results satisfied the logical problems in the proposed behavior model analysis. Findings Model checking results represent satisfaction of the logical problems in the proposed behavior model analysis. In the statistical testing, the proposed URM mechanism supported KCP conditions. Also, the percentage of state reachability in the URM with KCP conditions is higher than the URM mechanism without supporting KCP conditions. Originality/value The model checking results show that the proposed URM mechanism with supporting the KCP conditions satisfies comprehensively behavioral interactions rather than the mechanism without KCP conditions in the social networks.

Sign in / Sign up

Export Citation Format

Share Document