diff --git a/Application_examples/Authentication.mp b/Application_examples/Authentication.mp index 4b017f65197ae485ac2376ee9854656bec764985..275b59a8224826db5277d051d43b404b175a006b 100644 --- a/Application_examples/Authentication.mp +++ b/Application_examples/Authentication.mp @@ -1,5 +1,9 @@ /* Model of Authentication +Purpose: + +Description: + A Model for Simple Authentication A demonstration that shows how to reject unwanted behaviors with ENSURE @@ -8,7 +12,13 @@ constraints. created by K.Giammarco on 05/16/2017 modified by K.Giammarco on 08/07/2017 for capitalization of state events modified by K.Giammarco on 08/07/2017 for ENSURE constraints - + +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Authentication diff --git a/Application_examples/Autonomous_Car.mp b/Application_examples/Autonomous_Car.mp index 4c71cb975178225e66bfd71fb1be89f886eaaae6..05984df4616f48f67bcdd77a604539e964b1c879 100644 --- a/Application_examples/Autonomous_Car.mp +++ b/Application_examples/Autonomous_Car.mp @@ -1,9 +1,19 @@ /* Model of Autonomous Car +Purpose: + +Description: + A model of an autonomous car that was used to support a failure mode analysis of autonomous automobile technology (student project). Created by G. Kaminski, November 2015 +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Autonomous_Car diff --git a/Application_examples/Beginner_Use_of_MP.mp b/Application_examples/Beginner_Use_of_MP.mp index 2c17c7d8f3a277a434082fefc8876fd5fdb76b2c..6cd3631130538bf7ee38d5fadfee5fb1f011f717 100644 --- a/Application_examples/Beginner_Use_of_MP.mp +++ b/Application_examples/Beginner_Use_of_MP.mp @@ -1,5 +1,9 @@ /* Model of Beginner Use of MP +Purpose: + +Description: + A Simple Model of Beginner MP-Firebird Use created by K.Giammarco 2021-02-08 @@ -23,6 +27,12 @@ of the contents of the text editor, and "Code and Event Trace" exports the contents of the text editor plus the graphs and any changes you made to the graph element positions. +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Beginner_Use_of_MP diff --git a/Application_examples/CargoScreening.mp b/Application_examples/CargoScreening.mp index 8b190e3510bd0d078009c8fc07bd3d6ef753389c..5d18b3a67599b5c720fc47985a4a439a633f8692 100644 --- a/Application_examples/CargoScreening.mp +++ b/Application_examples/CargoScreening.mp @@ -1,5 +1,9 @@ /* Model of Cargo Screening +Purpose: + +Description: + Cargo Screening process model May 6, 2011, draft written by Mikhail Auguston, NPS, Monterey, CA source: @@ -20,6 +24,12 @@ MP-Firebird may be used at least for the following: was it always preceded by ThreatIsNotFound or No_high_risk_cargo_selected events?" - typical query may be: "show all scenarios when Loading event does not happen" +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA CargoScreening diff --git a/Application_examples/Commercial_Flight b/Application_examples/Commercial_Flight index d830f8a72b1116960da91c5ff027832a8fcbffef..b609d0de24bfe17e4dc19c6a54c3b2083e446ccb 100644 --- a/Application_examples/Commercial_Flight +++ b/Application_examples/Commercial_Flight @@ -1,5 +1,9 @@ /* Model of Commercial Flight +Purpose: + +Description: + Model of a commercial flight, November 27, 2013 This model demonstrates the interlacing of root events as Phases @@ -7,6 +11,12 @@ and as Actors. The commented out code at the bottom represents a simulation of COORDINATE statements with SHARE ALL statements before COORDINATE statements were implemented in the early MP tools. +References: + +Search terms: + +Instructions: + ==========================================================*/ /*----------------------------------------------------- diff --git a/Application_examples/Cycle_Pattern.mp b/Application_examples/Cycle_Pattern.mp index 257a3ddeebe1b0a34b314429f839b69eef22fe42..aaa8d596c91823f85e0315957c39814bb2c97ebe 100644 --- a/Application_examples/Cycle_Pattern.mp +++ b/Application_examples/Cycle_Pattern.mp @@ -1,6 +1,10 @@ /* Model of Cycle Pattern - Cycle_ISP Model for Systems Journal Article +Purpose: + +Description: + +Cycle_ISP Model for Systems Journal Article Available at https://www.mdpi.com/2079-8954/6/2/18 created 2018-03-10 by K.Giammarco @@ -19,6 +23,12 @@ the different possible patterns for Cycle. Running at scope 1 will generate zero traces because of the ENSURE constraint on line 29. +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Cycle_ISP_v2 diff --git a/Application_examples/Dining_Philosophers.mp b/Application_examples/Dining_Philosophers.mp index 8b0f7bed653f96e17e759c1ba3e079e522245d7e..c467e09c694067ae8707c7cf38b2045eebaf2992 100644 --- a/Application_examples/Dining_Philosophers.mp +++ b/Application_examples/Dining_Philosophers.mp @@ -1,5 +1,9 @@ /* Model of Dining Philosophers +Purpose: + +Description: + Example 17, Dining_Philosophers.mp Five silent philosophers sit at a table around a bowl of spaghetti. A fork is placed between each pair of adjacent philosophers. @@ -32,6 +36,12 @@ scope 3 yields 6 traces in approx. 0.05 sec. scope 4 yields 14 traces in approx. 0.44 sec. scope 5 yields 30 traces in approx. 1.6 sec. +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Dining_Philosophers diff --git a/Application_examples/Elevator.mp b/Application_examples/Elevator.mp index c4ac119e403c63a76f4e4d1b75685ac81208d6b4..6f85993589c4dfe6618a301f67e522a4b74fe2a5 100644 --- a/Application_examples/Elevator.mp +++ b/Application_examples/Elevator.mp @@ -1,5 +1,9 @@ /* Model of Elevator +Purpose: + +Description: + Elevator Model K.Giammarco circa 2011 @@ -14,7 +18,13 @@ in the case of this model, ( Elevator_works_fine Get_Off | Emergency_Situation Call_for_help ) - + +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA ELEVATOR diff --git a/Application_examples/FindAdvisor.mp b/Application_examples/FindAdvisor.mp index d66db40d1c5b23caaddae0722a7e20ce00d18d66..b8d184d544992cf0599a872e97c66fffcadb41b0 100644 --- a/Application_examples/FindAdvisor.mp +++ b/Application_examples/FindAdvisor.mp @@ -1,5 +1,9 @@ /* Model of Find Advisor +Purpose: + +Description: + example63_Find_Advisor.mp modeling human interactions @@ -18,7 +22,13 @@ Run for scope 1 (there is no iteration in this example, so increaasing the scope produce more scenarios). 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: ==========================================================*/ diff --git a/Application_examples/First_Responder.mp b/Application_examples/First_Responder.mp index 8dc4db3c8988900abeb6cda169969244df3827fa..53a2fbb62539c0933b17b1b945dfd51ce828df8e 100644 --- a/Application_examples/First_Responder.mp +++ b/Application_examples/First_Responder.mp @@ -1,5 +1,9 @@ /* Model of First Responder +Purpose: + +Description: + A first responder scenario involving the administation of a rescue medication (Narcan) to an overdose victim by a First Responder or a Bystander. @@ -11,6 +15,12 @@ scenarios emerged that was previously not considered. Trace 6 and others show a double administration of Narcan by both the bystander and the first responder. +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Narcan_Administration diff --git a/Application_examples/Knapsack_Weight_Limit.mp b/Application_examples/Knapsack_Weight_Limit.mp index 43ed159c3e3111c5cb42473797b8aab9d6412526..9c09b79c969200e3887094f60fb8a32ad1f76871 100644 --- a/Application_examples/Knapsack_Weight_Limit.mp +++ b/Application_examples/Knapsack_Weight_Limit.mp @@ -1,5 +1,9 @@ /* Model of Knapsack Weight Limit +Purpose: + +Description: + Example 38 Knapsack This is a case of well-known Knapsack Dynamic Programming Problem. @@ -15,6 +19,12 @@ Example 38 Knapsack Run for scope 1 and up to 5 +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Knapsack diff --git a/Application_examples/MP_Architecture_Specification.mp b/Application_examples/MP_Architecture_Specification.mp index e4a3f72665467d03bac1d2af46dad98d1e5dd355..8f68fed3e7ae8609d3b636096cf43741e494f232 100644 --- a/Application_examples/MP_Architecture_Specification.mp +++ b/Application_examples/MP_Architecture_Specification.mp @@ -1,10 +1,20 @@ /* Model of MP Architecture Specification +Purpose: + +Description: + Example 28 MP compiler/trace generator architecture model run for scope 1 or more - + +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA MP_architecture diff --git a/Application_examples/Manufacturing_Process.mp b/Application_examples/Manufacturing_Process.mp index 9f3d1f44b7fa771c5846f9e4484ea73972c5fe98..83a252cb58b88360ca422e1d21e8bb376c5cfacd 100644 --- a/Application_examples/Manufacturing_Process.mp +++ b/Application_examples/Manufacturing_Process.mp @@ -1,5 +1,9 @@ /* Model of Manufacturing Process +Purpose: + +Description: + Application of Monterey Phoenix Modeling to Manufacturing Product Systems An example pre-dating MP-Firebird application that was used to generate scenarios for separately estimating probability, time and cost of each of these scenarios. @@ -7,6 +11,12 @@ MP version 4 may be used to conduct such analysis with its native capabilities. Created by: John Palmer August 2014 +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Manufacturing_System diff --git a/Application_examples/Martian_Lander.mp b/Application_examples/Martian_Lander.mp index 277988ce567204697ba5383a601d1a8b45b2e536..8ead385cd2639e4624b7ffa839217b85165cb390 100644 --- a/Application_examples/Martian_Lander.mp +++ b/Application_examples/Martian_Lander.mp @@ -1,5 +1,9 @@ /* Model of Martian Lander +Purpose: + +Description: + Example 45. Real time system behavior modeling. Landing system for Martian Lander. @@ -55,6 +59,12 @@ RRM 10 run for scope 1 and up. +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Martian_Lander diff --git a/Application_examples/Prisoners_Dilemma.mp b/Application_examples/Prisoners_Dilemma.mp index 1070aa47fbacc384d35a2da5f9156710c948a6d5..ee66e9f3e515c57753d3c49a9ccde130ae570428 100644 --- a/Application_examples/Prisoners_Dilemma.mp +++ b/Application_examples/Prisoners_Dilemma.mp @@ -1,5 +1,9 @@ /* Model of Prisoners Dilemma +Purpose: + +Description: + The Prisoner's Dilemma Michael Collins August 10, 2020. @@ -54,7 +58,13 @@ the payoff for Bob when Alice does not confess = 2. in all other circumstances the payoff for Bob = 0. To map it to classic values to show negative payoffs -- that is a sort of normalizing. -The total payoff is computed from the assignments above and then subtracting 2. +The total payoff is computed from the assignments above and then subtracting 2. + +References: + +Search terms: + +Instructions: ==========================================================*/ diff --git a/Application_examples/Railroad_Crossing_Safety.mp b/Application_examples/Railroad_Crossing_Safety.mp index 1f78a5e05d57943d18f88f4eafe5c4c06addb277..0433f8a9c22d3ef3c0fade4663b6749390cad574 100644 --- a/Application_examples/Railroad_Crossing_Safety.mp +++ b/Application_examples/Railroad_Crossing_Safety.mp @@ -1,5 +1,9 @@ /* Model of Railroad Crossing Safety +Purpose: + +Description: + Example 27. Timing attribute use. Railroad crossing example from [Formal Methods for Real-Time Computing, 1996]. @@ -9,6 +13,12 @@ each train enters and exits the crossing’s region. The main safety requirement is: if a train is in the crossing region, then gate must be down. +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Railroad_Crossing diff --git a/Application_examples/Replay_Attack.mp b/Application_examples/Replay_Attack.mp index 282ce7a7c8d17de6e1dc8eefff2b9d281d242cc6..35f1450f850eeff9c2cb5dd9058a2be25779e597 100644 --- a/Application_examples/Replay_Attack.mp +++ b/Application_examples/Replay_Attack.mp @@ -1,11 +1,21 @@ /* Model of Replay Attack +Purpose: + +Description: + Example 41. The description of Replay Attack is available at https://en.wikipedia.org/wiki/Replay_attack run scope up to 5 +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Replay_Attack diff --git a/Application_examples/Small_Package_Delivery.mp b/Application_examples/Small_Package_Delivery.mp index dcb5d51fefa3276f93f7cf16a3e31d585eaae932..ef3fb30bb9e0b620630b58f4c262cace6fe484cd 100644 --- a/Application_examples/Small_Package_Delivery.mp +++ b/Application_examples/Small_Package_Delivery.mp @@ -1,5 +1,9 @@ /* Model of Small Package Delivery +Purpose: + +Description: + Taken from use case description in the Skyzer IM20 Mission Model (Non-Combatant Operations Scenario): @@ -33,6 +37,12 @@ root (line 36 and lines 114-128) and running that model subset, one can see 6 event traces, one of which is unexpected: the Air_Vehicle drops the payload with no vessel in sight (trace 6). +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Small_Package_Delivery diff --git a/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp b/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp index 687946b79883718f3f918f6540c2a24bd4285e5f..6e599101a8b9f82c7778064d45abcc33147d6076 100644 --- a/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp +++ b/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp @@ -1,5 +1,9 @@ /* Model of Spent Fuel Cooling and Cleanup +Purpose: + +Description: + Cooling Pool created by K.Giammarco 5/4/2020 @@ -9,6 +13,12 @@ modified by K.Giammarco 5/13/2020 with D.VanBossuyt The purpose of this model is to identify the components of and interactions among a spent nuclear fuel cooling pool and its environment. +References: + +Search terms: + +Instructions: + ==========================================================*/ /*————————————————————————————— diff --git a/Application_examples/Spiral_Software_Process b/Application_examples/Spiral_Software_Process index 0602fc03ff143dc2343547aae5e17ef28f8bdef6..dd1bb9f323b3afd7092645f7a2429284dcc74149 100644 --- a/Application_examples/Spiral_Software_Process +++ b/Application_examples/Spiral_Software_Process @@ -1,5 +1,9 @@ /* Model of Spiral Software Process +Purpose: + +Description: + Example 16, model of the spiral software process This example also illustrates how Melvin Conway's law @@ -9,6 +13,12 @@ Example 16, model of the spiral software process run scope up to 5 +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA spiral diff --git a/Application_examples/Surgery.mp b/Application_examples/Surgery.mp index 8ccd439966ccc6afa97dd8a4d39166ecd461771b..8a0458e9b2d25285c6d1f889f2eca8441c3adbda 100644 --- a/Application_examples/Surgery.mp +++ b/Application_examples/Surgery.mp @@ -1,5 +1,9 @@ /* Model of Surgery +Purpose: + +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 @@ -11,6 +15,12 @@ Available at https://ieeexplore.ieee.org/abstract/document/7994952 Created by: J. Quartuccio (2017) Naval Postgraduate School +References: + +Search terms: + +Instructions: + ==========================================================*/ /*Actors*/ diff --git a/Application_examples/Swarm_Search_and_Track.mp b/Application_examples/Swarm_Search_and_Track.mp index fdaf889c05e5a584d779f7548f97fcff65e79782..f11628085cb0ceb62d31fd732591e474cbf4b656 100644 --- a/Application_examples/Swarm_Search_and_Track.mp +++ b/Application_examples/Swarm_Search_and_Track.mp @@ -1,5 +1,9 @@ /* Model of Swarm Search and Track +Purpose: + +Description: + Michael Revill 22 February 2016 Incorporating Failure Modes and Failsafe Behaviors @@ -15,6 +19,12 @@ Verb-oriented events in title case are states This model demonstrates the found unexpected behavior for object discovery after bingo fuel (trace 6) +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Swarm_Search_and_Track diff --git a/Application_examples/Swarm_UAV.mp b/Application_examples/Swarm_UAV.mp index 2b2b7265bf873c07d9073fecaa0edef8b6f24e61..4e3e7b58246a67c018e2cdc3eacfc74303ab2c3e 100644 --- a/Application_examples/Swarm_UAV.mp +++ b/Application_examples/Swarm_UAV.mp @@ -1,6 +1,10 @@ /* 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 11 February 2015 - Initial Model Started by KGiammarco 25 May 2015 - M.Auguston Merged several COORDINATE, SHARE ALL to speed up @@ -11,6 +15,12 @@ coordinated with external events (run for scopes 2 and 3 to see 2 and 3 UAVs, respectively). +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Swarm_UAV diff --git a/Application_examples/Turtles_in_the_Desert.mp b/Application_examples/Turtles_in_the_Desert.mp index 3a8801ae8f5cac3f1685766c052367068a908fac..d8152e7c80f8fdee596a7fcaba1fa7ed2282ff14 100644 --- a/Application_examples/Turtles_in_the_Desert.mp +++ b/Application_examples/Turtles_in_the_Desert.mp @@ -1,5 +1,9 @@ /* Model of Turtles in the Desert +Purpose: + +Description: + Example39 turtles.mp Demonstration of the benefits for complete @@ -25,7 +29,13 @@ Don't try to construct a non-Euclidean geometry to Here it is. Run for scope 1. There are 13 possible scenarios, and none when all three are telling the truth. - + +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Turtles diff --git a/Application_examples/UAV_Ingress.mp b/Application_examples/UAV_Ingress.mp index a47676f3c73051f005e0e78b09fccb557a65e670..08097bc880eda38767e36a702d7b919d1f360860 100644 --- a/Application_examples/UAV_Ingress.mp +++ b/Application_examples/UAV_Ingress.mp @@ -1,5 +1,9 @@ /* Model of UAV Ingress +Purpose: + +Description: + UAV HADR Mission 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 is acceptable but the operator aborts the ingress (trace 2). created by A. Constable May 2017 - + +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA UAV_Ingress diff --git a/Application_examples/UAV_OnStation.mp b/Application_examples/UAV_OnStation.mp index 6cccd16d33c8e8a20832c4f8c51bb8525c448a0d..94555c400dc16e84c1c2eaed3be205f322e7f3ad 100644 --- a/Application_examples/UAV_OnStation.mp +++ b/Application_examples/UAV_OnStation.mp @@ -1,5 +1,9 @@ /* Model of UAV On Station +Purpose: + +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 @@ -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-05-2017 to add normal events back to failure mode scenarios and added annotations - + +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA UAV_OnStation diff --git a/Application_examples/Unmanned_Spacecraft_Comms.mp b/Application_examples/Unmanned_Spacecraft_Comms.mp index 8dbbf3425f1f4636ee939a0a919dee3184ced451..82332ac90ce60f7c83f82b2472b02c0c2e0b9f0f 100644 --- a/Application_examples/Unmanned_Spacecraft_Comms.mp +++ b/Application_examples/Unmanned_Spacecraft_Comms.mp @@ -1,5 +1,9 @@ /* Model of Unmanned Spacecraft Comms +Purpose: + +Description: + Heartbeat.mp October 4, 2015 Created by: C. Nelson @@ -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 ISS. -Run for scope 1 and up. - +Run for scope 1 and up. + +References: + +Search terms: + +Instructions: + ==========================================================*/ /*————————————————————————————— diff --git a/Application_examples/Web_Browser_Formal_Security.mp b/Application_examples/Web_Browser_Formal_Security.mp index 3f4c37e2cbaec373806abe581838133b0bf14740..c64a6b35009af295940bdb7095e996701a004811 100644 --- a/Application_examples/Web_Browser_Formal_Security.mp +++ b/Application_examples/Web_Browser_Formal_Security.mp @@ -1,5 +1,9 @@ /* Model of Web Browser Formal Security +Purpose: + +Description: + Example 40. MP Web browsers formal security model. based on the papers by: @@ -37,7 +41,13 @@ in order to model the vulnerabilities explained in the papers above. This example borrowed from Daniel Jackson's paper demonstrates how MP can check whether Client's web query may be indirectly affected by Bad Server's Redirect intervention. - + +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Web_browser diff --git a/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors b/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors index 6bab881f790be917cac9445ada77863bc25bbfb5..9549df3c08d77227573bd6c88fc44c9967a0d06c 100644 --- a/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors +++ b/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors @@ -1,5 +1,9 @@ /* Model of Wide Range Search for Wreckage and Survivors +Purpose: + +Description: + Example8_OperationalProcess.mp modeling operational processes @@ -24,7 +28,13 @@ produce more scenarios). Only one scenario is produced because no decision point added to this model yet. 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: ==========================================================*/ diff --git a/Application_examples/Work_Productivity.mp b/Application_examples/Work_Productivity.mp index 6173948a35f52841544013ba74b9c8eb9dc6bab1..c7db03e200b91534f40ad7d2fb329bc10779d11d 100644 --- a/Application_examples/Work_Productivity.mp +++ b/Application_examples/Work_Productivity.mp @@ -1,5 +1,9 @@ /* Model of Work Productivity +Purpose: + +Description: + Example 26, timing attribute use also demonstrates how to print all @@ -8,6 +12,12 @@ Example 26, timing attribute use run for scopes 1 and up +References: + +Search terms: + +Instructions: + ==========================================================*/ SCHEMA Delays