add sysml verison of isolette model

loonwerks · Dec 19, 2024 · bc851e9 · bc851e9
1 parent ad49362
commit bc851e9
Show file tree

Hide file tree

Showing 66 changed files with 9,675 additions and 4,170 deletions.
diff --git a/.github/workflows/ci-hamr.yml b/.github/workflows/ci-hamr.yml
@@ -5,6 +5,7 @@ on:
   push:
     paths:
       - 'micro-examples/microkit/**'
+      - 'isolette/**'
   schedule:
     - cron: "0 2 * * 6" # every sunday at 2am      
 jobs:

diff --git a/isolette/.ci/ci.cmd b/isolette/.ci/ci.cmd
@@ -46,19 +46,43 @@ if (result == 0) {
 }
 
 if (result == 0) {
-  result = run("Running codegen targeting JVM", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} JVM")
+  result = run("Running codegen from AADL model targeting JVM", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} JVM")
 }
 
 if (result == 0) {
   result = run("Verifying via Logika", T, proc"$sireum slang run ${homeDir / "hamr" / "slang" / "bin" / "run-logika.cmd"}")
 }
 
 if (result == 0) {
-  result = run("Running codegen targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit")
+  result = run("Cloning https://github.com/santoslab/sysml-aadl-libraries.git", F, proc"git clone https://github.com/santoslab/sysml-aadl-libraries.git sysml/sysml-aadl-libraries".at(homeDir / "sysml"))
+}
+
+if (result == 0) {
+  result = run("Running codegen from SysMLv2 model targeting JVM", F, proc"$sireum slang run ${homeDir / "sysml" / "bin" / "run-hamr.cmd"} JVM")
+}
+
+if (result == 0) {
+  result = run("Verifying via Logika", T, proc"$sireum slang run ${homeDir / "hamr" / "slang" / "bin" / "run-logika.cmd"}")
+}
+
+if (result == 0) {
+  result = run("Checking integration constraints", F, proc"$sireum hamr sysml logika --sourcepath ${homeDir / "sysml"}")
+}
+
+if (result == 0) {
+  result = run("Running codegen from AADL model targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit")
+}
+
+if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
+  result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
+}
+
+if (result == 0) {
+  result = run("Running codegen from SysMLv2 model targeting Microkit", F, proc"$sireum slang run ${homeDir / "sysml" / "bin" / "run-hamr.cmd"} Microkit")
 }
 
 if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
   result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
 }
 
-Os.exit(result)
+Os.exit(result)
diff --git a/isolette/.gitignore b/isolette/.gitignore
@@ -13,4 +13,5 @@
 **/target/
 **/lib/
 **/slang/js/
-**/build/*
+**/build/*
+**/sysml-aadl-libraries/
diff --git a/isolette/aadl/.slang/Isolette_isolette_single_sensor_Instance.json b/isolette/aadl/.slang/Isolette_isolette_single_sensor_Instance.json
diff --git a/isolette/aadl/aadl/packages/Abstract_Definitions.aadl b/isolette/aadl/aadl/packages/Abstract_Definitions.aadl
@@ -7,8 +7,6 @@ public
 
 			Period => Isolette_Properties::ThreadPeriod;
 
-			Stack_Size => Isolette_Properties::StackSize;
-
 			Timing_Properties::Compute_Execution_Time => Isolette_Properties::Default_Compute_Execution_Time;
 
 	end Periodic_Thread;

diff --git a/isolette/aadl/aadl/packages/Isolette.aadl b/isolette/aadl/aadl/packages/Isolette.aadl
@@ -132,13 +132,8 @@ package Isolette
 
 			Frame_Period => 1000ms;
 
-			Clock_Period => 2ms;
-
-			CASE_Scheduling::Max_Domain => 10; -- not currently used by HAMR
+			Clock_Period => 1ms;
 
 	end Isolette_Processor;
-
-	processor implementation Isolette_Processor.impl
-	end Isolette_Processor.impl;
 end Isolette;
 
diff --git a/isolette/aadl/aadl/packages/Isolette_Data_Model.aadl b/isolette/aadl/aadl/packages/Isolette_Data_Model.aadl
@@ -31,7 +31,7 @@ end TempWstatus;
 
 data implementation TempWstatus.i
   subcomponents
-    value: data Base_Types::Float_32;
+    degrees: data Base_Types::Float_32;
     status: data ValueStatus;
 end TempWstatus.i;
 
@@ -47,7 +47,7 @@ end Temp;
 
 data implementation Temp.i
   subcomponents
-    value: data Base_Types::Float_32;
+    degrees: data Base_Types::Float_32;
 end Temp.i;
 
 
@@ -57,7 +57,7 @@ end PhysicalTemp;
 
 data implementation PhysicalTemp.i
 	subcomponents
-		value: data Base_Types::Float_32;
+		degrees: data Base_Types::Float_32;
 end PhysicalTemp.i;
 
 
@@ -80,7 +80,7 @@ end Failure_Flag;
 
 data implementation Failure_Flag.i
 	subcomponents
-		value: data Base_Types::Boolean;
+		flag: data Base_Types::Boolean;
 end Failure_Flag.i;
 
 data ValueStatus

diff --git a/isolette/aadl/aadl/packages/Monitor.aadl b/isolette/aadl/aadl/packages/Monitor.aadl
@@ -180,11 +180,11 @@ public
 
 						assume Table_A_12_LowerAlarmTemp "Range [96..101]
 														|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
-							96.0f <= lower_alarm_tempWstatus.value && lower_alarm_tempWstatus.value <= 101.0f;
+							96.0f <= lower_alarm_tempWstatus.degrees && lower_alarm_tempWstatus.degrees <= 101.0f;
 
 						assume Table_A_12_UpperAlarmTemp "Range [97..102]
 														|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
-							97.0f <= upper_alarm_tempWstatus.value && upper_alarm_tempWstatus.value <= 102.0f;
+							97.0f <= upper_alarm_tempWstatus.degrees && upper_alarm_tempWstatus.degrees <= 102.0f;
 
 					--  ====== I n i t i a l i z e    E n t r y    P o i n t    Behavior Constraints ======
 					initialize
@@ -223,7 +223,7 @@ public
 										|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=113 " :
 							assume lower_alarm_tempWstatus.status == Isolette_Data_Model::ValueStatus.Invalid |
 								upper_alarm_tempWstatus.status == Isolette_Data_Model::ValueStatus.Invalid;
-							guarantee interface_failure.value;
+							guarantee interface_failure.flag;
 
 						case REQ_MMI_5 "If the Status attribute of the Lower Alarm Temperature
 											|and the Upper Alarm Temperature is Valid,
@@ -232,7 +232,7 @@ public
 							assume lower_alarm_tempWstatus.status == Isolette_Data_Model::ValueStatus.Valid
 								&
 								upper_alarm_tempWstatus.status == Isolette_Data_Model::ValueStatus.Valid;
-							guarantee !interface_failure.value;
+							guarantee !interface_failure.flag;
 
 						-- ===== Upper and Lower Temperature Values =====
 
@@ -241,17 +241,17 @@ public
 										|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=113 " :
 							assume T;
 							guarantee 
-								(!interface_failure.value) ~~>: 
-									(lower_alarm_temp.value == lower_alarm_tempWstatus.value
+								(!interface_failure.flag) ~~>: 
+									(lower_alarm_temp.degrees == lower_alarm_tempWstatus.degrees
 									&
-									upper_alarm_temp.value == upper_alarm_tempWstatus.value);
+									upper_alarm_temp.degrees == upper_alarm_tempWstatus.degrees);
 
 						case REQ_MMI_7 "If the Monitor Interface Failure is True,
 										|the Alarm Range variable is UNSPECIFIED
 										|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=113 " :
 							assume T;
 							guarantee 
-								interface_failure.value ~~>: T;
+								interface_failure.flag ~~>: T;
 
 		**};
 	end Manage_Monitor_Interface.i;
@@ -336,7 +336,7 @@ public
 										|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=114 " :
 							assume lastMonitorMode == Isolette_Data_Model::Monitor_Mode.Init_Monitor_Mode;
 							guarantee 
-								((!(interface_failure.value || internal_failure.value)) && current_tempWstatus.status == Isolette_Data_Model::ValueStatus.Valid) ~~>: 
+								((!(interface_failure.flag || internal_failure.flag)) && current_tempWstatus.status == Isolette_Data_Model::ValueStatus.Valid) ~~>: 
 									(monitor_mode == Isolette_Data_Model::Monitor_Mode.Normal_Monitor_Mode);
 
 						case REQ_MMM_3 "If the current Monitor mode is Normal, then
@@ -347,7 +347,7 @@ public
 										|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=114 " :
 							assume lastMonitorMode == Isolette_Data_Model::Monitor_Mode.Normal_Monitor_Mode;
 							guarantee 
-								((interface_failure.value || internal_failure.value) || current_tempWstatus.status != Isolette_Data_Model::ValueStatus.Valid) ~~>: 
+								((interface_failure.flag || internal_failure.flag) || current_tempWstatus.status != Isolette_Data_Model::ValueStatus.Valid) ~~>: 
 									(monitor_mode == Isolette_Data_Model::Monitor_Mode.Failed_Monitor_Mode);
 
 						case REQ_MMM_4 "If the current mode is Init, then
@@ -428,17 +428,7 @@ public
 
 			functions
 				def timeout_condition_satisfied():Base_Types::Boolean := T;
-
-			integration
-
-				assume Table_A_12_LowerAlarmTemp "Range [96..101]
-													|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
-					96.0f <= lower_alarm_temp.value && lower_alarm_temp.value <= 101.0f;
-
-				assume Table_A_12_UpperAlarmTemp "Range [97..102]
-												|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
-					97.0f <= upper_alarm_temp.value && upper_alarm_temp.value <= 102.0f;					
-
+
 			initialize
 				--     
 				guarantee REQ_MA_1 "If the Monitor Mode is INIT, the Alarm Control shall be set
@@ -454,7 +444,15 @@ public
 									|assumption is that the lower alarm must be at least 1.0f less than
 									|the upper alarm in order to account for the 0.5f tolerance
 									|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=115 ": 
-					upper_alarm_temp.value - lower_alarm_temp.value >= 1.0f;
+					upper_alarm_temp.degrees - lower_alarm_temp.degrees >= 1.0f;
+
+				assume Table_A_12_LowerAlarmTemp "Range [96..101]
+													|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
+					96.0f <= lower_alarm_temp.degrees && lower_alarm_temp.degrees <= 101.0f;
+
+				assume Table_A_12_UpperAlarmTemp "Range [97..102]
+												|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
+					97.0f <= upper_alarm_temp.degrees && upper_alarm_temp.degrees <= 102.0f;
 
 				cases
 
@@ -472,7 +470,7 @@ public
 									|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=115 " :
 						assume monitor_mode == Isolette_Data_Model::Monitor_Mode.Normal_Monitor_Mode
 							&
-							(current_tempWstatus.value < lower_alarm_temp.value || current_tempWstatus.value > upper_alarm_temp.value);
+							(current_tempWstatus.degrees < lower_alarm_temp.degrees || current_tempWstatus.degrees > upper_alarm_temp.degrees);
 						guarantee alarm_control == Isolette_Data_Model::On_Off.Onn
 							&
 							lastCmd == Isolette_Data_Model::On_Off.Onn;
@@ -486,10 +484,10 @@ public
 									|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=115 " :
 						assume monitor_mode == Isolette_Data_Model::Monitor_Mode.Normal_Monitor_Mode
 							& 
-							((current_tempWstatus.value >= lower_alarm_temp.value &&
-								current_tempWstatus.value < lower_alarm_temp.value + f32"0.5") ||
-							((current_tempWstatus.value > upper_alarm_temp.value - f32"0.5") &&
-								current_tempWstatus.value <= upper_alarm_temp.value));
+							((current_tempWstatus.degrees >= lower_alarm_temp.degrees &&
+								current_tempWstatus.degrees < lower_alarm_temp.degrees + f32"0.5") ||
+							((current_tempWstatus.degrees > upper_alarm_temp.degrees - f32"0.5") &&
+								current_tempWstatus.degrees <= upper_alarm_temp.degrees));
 						guarantee alarm_control == In(lastCmd)
 							&
 							lastCmd == In(lastCmd);
@@ -501,8 +499,8 @@ public
 									|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=115 " :
 						assume monitor_mode == Isolette_Data_Model::Monitor_Mode.Normal_Monitor_Mode
 							&
-							current_tempWstatus.value >= lower_alarm_temp.value + f32"0.5" &
-							current_tempWstatus.value <= upper_alarm_temp.value - f32"0.5";
+							current_tempWstatus.degrees >= lower_alarm_temp.degrees + f32"0.5" &
+							current_tempWstatus.degrees <= upper_alarm_temp.degrees - f32"0.5";
 						guarantee alarm_control == Isolette_Data_Model::On_Off.Off
 							&
 							lastCmd == Isolette_Data_Model::On_Off.Off;

diff --git a/isolette/aadl/aadl/packages/Operator_Interface.aadl b/isolette/aadl/aadl/packages/Operator_Interface.aadl
@@ -107,11 +107,11 @@ public
 
 				guarantee Table_A_12_LowerAlarmTemp "Range [96..101]
 													|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
-					96.0f <= lower_alarm_tempWstatus.value && lower_alarm_tempWstatus.value <= 101.0f;
+					96.0f <= lower_alarm_tempWstatus.degrees && lower_alarm_tempWstatus.degrees <= 101.0f;
 
 				guarantee Table_A_12_UpperAlarmTemp "Range [97..102]
 												|http://pub.santoslab.org/high-assurance/module-requirements/reading/FAA-DoT-Requirements-AR-08-32.pdf#page=112 " :
-					97.0f <= upper_alarm_tempWstatus.value && upper_alarm_tempWstatus.value <= 102.0f;
+					97.0f <= upper_alarm_tempWstatus.degrees && upper_alarm_tempWstatus.degrees <= 102.0f;
 		**};
 	end Operator_Interface_Thread;