diff --git a/models/Application_examples/Dining_Philosophers.mp b/models/Application_examples/Dining_Philosophers.mp index efa7e50b4020f60077370a028d0fb7d7f27aad0c..34562e771d6101bfaceddf485c6f60ffb3be5839 100644 --- a/models/Application_examples/Dining_Philosophers.mp +++ b/models/Application_examples/Dining_Philosophers.mp @@ -56,9 +56,16 @@ │*│ └────────────────────────────────────────────────────┘ │ │*│ │ │*│ ┌─[ References ]─────────────────────────────────────┠│ +│*│ │ "Example 25: Dining Philosophers." from │ │ +│*│ │ Auguston, M. "Monterey Phoenix System and │ │ +│*│ │ Software Architecture and Workflow Modeling │ │ +│*│ │ Language Manual" (Version 4). 2020. Available │ │ +│*│ │ online: │ │ +│*│ │ https://wiki.nps.edu/display/MP/Documentation │ │ +│*│ │ │ │ │*│ │ "Dining philosophers problem." Wikipedia. │ │ -│*│ │ Wikimedia Foundation, August 6, 2021. │ │ -│*│ │ https://en.wikipedia.org/wiki/Dining_philosophers_problem +│*│ │ Wikimedia Foundation, August 6, 2021. │ │ +│*│ │ https://en.wikipedia.org/wiki/Dining_philosophers_problem │*│ └────────────────────────────────────────────────────┘ │ │*│ │ │*│ ┌─[ Search Terms ]───────────────────────────────────┠│ diff --git a/models/Application_examples/Railroad_Crossing_Safety.mp b/models/Application_examples/Railroad_Crossing_Safety.mp index af64619cef94c30d0cf3d4ff79c52f8cba8a8efb..7ba9ee4f720b77e456e4cbf48c1ddce66746a287 100644 --- a/models/Application_examples/Railroad_Crossing_Safety.mp +++ b/models/Application_examples/Railroad_Crossing_Safety.mp @@ -32,9 +32,16 @@ │*│ └────────────────────────────────────────────────────┘ │ │*│ │ │*│ ┌─[ References ]─────────────────────────────────────┠│ +│*│ │ "Example 24: Railroad crossing example" from │ │ +│*│ │ Auguston, M. "Monterey Phoenix System and │ │ +│*│ │ Software Architecture and Workflow Modeling │ │ +│*│ │ Language Manual" (Version 4). 2020. Available │ │ +│*│ │ online: │ │ +│*│ │ https://wiki.nps.edu/display/MP/Documentation │ │ +│*│ │ │ │ │*│ │ Heitmeyer, Constance, and Dino Mandrioli. Formal │ │ -│*│ │ Methods for Real-Time Computing. New York, NY: │ │ -│*│ │ John Wiley & Sons, Inc., 1996. │ │ +│*│ │ Methods for Real-Time Computing. New York, NY: │ │ +│*│ │ John Wiley & Sons, Inc., 1996. │ │ │*│ └────────────────────────────────────────────────────┘ │ │*│ │ │*│ ┌─[ Search Terms ]───────────────────────────────────┠│ diff --git a/models/Application_examples/Replay_Attack.mp b/models/Application_examples/Replay_Attack.mp index 73c06714fb3aa107a0f82aa4035d7d09464d6a4a..0af8ba4a322d8f9b198808196b6e955889b1876d 100644 --- a/models/Application_examples/Replay_Attack.mp +++ b/models/Application_examples/Replay_Attack.mp @@ -19,9 +19,16 @@ │*│ └────────────────────────────────────────────────────┘ │ │*│ │ │*│ ┌─[ References ]─────────────────────────────────────┠│ +│*│ │ "Example 20: Simple MP model for the Replay │ │ +│*│ │ Attack." from Auguston, M. "Monterey Phoenix │ │ +│*│ │ System and Software Architecture and Workflow │ │ +│*│ │ Modeling Language Manual" (Version 4). 2020. │ │ +│*│ │ Available online: │ │ +│*│ │ https://wiki.nps.edu/display/MP/Documentation │ │ +│*│ │ │ │ │*│ │ "Replay attack." Wikipedia. Wikimedia Foundation, │ │ -│*│ │ July 1, 2021. │ │ -│*│ │ https://en.wikipedia.org/wiki/Replay_attack │ │ +│*│ │ July 1, 2021. │ │ +│*│ │ https://en.wikipedia.org/wiki/Replay_attack │ │ │*│ └────────────────────────────────────────────────────┘ │ │*│ │ │*│ ┌─[ Search Terms ]───────────────────────────────────┠│ diff --git a/models/Application_examples/Web_Browser_Formal_Security.mp b/models/Application_examples/Web_Browser_Formal_Security.mp index 66d9d57c1cc29e64dadd18c4a66f3a757567f90c..cf69d877fb989b5077fea0e97e71554d558de89a 100644 --- a/models/Application_examples/Web_Browser_Formal_Security.mp +++ b/models/Application_examples/Web_Browser_Formal_Security.mp @@ -33,6 +33,13 @@ │*│ └────────────────────────────────────────────────────┘ │ │*│ │ │*│ ┌─[ References ]─────────────────────────────────────┠│ +│*│ │ "Example 19: Web browsers formal security model." │ │ +│*│ │ from Auguston, M. "Monterey Phoenix System and │ │ +│*│ │ Software Architecture and Workflow Modeling │ │ +│*│ │ Language Manual" (Version 4). 2020. Available │ │ +│*│ │ online: │ │ +│*│ │ https://wiki.nps.edu/display/MP/Documentation │ │ +│*│ │ │ │ │*│ │ Jackson, Daniel. "Alloy: A Language and Tool for │ │ │*│ │ Exploring Software Designs." Communications of │ │ │*│ │ the ACM 62, no. 9 (September 2019): 66–76. │ │ diff --git a/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp b/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp index 3cfb81dd38279685e2446a5fee7f27286902a853..6af5cf19c8996a8f653706072cfb2dcc92b04b83 100644 --- a/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp +++ b/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp @@ -34,7 +34,7 @@ │*│ │ probability by that sum. This prorating operation │ │ │*│ │ distributes the contributions that would have been │ │ │*│ │ made by the rejected traces equally across the │ │ -│*│ │valid traces. The resulting probabilities show how │ │ +│*│ │ valid traces. The resulting probabilities show how │ │ │*│ │ "SHARE ALL" increases the chances of the shared │ │ │*│ │ event. │ │ │*│ └────────────────────────────────────────────────────┘ │