diff --git a/Application_examples/Spiral_Software_Process b/Application_examples/Spiral_Software_Process index bfb3c669c2188a23d5178c05fa671de06c5ade80..dbc90e8e9e3f59aef5576a6b30a73867f39b807f 100644 --- a/Application_examples/Spiral_Software_Process +++ b/Application_examples/Spiral_Software_Process @@ -6,7 +6,7 @@ Author credits: Purpose: -Users may use this model to learn about SHARE ALL usage to make connections +This model demonstrates the usage of shared events to model the spiral software process to develop a prototype and release a product. Users may use this model to learn about SHARE ALL usage to make connections between roots. Description: diff --git a/Application_examples/Surgery.mp b/Application_examples/Surgery.mp index 8a0458e9b2d25285c6d1f889f2eca8441c3adbda..b9158b055de8ee7ca9b65e0c84753ad2f3f163f1 100644 --- a/Application_examples/Surgery.mp +++ b/Application_examples/Surgery.mp @@ -1,22 +1,30 @@ /* Model of Surgery +Author credits: + +Created by J. Quartuccio (2017) +Naval Postgraduate School + Purpose: +This model demonstrates decisionmaking in a system with several actors +capable of making choices that could effect the situation. Users may +reference this model to learn about using ENSURE and COORDINATE statements +to constrain a model and how to make a decision structure. + Description: Surgery example 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 setting. + +References: + "Identifying decision patterns using Monterey Phoenix" by Quartuccio, John, Kristin Giammarco, and Mikhail Auguston. Available at https://ieeexplore.ieee.org/abstract/document/7994952 -Created by: J. Quartuccio (2017) -Naval Postgraduate School - -References: - Search terms: Instructions: diff --git a/Application_examples/Swarm_Search_and_Track.mp b/Application_examples/Swarm_Search_and_Track.mp index f11628085cb0ceb62d31fd732591e474cbf4b656..8cd36799094a4550c51dcf08b0382c011b672366 100644 --- a/Application_examples/Swarm_Search_and_Track.mp +++ b/Application_examples/Swarm_Search_and_Track.mp @@ -1,16 +1,25 @@ /* Model of Swarm Search and Track +Author credits: + +Created by Michael Revill on the 22nd of February, 2016 +Edited by K.Giamamrco on the 26th of February, 2016 + Purpose: +This model demonstrates using a decision structure to +model a UAV drone's target aquisition. Users may +reference this model to learn about COORDINATE statements +and or blocks when automatically generating traces with +connections between roots. + Description: -Michael Revill -22 February 2016 Incorporating Failure Modes and Failsafe Behaviors MP model Swarm_Search_and_Track elaborates on "Perform_Mission" event in Swarm2-v8.mp -Edited by K.Giamamrco on 26 Feb 2016 + Established naming convention: Noun-oriented events are actors (root events) Verb-oriented events in sentence case are activities diff --git a/Application_examples/Swarm_UAV.mp b/Application_examples/Swarm_UAV.mp index 4e3e7b58246a67c018e2cdc3eacfc74303ab2c3e..83c4a8abf03de87d10198e5a51202f2386a55dc9 100644 --- a/Application_examples/Swarm_UAV.mp +++ b/Application_examples/Swarm_UAV.mp @@ -1,19 +1,24 @@ /* Model of Swarm UAV +Author credits: + +Kristin Giammarco and Mikhail Auguston +MP Model based on "Swarm CONOPs" Draft 11 February 2015 +11 February 2015 - Initial Model Started by KGiammarco +25 May 2015 - M.Auguston Merged several COORDINATE, SHARE ALL to speed up +trace generation +22 July 2015 - added a few more coordinate statements to capture dependencies + Purpose: -Description: +This model demonstrates using itteration to model multiple drones with similar +duties. Users may reference this model as an example of using itteration to make +multiple "roots" and connecting them with COORDINATE statements. -Kristin Giammarco and Mikhail Auguston - MP Model based on "Swarm CONOPs" Draft 11 February 2015 - 11 February 2015 - Initial Model Started by KGiammarco - 25 May 2015 - M.Auguston Merged several COORDINATE, SHARE ALL to speed up - trace generation - 22 July 2015 - added a few more coordinate statements to capture dependencies +Description: - This model demonstrates how to get several instances of the same actor (UAV) - coordinated with external events (run for scopes 2 and 3 to see 2 and 3 UAVs, - respectively). +This model demonstrates how to get several instances of the same actor (UAV) +coordinated with external events References: @@ -21,6 +26,8 @@ Search terms: Instructions: +Run for scopes 2 and 3 to see 2 and 3 UAVs, respectively. + ==========================================================*/ SCHEMA Swarm_UAV diff --git a/Application_examples/Turtles_in_the_Desert.mp b/Application_examples/Turtles_in_the_Desert.mp index d8152e7c80f8fdee596a7fcaba1fa7ed2282ff14..2e27b379e55a7235a1c48521fc06426932b69b04 100644 --- a/Application_examples/Turtles_in_the_Desert.mp +++ b/Application_examples/Turtles_in_the_Desert.mp @@ -1,7 +1,15 @@ /* Model of Turtles in the Desert +Author credits: + + + Purpose: +This model demonstrates using MP to solve a logic puzzle with exhaustive trace +generation. Users may use this model as an example of using IF, ENSURE, and +BUILD statements to constrain models as logical problem solving tools. + Description: Example39 turtles.mp @@ -9,7 +17,6 @@ Example39 turtles.mp Demonstration of the benefits for complete example set generation in MP. - Three turtles are moving on a desert plain, all in the same direction. The first has been asked: "What do you see?" It answered: "I see nobody before me and two turtles behind." The second turtle has been diff --git a/Application_examples/UAV_Ingress.mp b/Application_examples/UAV_Ingress.mp index 08097bc880eda38767e36a702d7b919d1f360860..9a011aa8d3a5ab341449746f0a9ba986bc4194a8 100644 --- a/Application_examples/UAV_Ingress.mp +++ b/Application_examples/UAV_Ingress.mp @@ -1,7 +1,16 @@ /* Model of UAV Ingress +Author credits: + +Created by A. Constable May 2017 + Purpose: +This model demonstrates a coordinated UAV flight scenario with +multiple teams involved in making the launch and flight happen. +Users may use this model to learn aobut forming relationships +between roots using COORDINATE statements. + Description: UAV HADR Mission @@ -12,8 +21,6 @@ phase, and followed by the on-station phase. This model contains an unexpected behavior in which the UAV status is acceptable but the operator aborts the ingress (trace 2). - - created by A. Constable May 2017 References: diff --git a/Application_examples/UAV_OnStation.mp b/Application_examples/UAV_OnStation.mp index 449c96135b09150472284096ad7c2b97dc7065f4..e81ee185b33dfd82b96af77ed2c63b18d0061162 100644 --- a/Application_examples/UAV_OnStation.mp +++ b/Application_examples/UAV_OnStation.mp @@ -1,25 +1,29 @@ /* Model of UAV on Station +Author credits: + +Created by K.Giammarco on the 3rd of February, 2017 +Modified by K.Giammarco on the 4th of February, 2017 to remove normal events from failure mode scenarios +Modified by K.Giammarco on the 5th of February, 2017 to add normal events back to failure mode scenarios +and added annotations + Purpose: +This model demonstrates the use of concurrent events within a root and annotations +with SAY and MARK in order to improve the clarity of the model. Users may use this +model as an example of COORDINATE, IF, and MARK statement usage in order to generate +"stories" for traces automatically. + Description: 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 -SAY and MARK +References: "Comprehensive use case scenario generation: An approach for modeling system of systems behaviors" by Kristin Giammarco, Kathleen Giles, and Clifford A. Whitcomb Paper available at https://ieeexplore.ieee.org/abstract/document/7994950 - created by K.Giammarco on 02-03-2017 - 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 - and added annotations - -References: - Search terms: Instructions: diff --git a/Application_examples/Unmanned_Spacecraft_Comms.mp b/Application_examples/Unmanned_Spacecraft_Comms.mp index 82332ac90ce60f7c83f82b2472b02c0c2e0b9f0f..c231281c1a38784d0563d6fd4efbe2766d02609d 100644 --- a/Application_examples/Unmanned_Spacecraft_Comms.mp +++ b/Application_examples/Unmanned_Spacecraft_Comms.mp @@ -1,12 +1,19 @@ /* Model of Unmanned Spacecraft Comms +Author credits: + +Created by C. Nelson on the 4th of October, 2015 + Purpose: +This model demonstrates using MP to model communications between a +spacecraft and a station. Users may reference this model as an example +of using COORDINATE and SHARE ALL statements to mark relationships +between roots. + Description: Heartbeat.mp -October 4, 2015 -Created by: C. Nelson The communication link between a spacecraft and the ISS is monitored through a frame counter called the "Heartbeat". This model represents diff --git a/Application_examples/Web_Browser_Formal_Security.mp b/Application_examples/Web_Browser_Formal_Security.mp index c64a6b35009af295940bdb7095e996701a004811..72b95dc52186ae36f05023a4da4634d01c94d3a8 100644 --- a/Application_examples/Web_Browser_Formal_Security.mp +++ b/Application_examples/Web_Browser_Formal_Security.mp @@ -1,7 +1,17 @@ /* Model of Web Browser Formal Security +Author credits: + + + Purpose: +This model demonstrates using MP to model server-client communication +involving a bad server and a good server. Users may reference this model +for learning about using BUILD, ENSURE, COORDINATE, and scope limitations +in order to add clarity to traces that would be difficult to understand +otherwise, and cut out unwanted traces. + Description: Example 40. MP Web browsers formal security model. diff --git a/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors b/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors index 9549df3c08d77227573bd6c88fc44c9967a0d06c..0c0c2d2102afd3e0a1256bc892d1f930ed443b4a 100644 --- a/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors +++ b/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors @@ -1,7 +1,15 @@ /* Model of Wide Range Search for Wreckage and Survivors +Author credits: + + + Purpose: +This model demonstrates using MP to model a search and rescue opporation with +several environmental and coordination concerns to address. Users may reference this model when learning about +using COORDINATE statements to create complex diagrams through traces. + Description: Example8_OperationalProcess.mp diff --git a/Application_examples/Work_Productivity.mp b/Application_examples/Work_Productivity.mp index 351be81a48fdb0840de178f22e9361e62e5b113a..4f4322dd3c2aef50868cd9985fe9c9df0c39dea4 100644 --- a/Application_examples/Work_Productivity.mp +++ b/Application_examples/Work_Productivity.mp @@ -1,7 +1,17 @@ /* Model of Work Productivity +Author credits: + + + Purpose: +This model demonstrates using MP to show how visitors can +distract workers with stacked time usage. Users may reference +this model when learning about BUILD, COORDINATE, and SAY +statements in order to constrain models and comment on models +directly in the traces. + Description: demonstrates how to print all