diff --git a/models/Application_examples/First_Responder.mp b/models/Application_examples/First_Responder.mp index e6ff0e9876893069c861a32e21a99c605de08672..d0816a4f860da09c330a0cc46d39520bf31ba2a0 100644 --- a/models/Application_examples/First_Responder.mp +++ b/models/Application_examples/First_Responder.mp @@ -14,40 +14,40 @@ consequences of allowing or even encouraging bystanders to administer medication in an overdose scenario. This model is a draft snapshot of a high school student's -senior capstone project studying safety issues pertaining to -a proposed process for layperson administration of a rescue -medication called Narcan (Bryant 2016). It produces various -possible scenarios that could emerge based on the possible -actions of bystanders and first responders and their -interactions with the victim. The original analysis goal was -to determine the time savings in having bystanders prepared to -administer the rescue medication, but an unexpected behavior -was found among the generated a trace that neither student nor -mentor considered. For example, trace 6 prompted the idea to -modify the process to include the bystander marking the victim -to indicate the dose and time they administered while waiting -for the first responders. Being a work in progress, this model -is incomplete, but this version of it was archived in order to -capture the state of the model in which the unexpected emergent -behavior was first observed. +senior capstone project studying safety issues pertaining +to a proposed process for layperson administration of a +rescue medication called Narcan (Bryant 2016). It produces +various possible scenarios that could emerge based on the +possible actions of bystanders and first responders and +their interactions with the victim. The original analysis +goal was to determine the time savings in having bystanders +prepared to administer the rescue medication, but an +unexpected behavior was found among the generated a trace +that neither student nor mentor considered. For example, +trace 6 prompted the idea to modify the process to include +the bystander marking the victim to indicate the dose and +time they administered while waitingfor the first +responders. Being a work in progress, this modelis +incomplete, but this version of it was archived in order to +capture the state of the model in which the unexpected +emergent behavior was first observed. References: -Bryant, Jordan (2016). "Using Monterey Phoenix to analyze an -alternative process for administering Naloxone," mentored by -Kristin Giammarco (NPS) and Rick Schlegel (EMT). +Bryant, Jordan (2016). "Using Monterey Phoenix to analyze +an alternative process for administering Naloxone," +mentored by Kristin Giammarco (NPS) and Rick Schlegel (EMT). Available online: http://scienceandmathacademy.com/academics/srt4/student_work/2016/bryant_jordan.pdf -Giammarco, Kristin, and Kathleen Giles. "Verification and validation -of behavior models using lightweight formal methods." In Disciplinary -convergence in systems engineering research, pp. 431-447. Springer, -Cham, 2018. +Giammarco, Kristin, and Kathleen Giles. "Verification and +validation of behavior models using lightweight formal +methods." In Disciplinary convergence in systems engineering +research, pp. 431-447. Springer, Cham, 2018. Available online: https://calhoun.nps.edu/handle/10945/58237 -Search terms: behavior, first responder; -behavior, bystander; behavior, unexpected; -behavior, emergent +Search terms: behavior, first responder; behavior, +bystander; behavior, unexpected Instructions: Run for Scope 1. Scope 1: 8 traces in less than 1 sec. diff --git a/models/Application_examples/Small_Package_Delivery.mp b/models/Application_examples/Small_Package_Delivery.mp index 89de12c04ae27f3eedf4fd9f7302c11dd1d9553a..587c138bebfc04de00ef7047c68fcc2de25f1528 100644 --- a/models/Application_examples/Small_Package_Delivery.mp +++ b/models/Application_examples/Small_Package_Delivery.mp @@ -50,6 +50,8 @@ Scenario)" in Giammarco, K; Carlson, C., Blackburn, M. Specifications." Final Technical Report SERC-2018-TR-116; Systems Engineering Research Center: Hoboken, NJ, USA, 2018. +Available online: +https://apps.dtic.mil/sti/citations/AD1063328 Search terms: small package delivery; autonomous; ENSURE condition; probability, Type 1 diff --git a/models/Application_examples/Swarm_Search_and_Track.mp b/models/Application_examples/Swarm_Search_and_Track.mp index f74ab27792abe39e43c7d2b8006601785039810b..8aae4f82e35ba2535669341ca4d4c433f540f110 100644 --- a/models/Application_examples/Swarm_Search_and_Track.mp +++ b/models/Application_examples/Swarm_Search_and_Track.mp @@ -24,6 +24,13 @@ This MP model "Swarm_Search_and_Track.mp" incorporates Failure Modes and Failsafe Behaviors by elaborating on the "Perform_Mission" event in the MP model "Swarm_UAV.mp". +Giammarco, Kristin, and Kathleen Giles. "Verification and +validation of behavior models using lightweight formal +methods." In Disciplinary convergence in systems engineering +research, pp. 431-447. Springer, Cham, 2018. +Available online: +https://calhoun.nps.edu/handle/10945/58237 + Search terms: behavior, swarm; search and track; autonomous; behavior, environment; failure mode; behavior, failsafe; behavior, unexpected; behavior, emergent diff --git a/models/Application_examples/UAV_Ingress.mp b/models/Application_examples/UAV_Ingress.mp index b6250d535016d3c1f2f8a440ebe0c51ad8535aa2..fc58caf77dd5fdf9b4da562ee6cecc2d44fb8326 100644 --- a/models/Application_examples/UAV_Ingress.mp +++ b/models/Application_examples/UAV_Ingress.mp @@ -15,6 +15,13 @@ phase. Users may use this model to learn about forming relationships between roots using COORDINATE statements. References: +Giammarco, K; Carlson, C., Blackburn, M. +"Verification and Validation (V&V) of System Behavior +Specifications." Final Technical Report SERC-2018-TR-116; +Systems Engineering Research Center: Hoboken, NJ, +USA, 2018. +Available online: +https://apps.dtic.mil/sti/citations/AD1063328 Search terms: behavior, UAV ingress; autonomous; behavior, unexpected; behavior, emergent diff --git a/models/Application_examples/Unmanned_Spacecraft_Comms.mp b/models/Application_examples/Unmanned_Spacecraft_Comms.mp index d08c0e9b78ebab0d115952c8c67e32c4c0f1205d..7ff66676234271ad455fa8616e407c84c78e21d7 100644 --- a/models/Application_examples/Unmanned_Spacecraft_Comms.mp +++ b/models/Application_examples/Unmanned_Spacecraft_Comms.mp @@ -16,6 +16,12 @@ COORDINATE and SHARE ALL statements to mark relationships between roots. References: +Giammarco, Kristin, and Kathleen Giles. "Verification and +validation of behavior models using lightweight formal +methods." In Disciplinary convergence in systems engineering +research, pp. 431-447. Springer, Cham, 2018. +Available online: +https://calhoun.nps.edu/handle/10945/58237 Search terms: unmanned spacecraft; Heartbeat; communication; autonomous