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

Merge branch 'master' into 'Keane_Branch'

# Conflicts:
#   Example01_SimpleMessageFlow_EventCoordination.mp
#   Example01a_UnreliableMessageFlow_VirtualEvents.mp
#   Example02_DataFlow_EventSharing.mp
#   Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
#   Example06_UnreliableChannel_AssertionChecking.mp
#   Example09_PipeFilter_TraceAnnotationQueries.mp
#   Example12_CardiacArrestWorkflow_VirtualEvents.mp
#   Example15_BackpackWeight_IntervalAttributes.mp
#   Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
#   Example21_DataFlow_LocalReport.mp
#   Example22_SimpleMessageFlow_GlobalReport.mp
#   Example24_Compiler_ComponentDiagram.mp
#   Example25_Graph_as_Data_Structure.mp
#   Example26_UnreliableMessageFlow_GlobalQuery.mp
#   Example28_AssemblingStatistics_Histogram.mp
#   Example29_AssemblingStatistics_Gantt_Chart.mp
#   Example30_MicrowaveOven_ModelingModelChecking.mp
#   Example33_ATMWithdrawal_StatechartView.mp
#   Example35_FiniteStateDiagram_PathDiagram.mp
#   Example36_Authentication_SystemReuse.mp
parents f2268f64 51979e9b
No related branches found
No related tags found
2 merge requests!6Keane branch,!5Keane branch
Showing
with 86 additions and 58 deletions
/* Surgery example /* Model of [Surgery]
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
setting. setting.
...@@ -8,7 +10,8 @@ Available at https://ieeexplore.ieee.org/abstract/document/7994952 ...@@ -8,7 +10,8 @@ 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
*/
==========================================================*/
/*Actors*/ /*Actors*/
SCHEMA Surgery SCHEMA Surgery
...@@ -83,4 +86,4 @@ ENSURE (#Correct_decision FROM Physician == 1 -> ...@@ -83,4 +86,4 @@ ENSURE (#Correct_decision FROM Physician == 1 ->
#Successful_outcome FROM Environment #Successful_outcome FROM Environment
==1); ==1);
ENSURE (#Incorrect_decision FROM Physician == 1 -> ENSURE (#Incorrect_decision FROM Physician == 1 ->
#Failed_outcome FROM Environment ==1); #Failed_outcome FROM Environment ==1);
\ No newline at end of file
/* /* Model of [Swarm_Search_and_Track]
Michael Revill Michael Revill
22 February 2016 22 February 2016
Incorporating Failure Modes and Failsafe Behaviors Incorporating Failure Modes and Failsafe Behaviors
...@@ -14,7 +15,7 @@ Verb-oriented events in title case are states ...@@ -14,7 +15,7 @@ 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)
*/ ==========================================================*/
SCHEMA Swarm_Search_and_Track SCHEMA Swarm_Search_and_Track
......
/* /* Model of [Swarm_UAV]
Kristin Giammarco and Mikhail Auguston 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
...@@ -9,7 +10,8 @@ ...@@ -9,7 +10,8 @@
This model demonstrates how to get several instances of the same actor (UAV) 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, coordinated with external events (run for scopes 2 and 3 to see 2 and 3 UAVs,
respectively). respectively).
*/
==========================================================*/
SCHEMA Swarm_UAV SCHEMA Swarm_UAV
......
/* Example39 turtles.mp /* Model of [Turtles_in_the_Desert]
Example39 turtles.mp
Demonstration of the benefits for complete Demonstration of the benefits for complete
example set generation in MP. example set generation in MP.
...@@ -24,7 +26,8 @@ Don't try to construct a non-Euclidean geometry to ...@@ -24,7 +26,8 @@ Don't try to construct a non-Euclidean geometry to
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.
==================================*/ ==========================================================*/
SCHEMA Turtles SCHEMA Turtles
neighbors: { (nobody_before | one_before | two_before ), neighbors: { (nobody_before | one_before | two_before ),
......
/******************************************************************* /* Model of [UAV_Ingress]
UAV HADR Mission UAV HADR Mission
...@@ -11,8 +11,7 @@ is acceptable but the operator aborts the ingress (trace 2). ...@@ -11,8 +11,7 @@ is acceptable but the operator aborts the ingress (trace 2).
created by A. Constable May 2017 created by A. Constable May 2017
********************************************************************/ ==========================================================*/
SCHEMA UAV_Ingress SCHEMA UAV_Ingress
......
/********************************************************************************************* /* Model of [UAV_OnStation]
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
...@@ -14,8 +14,7 @@ Paper available at https://ieeexplore.ieee.org/abstract/document/7994950 ...@@ -14,8 +14,7 @@ Paper available at https://ieeexplore.ieee.org/abstract/document/7994950
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
*********************************************************************************************/ ==========================================================*/
SCHEMA UAV_OnStation SCHEMA UAV_OnStation
......
/* Heartbeat.mp /* Model of [Unmanned_Spacecraft_Comms]
Heartbeat.mp
October 4, 2015 October 4, 2015
Created by: C. Nelson Created by: C. Nelson
...@@ -9,7 +11,7 @@ the ISS. ...@@ -9,7 +11,7 @@ the ISS.
Run for scope 1 and up. Run for scope 1 and up.
*/ ==========================================================*/
/*————————————————————————————— /*—————————————————————————————
Actors Actors
......
/* Example 40. MP Web browsers formal security model. /* Model of [Web_Browser_Formal_Security]
Example 40. MP Web browsers formal security model.
based on the papers by: based on the papers by:
...@@ -36,7 +38,8 @@ in order to model the vulnerabilities explained in the papers above. ...@@ -36,7 +38,8 @@ in order to model the vulnerabilities explained in the papers above.
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.
==============================================================================*/ ==========================================================*/
SCHEMA Web_browser SCHEMA Web_browser
/* Response may embed some Request events, /* Response may embed some Request events,
......
/* Example8_OperationalProcess.mp /* Model of [Wide_Range_Search_for_Wreckage_and_Survivors]
Example8_OperationalProcess.mp
modeling operational processes modeling operational processes
Operational processes can be modeled to provide a common baseline against which Operational processes can be modeled to provide a common baseline against which
...@@ -24,8 +26,7 @@ added to this model yet. ...@@ -24,8 +26,7 @@ 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.
*/ ==========================================================*/
/* Actors */ /* Actors */
......
/* Example 26, timing attribute use /* Model of [Work_Productivity]
Example 26, timing attribute use
also demonstrates how to print all also demonstrates how to print all
events present in the trace events present in the trace
with timing attributes with timing attributes
run for scopes 1 and up run for scopes 1 and up
*/
==========================================================*/
SCHEMA Delays SCHEMA Delays
Work: Work:
......
/* /* Example 01. Model of [Simple_Message_Flow]
Example1_simple_message_flow.mp
Event grammar rules for each root define derivations for event traces, Event grammar rules for each root define derivations for event traces,
in this case a simple sequence of zero or more events for each root. in this case a simple sequence of zero or more events for each root.
...@@ -12,7 +11,7 @@ The coordination operation behaves as a "cross-cutting" derivation rule. ...@@ -12,7 +11,7 @@ The coordination operation behaves as a "cross-cutting" derivation rule.
Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are
the most appropriate for browsing traces here. the most appropriate for browsing traces here.
*/ ==========================================================*/
SCHEMA Simple_Message_Flow SCHEMA Simple_Message_Flow
......
/* Example 1a /* Example 01a. Model of [Unreliable_Message_Flow]
Unreliable message flow.
We may want to specify behaviors when some messages get lost in the transition. We may want to specify behaviors when some messages get lost in the transition.
It can be done using ‘virtual’ events. It can be done using ‘virtual’ events.
run for scopes 1 and up. run for scopes 1 and up.
*/ ==========================================================*/
SCHEMA Unreliable_Message_Flow
SCHEMA unreliable_message_flow
ROOT Sender: (* send *); ROOT Sender: (* send *);
ROOT Receiver: (* (receive | does_not_receive) *); ROOT Receiver: (* (receive | does_not_receive) *);
......
/* Example2_DataAsEvents.mp /* Example 02. Model of [Data_Flow]
data items as behaviors
data items as behaviors
MP employs the Abstract Data Type (ADT) principle introduced by MP employs the Abstract Data Type (ADT) principle introduced by
Barbara Liskov to represent data items as operations Barbara Liskov to represent data items as operations
...@@ -22,7 +23,7 @@ This is a toy example of System_of_Systems emerging behavior modeling. ...@@ -22,7 +23,7 @@ This is a toy example of System_of_Systems emerging behavior modeling.
Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are
the most appropriate for browsing traces here. the most appropriate for browsing traces here.
*/ ==========================================================*/
SCHEMA Data_Flow SCHEMA Data_Flow
......
/* Example3_ATM_withdrawal.mp /* Example 03. Model of [ATM_Withdrawal]
Integrated system and environment behaviors
Integrated system and environment behaviors
MP separates models of component behaviors and component interactions MP separates models of component behaviors and component interactions
to permit elaboration on behaviors of multiple interacting actors. to permit elaboration on behaviors of multiple interacting actors.
...@@ -25,7 +26,7 @@ By selecting a representative enough trace (containing all events and interactio ...@@ -25,7 +26,7 @@ By selecting a representative enough trace (containing all events and interactio
like traces 2 or 3 for scope 1), and then collapsing root event, it becomes possible like traces 2 or 3 for scope 1), and then collapsing root event, it becomes possible
to view a traditional "box-and-arrow" architecture diagram, i.e. to visualize an architecture view. to view a traditional "box-and-arrow" architecture diagram, i.e. to visualize an architecture view.
*/ ==========================================================*/
SCHEMA ATM_Withdrawal SCHEMA ATM_Withdrawal
......
/* Example4_Stack_behavior.mp /* Example 04b. Model of [Queue_Behavior]
The event trace is a set of events and the Boolean expression constructs in MP The event trace is a set of events and the Boolean expression constructs in MP
can support the traditional first order predicate calculus notation. can support the traditional first order predicate calculus notation.
...@@ -8,9 +8,8 @@ grammar rules, composition operations, and some additional constraints – ...@@ -8,9 +8,8 @@ grammar rules, composition operations, and some additional constraints –
ENSURE conditions. ENSURE conditions.
run for scopes 1, 2, 3, and up. run for scopes 1, 2, 3, and up.
*/
/* This rule specifies the behavior of a stack in terms of stack operations This rule specifies the behavior of a stack in terms of stack operations
push and pop. It is assumed that initially Stack is empty. push and pop. It is assumed that initially Stack is empty.
The BUILD block associated with a root or composite event The BUILD block associated with a root or composite event
contains composition operations performed when event trace segment contains composition operations performed when event trace segment
...@@ -27,7 +26,8 @@ that satisfy the constraint. This example presents a filtering operation ...@@ -27,7 +26,8 @@ that satisfy the constraint. This example presents a filtering operation
as yet another kind of behavior composition, and demonstrates an as yet another kind of behavior composition, and demonstrates an
example of combining imperative (event grammar) and declarative example of combining imperative (event grammar) and declarative
(Boolean expressions) constructs for behavior specification. (Boolean expressions) constructs for behavior specification.
*/
==========================================================*/
SCHEMA Stack_Behavior SCHEMA Stack_Behavior
......
/* Example5_CarRace.mp /* Example 05. Model of [Car_Race]
more coordination patterns: more coordination patterns:
- ordering of selected events in concurrent threads - ordering of selected events in concurrent threads
can be modeled by coordinating them with event sequence; can be modeled by coordinating them with event sequence;
- one-many coordination. - one-many coordination.
Run for scopes 1 and up. The "Sequence" or "Swim Lanes" Run for scopes 1 and up. The "Sequence" or "Swim Lanes"
layouts are the most appropriate for browsing traces here. layouts are the most appropriate for browsing traces here.
*/
==========================================================*/
SCHEMA Car_Race SCHEMA Car_Race
......
/* Example6 Assertion checking, Communicating via unreliable channel. /* Example 06. Model of [Unreliable_Channel]
Assertion checking, Communicating via unreliable channel.
MP models need to be tested and debugged like any other MP models need to be tested and debugged like any other
programming artifacts. Trace generation for a given scope programming artifacts. Trace generation for a given scope
...@@ -17,7 +19,8 @@ ...@@ -17,7 +19,8 @@
This can significantly speed up the testing process. Of course, This can significantly speed up the testing process. Of course,
if the property should always hold, it makes sense to convert it if the property should always hold, it makes sense to convert it
into the ENSURE condition. into the ENSURE condition.
*/
==========================================================*/
SCHEMA Unreliable_Channel SCHEMA Unreliable_Channel
......
/* Example7 Trace annotation techniques /* Example 07. Model of [Unconstrained_Stack]
Trace annotation techniques
Assertion checking with the CHECK clause may be the simplest and most Assertion checking with the CHECK clause may be the simplest and most
common tool for finding counterexamples of traces, which violate some common tool for finding counterexamples of traces, which violate some
...@@ -14,7 +16,8 @@ unwanted behaviors. The MP code illustrates how to pinpoint events that ...@@ -14,7 +16,8 @@ unwanted behaviors. The MP code illustrates how to pinpoint events that
might violate certain property, and how to annotate these particular might violate certain property, and how to annotate these particular
events in the trace with additional messages. Programmers will recognize events in the trace with additional messages. Programmers will recognize
the use of debugging print statements for traditional program testing/debugging. the use of debugging print statements for traditional program testing/debugging.
*/
==========================================================*/
SCHEMA Unconstrained_Stack SCHEMA Unconstrained_Stack
ROOT Stack: (* ( push | pop [ bang ]) *) ROOT Stack: (* ( push | pop [ bang ]) *)
......
/* Example9_Employee_Employer.mp /* Example 08. Model of [Employee_Employer]
The web site http://www.infoq.com/articles/bpelbpm The web site http://www.infoq.com/articles/bpelbpm
“Why BPEL is not the holy grail for BPM “ “Why BPEL is not the holy grail for BPM “
...@@ -23,7 +23,8 @@ parallel workflow [in BPEL] that is equivalent to this one ..." ...@@ -23,7 +23,8 @@ parallel workflow [in BPEL] that is equivalent to this one ..."
Run for scope 1. The "Sequence" or "Swim Lanes" Run for scope 1. The "Sequence" or "Swim Lanes"
layouts are the most appropriate for browsing traces here. layouts are the most appropriate for browsing traces here.
Some box reshuffling may be needed to improve the trace layout. Some box reshuffling may be needed to improve the trace layout.
*/
==========================================================*/
SCHEMA Employee_Employer SCHEMA Employee_Employer
......
/* Example10_Pipe_Filter.mp /* Example 09. Model of [Pipe_Filter]
pipe/filter architecture model with 2 filters pipe/filter architecture model with 2 filters
assumptions: assumptions:
...@@ -6,7 +7,8 @@ ...@@ -6,7 +7,8 @@
2) after a message has been sent, it cannot be send repeatedly, 2) after a message has been sent, it cannot be send repeatedly,
3) received message can stay in the Filter for while, 3) received message can stay in the Filter for while,
before being sent (if at all). before being sent (if at all).
*/
==========================================================*/
SCHEMA Pipe_Filter SCHEMA Pipe_Filter
......
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