Upload New File

Example57_Authentication.mp

+/*******************************************************************************
+
+A Model for Simple Authentication
+
+A demonstration that shows how to reject unwanted behaviors with ENSURE 
+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
+  
+********************************************************************************/
+
+SCHEMA Authentication
+
+/*-----------------------
+  USER BEHAVIORS
+-------------------------*/
+
+ROOT User: 	Provide_credentials
+			  (* CREDS_INVALID Reenter_credentials *)
+			 [ CREDS_VALID Access_system ];
+
+/*-----------------------
+  SYSTEM BEHAVIORS
+-------------------------*/
+
+ROOT System:	Verify_credentials
+				(+ ( CREDS_INVALID Deny_access |
+                    	CREDS_VALID Grant_access ) +)
+				[ Lock_account ]
+                ;
+
+/*-----------------------
+  INTERACTION CONSTRAINTS
+-------------------------*/
+
+User, System SHARE ALL CREDS_VALID, CREDS_INVALID;
+
+COORDINATE 	$a: Provide_credentials	FROM User,
+			$b: Verify_credentials	FROM System
+		DO ADD $a PRECEDES $b; OD;
+
+COORDINATE 	$a: Deny_access				FROM System,
+			$b: Reenter_credentials 	FROM User
+		DO ADD $a PRECEDES $b; OD; 
+
+COORDINATE 	$a: Grant_access		FROM System,
+			$b: Access_system		FROM User
+		DO ADD $a PRECEDES $b; OD; 
+
+ENSURE #CREDS_INVALID <= 3;
+
+ENSURE #Deny_access >= 3 <-> #Lock_account == 1;
+
+ENSURE #Grant_access >= 1 -> #Lock_account == 0;
\ No newline at end of file