commented out resolute

.gitignore

@@ -2,3 +2,4 @@
 /agree.log
 /diagrams/
 /instances/
+/.metadata/

Cyber-Resilient-UAV/.aadlbin-gen/.gitignore

@@ -0,0 +1,13 @@
+/.AGREE_Definitions.aadlbin
+/.CASE_Scheduling.aadlbin
+/.Data_Types.aadlbin
+/.FC.aadlbin
+/.GS.aadlbin
+/.HAMR.aadlbin
+/.MC.aadlbin
+/.SW.aadlbin
+/.UAS.aadlbin
+/.UAS_Buses.aadlbin
+/.UAV.aadlbin
+/.CASE_Model_Transformations.aadlbin
+/.CASE_Properties.aadlbin

Cyber-Resilient-UAV/.aadlbin-gen/Requirements/.gitignore

@@ -0,0 +1 @@
+/.CASE_Requirements.aadlbin

Cyber-Resilient-UAV/MC.aadl

@@ -102,26 +102,26 @@ public
 			Actual_Memory_Binding => (reference (Mem_HW)) applies to SW;
 			HAMR::Bit_Codec_Raw_Connections => true;
 			CASE_Properties::OS => seL4 applies to Proc_HW;
-		annex resolute {**
-			check HAMR_Guidelines
-			argue MissionComputer_Impl_cyber_resilient(this)
-		**};
+--		annex resolute {**
+--			check HAMR_Guidelines
+--			argue MissionComputer_Impl_cyber_resilient(this)
+--		**};
 	end MissionComputer.Impl;
 
-	annex resolute {**
-
-		goal MissionComputer_Impl_cyber_resilient(sys : system) <=
-			** "The " sys " is acceptably cyber-resilient" **
-			strategy : "Argue over security requirements";
-			security_requirements_complete(sys) and MissionComputer_Impl_security_requirements_satisfied(sys)
-
-		goal MissionComputer_Impl_security_requirements_satisfied(sys : system) <=
-			** "Security requirements are satisfied" **
-			MissionComputer_Impl_security_requirements_satisfied_in_model() and security_requirements_satisfied_in_implementation(sys)
-
-		goal MissionComputer_Impl_security_requirements_satisfied_in_model() <=
-			** "Security requirements are satisfied in the system model" **
-			Req_Attestation() and Req_Filter() and Req_Monitor() and Req_Separation()
-
-	**};
+--	annex resolute {**
+--		
+--		goal MissionComputer_Impl_cyber_resilient(sys : system) <=
+--			** "The " sys " is acceptably cyber-resilient" **
+--			strategy : "Argue over security requirements";
+--			security_requirements_complete(sys) and MissionComputer_Impl_security_requirements_satisfied(sys)
+--		
+--		goal MissionComputer_Impl_security_requirements_satisfied(sys : system) <=
+--			** "Security requirements are satisfied" **
+--			MissionComputer_Impl_security_requirements_satisfied_in_model() and security_requirements_satisfied_in_implementation(sys)
+--		
+--		goal MissionComputer_Impl_security_requirements_satisfied_in_model() <=
+--			** "Security requirements are satisfied in the system model" **
+--			Req_Attestation() and Req_Filter() and Req_Monitor() and Req_Separation()
+--		
+--	**};
 end MC;

Cyber-Resilient-UAV/Requirements/CASE_Requirements.aadl

@@ -2,37 +2,37 @@ package CASE_Requirements
 private
 	annex resolute {**
 
-		goal Req_Attestation() <=
-			** "[attestation] Communication sources shall be trusted" **
-			context Generated_By : "GearCASE";
-			context Generated_On : "2022-09-09-180532";
-			context Req_Component : "MC::MissionComputer.Impl.SW.RadioDriver";
-			context Formalized : "False";
-			add_attestation_manager("MC::MissionComputer.Impl.SW.RadioDriver", "MC::MissionComputer.Impl.SW.AttestationManager", "MC::MissionComputer.Impl.SW.AttestationGate")
-
-		goal Req_Filter() <=
-			** "[permit_well_formed_data] Messages shall be well-formed" **
-			context Generated_By : "GearCASE";
-			context Generated_On : "2022-09-09-180532";
-			context Req_Component : "MC::MissionComputer.Impl.SW.FlightPlanner";
-			context Formalized : "True";
-			agree_property_checked("MC::MissionComputer.Impl.SW.FlightPlanner", "Req_Filter") and add_filter("MC::MissionComputer.Impl.SW.FlightPlanner", "MC::MissionComputer.Impl.SW.Filter", "MC::MissionComputer.Impl.SW.c7", Data_Types::RF_Msg.Impl)
-
-		goal Req_Monitor() <=
-			** "[monitor_correctness] Output of uncontrolled component shall be monitored for incorrect behavior" **
-			context Generated_By : "GearCASE";
-			context Generated_On : "2022-09-09-180532";
-			context Req_Component : "MC::MissionComputer.Impl.SW.FlightPlanner";
-			context Formalized : "False";
-			add_monitor_gate("MC::MissionComputer.Impl.SW.FlightPlanner", "MC::MissionComputer.Impl.SW.Monitor", "MC::MissionComputer.Impl.SW.Monitor.Alert", "MC::MissionComputer.Impl.SW.FlightController", Data_Types::Mission)
-
-		goal Req_Separation() <=
-			** "[separation_kernel] Software shall run on a formally verified separation kernel" **
-			context Generated_By : "GearCASE";
-			context Generated_On : "2022-09-09-180532";
-			context Req_Component : "MC::MissionComputer.Impl.SW";
-			context Formalized : "False";
-			sel4_transform("MC::MissionComputer.Impl.SW")
-
-	**};
+--		goal Req_Attestation() <=
+--			** "[attestation] Communication sources shall be trusted" **
+--			context Generated_By : "GearCASE";
+--			context Generated_On : "2022-09-09-180532";
+--			context Req_Component : "MC::MissionComputer.Impl.SW.RadioDriver";
+--			context Formalized : "False";
+--			add_attestation_manager("MC::MissionComputer.Impl.SW.RadioDriver", "MC::MissionComputer.Impl.SW.AttestationManager", "MC::MissionComputer.Impl.SW.AttestationGate")
+--		
+--		goal Req_Filter() <=
+--			** "[permit_well_formed_data] Messages shall be well-formed" **
+--			context Generated_By : "GearCASE";
+--			context Generated_On : "2022-09-09-180532";
+--			context Req_Component : "MC::MissionComputer.Impl.SW.FlightPlanner";
+--			context Formalized : "True";
+--			agree_property_checked("MC::MissionComputer.Impl.SW.FlightPlanner", "Req_Filter") and add_filter("MC::MissionComputer.Impl.SW.FlightPlanner", "MC::MissionComputer.Impl.SW.Filter", "MC::MissionComputer.Impl.SW.c7", Data_Types::RF_Msg.Impl)
+--		
+--		goal Req_Monitor() <=
+--			** "[monitor_correctness] Output of uncontrolled component shall be monitored for incorrect behavior" **
+--			context Generated_By : "GearCASE";
+--			context Generated_On : "2022-09-09-180532";
+--			context Req_Component : "MC::MissionComputer.Impl.SW.FlightPlanner";
+--			context Formalized : "False";
+--			add_monitor_gate("MC::MissionComputer.Impl.SW.FlightPlanner", "MC::MissionComputer.Impl.SW.Monitor", "MC::MissionComputer.Impl.SW.Monitor.Alert", "MC::MissionComputer.Impl.SW.FlightController", Data_Types::Mission)
+--		
+--		goal Req_Separation() <=
+--			** "[separation_kernel] Software shall run on a formally verified separation kernel" **
+--			context Generated_By : "GearCASE";
+--			context Generated_On : "2022-09-09-180532";
+--			context Req_Component : "MC::MissionComputer.Impl.SW";
+--			context Formalized : "False";
+--			sel4_transform("MC::MissionComputer.Impl.SW")
+--		
+--	**};
 end CASE_Requirements;