Skip to content
Snippets Groups Projects
Commit 6ebab462 authored by Giammarco, Kristin M's avatar Giammarco, Kristin M
Browse files

Merge branch 'Pamela_Branch_2' into 'master'

Pamela's Merge Request: 07-09-2021

See merge request !20
parents 3ad5501e 88cac050
No related branches found
No related tags found
1 merge request!20Pamela's Merge Request: 07-09-2021
/* Model of Surgery /* Model of Surgery
Purpose:
Description:
Surgery example Surgery example
This model shows an example of decisions made by a leader (Physician), This model shows an example of decisions made by a leader (Physician),
a subordinate(s) (Nurse(s)), and the Environment as applied in a surgery a subordinate(s) (Nurse(s)), and the Environment as applied in a surgery
...@@ -11,6 +15,12 @@ Available at https://ieeexplore.ieee.org/abstract/document/7994952 ...@@ -11,6 +15,12 @@ Available at https://ieeexplore.ieee.org/abstract/document/7994952
Created by: J. Quartuccio (2017) Created by: J. Quartuccio (2017)
Naval Postgraduate School Naval Postgraduate School
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
/*Actors*/ /*Actors*/
......
/* Model of Swarm Search and Track /* Model of Swarm Search and Track
Purpose:
Description:
Michael Revill Michael Revill
22 February 2016 22 February 2016
Incorporating Failure Modes and Failsafe Behaviors Incorporating Failure Modes and Failsafe Behaviors
...@@ -15,6 +19,12 @@ Verb-oriented events in title case are states ...@@ -15,6 +19,12 @@ Verb-oriented events in title case are states
This model demonstrates the found unexpected behavior for This model demonstrates the found unexpected behavior for
object discovery after bingo fuel (trace 6) object discovery after bingo fuel (trace 6)
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA Swarm_Search_and_Track SCHEMA Swarm_Search_and_Track
......
/* Model of Swarm UAV /* Model of Swarm UAV
Kristin Giammarco and Mikhail Auguston Purpose:
Description:
Kristin Giammarco and Mikhail Auguston
MP Model based on "Swarm CONOPs" Draft 11 February 2015 MP Model based on "Swarm CONOPs" Draft 11 February 2015
11 February 2015 - Initial Model Started by KGiammarco 11 February 2015 - Initial Model Started by KGiammarco
25 May 2015 - M.Auguston Merged several COORDINATE, SHARE ALL to speed up 25 May 2015 - M.Auguston Merged several COORDINATE, SHARE ALL to speed up
...@@ -11,6 +15,12 @@ ...@@ -11,6 +15,12 @@
coordinated with external events (run for scopes 2 and 3 to see 2 and 3 UAVs, coordinated with external events (run for scopes 2 and 3 to see 2 and 3 UAVs,
respectively). respectively).
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA Swarm_UAV SCHEMA Swarm_UAV
......
/* Model of Turtles in the Desert /* Model of Turtles in the Desert
Purpose:
Description:
Example39 turtles.mp Example39 turtles.mp
Demonstration of the benefits for complete Demonstration of the benefits for complete
...@@ -25,7 +29,13 @@ Don't try to construct a non-Euclidean geometry to ...@@ -25,7 +29,13 @@ Don't try to construct a non-Euclidean geometry to
Here it is. Run for scope 1. Here it is. Run for scope 1.
There are 13 possible scenarios, and none when all three There are 13 possible scenarios, and none when all three
are telling the truth. are telling the truth.
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA Turtles SCHEMA Turtles
......
/* Model of UAV Ingress /* Model of UAV Ingress
Purpose:
Description:
UAV HADR Mission UAV HADR Mission
The following model specifies the ingress phase of the UAS HADR The following model specifies the ingress phase of the UAS HADR
...@@ -10,7 +14,13 @@ This model contains an unexpected behavior in which the UAV status ...@@ -10,7 +14,13 @@ This model contains an unexpected behavior in which the UAV status
is acceptable but the operator aborts the ingress (trace 2). is acceptable but the operator aborts the ingress (trace 2).
created by A. Constable May 2017 created by A. Constable May 2017
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA UAV_Ingress SCHEMA UAV_Ingress
......
/* Model of UAV On Station /* Model of UAV On Station
Purpose:
Description:
A Model for an Unmanned Aerial Vehicle in the OnStation Phase of an ISR Mission A Model for an Unmanned Aerial Vehicle in the OnStation Phase of an ISR Mission
Demonstrates use of concurrent events within a root and annotations with Demonstrates use of concurrent events within a root and annotations with
...@@ -13,7 +17,13 @@ Paper available at https://ieeexplore.ieee.org/abstract/document/7994950 ...@@ -13,7 +17,13 @@ Paper available at https://ieeexplore.ieee.org/abstract/document/7994950
modified by K.Giammarco on 02-04-2017 to remove normal events from failure mode scenarios modified by K.Giammarco on 02-04-2017 to remove normal events from failure mode scenarios
modified by K.Giammarco on 02-05-2017 to add normal events back to failure mode scenarios modified by K.Giammarco on 02-05-2017 to add normal events back to failure mode scenarios
and added annotations and added annotations
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA UAV_OnStation SCHEMA UAV_OnStation
......
/* Model of Unmanned Spacecraft Comms /* Model of Unmanned Spacecraft Comms
Purpose:
Description:
Heartbeat.mp Heartbeat.mp
October 4, 2015 October 4, 2015
Created by: C. Nelson Created by: C. Nelson
...@@ -9,8 +13,14 @@ through a frame counter called the "Heartbeat". This model represents ...@@ -9,8 +13,14 @@ through a frame counter called the "Heartbeat". This model represents
the behavior of the Heartbeat while a Spacecraft is approaching the behavior of the Heartbeat while a Spacecraft is approaching
the ISS. the ISS.
Run for scope 1 and up. Run for scope 1 and up.
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
/*————————————————————————————— /*—————————————————————————————
......
/* Model of Web Browser Formal Security /* Model of Web Browser Formal Security
Purpose:
Description:
Example 40. MP Web browsers formal security model. Example 40. MP Web browsers formal security model.
based on the papers by: based on the papers by:
...@@ -37,7 +41,13 @@ in order to model the vulnerabilities explained in the papers above. ...@@ -37,7 +41,13 @@ in order to model the vulnerabilities explained in the papers above.
This example borrowed from Daniel Jackson's paper demonstrates This example borrowed from Daniel Jackson's paper demonstrates
how MP can check whether Client's web query may how MP can check whether Client's web query may
be indirectly affected by Bad Server's Redirect intervention. be indirectly affected by Bad Server's Redirect intervention.
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA Web_browser SCHEMA Web_browser
......
/* Model of Wide Range Search for Wreckage and Survivors /* Model of Wide Range Search for Wreckage and Survivors
Purpose:
Description:
Example8_OperationalProcess.mp Example8_OperationalProcess.mp
modeling operational processes modeling operational processes
...@@ -24,7 +28,13 @@ produce more scenarios). Only one scenario is produced because no decision point ...@@ -24,7 +28,13 @@ produce more scenarios). Only one scenario is produced because no decision point
added to this model yet. added to this model yet.
The "Sequence" or "Swim Lanes" layouts are the most appropriate for browsing traces here. The "Sequence" or "Swim Lanes" layouts are the most appropriate for browsing traces here.
The "Sequence" mode yields views very similar to the UML or SysML Sequence Diagrams. The "Sequence" mode yields views very similar to the UML or SysML Sequence Diagrams.
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
......
/* Model of Work Productivity /* Model of Work Productivity
Purpose:
Description:
Example 26, timing attribute use Example 26, timing attribute use
also demonstrates how to print all also demonstrates how to print all
...@@ -8,6 +12,12 @@ Example 26, timing attribute use ...@@ -8,6 +12,12 @@ Example 26, timing attribute use
run for scopes 1 and up run for scopes 1 and up
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA Delays SCHEMA Delays
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment