scholarly journals Generating Erroneous Human Behavior From Strategic Knowledge in Task Models and Evaluating Its Impact on System Safety With Model Checking

2013 ◽  
Vol 43 (6) ◽  
pp. 1314-1327 ◽  
Author(s):  
Matthew L. Bolton ◽  
Ellen J. Bass
Keyword(s):  
Model Checking ◽  
Human Behavior ◽  
Strategic Knowledge ◽  
System Safety

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.

System safety assessment based on STPA and model checking

2018 ◽  
Vol 109 ◽  
pp. 130-143 ◽  
Author(s):  
Alheri Longji Dakwat ◽  
Emilia Villani
Keyword(s):  
Model Checking ◽  
Safety Assessment ◽  
System Safety

A formal method for assessing the impact of task-based erroneous human behavior on system safety

2019 ◽  
Vol 188 ◽  
pp. 168-180 ◽  
Author(s):  
Matthew L. Bolton ◽  
Kylie A. Molinaro ◽  
Adam M. Houser
Keyword(s):  
Human Behavior ◽  
Formal Method ◽  
System Safety ◽  
The Impact

scholarly journals Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games

Electronics ◽  
2019 ◽  
Vol 8 (2) ◽  
pp. 212 ◽  
Author(s):  
Xiaomin Wei ◽  
Yunwei Dong ◽  
Pengpeng Sun ◽  
Mingrui Xiao
Keyword(s):  
Model Checking ◽  
Stochastic Games ◽  
Safety Analysis ◽  
Cyber Physical Systems ◽  
System Level ◽  
Probabilistic Model Checking ◽  
Critical Systems ◽  
System Safety ◽  
Physical Systems ◽  
Analysis And Design

As safety-critical systems, grid cyber-physical systems (GCPSs) are required to ensure the safety of power-related systems. However, in many cases, GCPSs may be subject to uncertain and nondeterministic environmental hazards, as well as the variable quality of devices. They can cause failures and hazards in the whole system and may jeopardize system safety. Thus, it necessitates safety analysis for system safety assurance. This paper proposes an architecture-level safety analysis approach for GCPSs applying the probabilistic model-checking of stochastic games. GCPSs are modeled using Architecture Analysis and Design Language (AADL). Random errors and failures of a GCPS and nondeterministic environment behaviors are explicitly described with AADL annexes. A GCPS AADL model including the environment can be regarded as a game. To transform AADL models to stochastic multi-player games (SMGs) models, model transformation rules are proposed and the completeness and consistency of rules are proved. Property formulae are formulated for formal verification of GCPS SMG models, so that occurrence probabilities of failed states and hazards can be obtained for system-level safety analysis. Finally, a modified IEEE 9-bus system with grid elements that are power management systems is modeled and analyzed using the proposed approach.

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