diff --git a/CHANGES b/CHANGES
index a0a479cb6..fbe5c4518 100644
--- a/CHANGES
+++ b/CHANGES
@@ -30,6 +30,7 @@ Upcoming release: BREAKING
   - Constant bandwidth observes a continuous constant bandwidth of budget/period
   - Sporadic server behaves as described by Sprunt et. al.
   - In an overcommitted system, sporadic preserves accumulated time
+* MCS kernel configuration option KernelStaticMaxBudgetUs renamed to KernelStaticMaxPeriodUs
 
 
 ## Upgrade Notes
diff --git a/config.cmake b/config.cmake
index 183e2597e..c99b179c2 100644
--- a/config.cmake
+++ b/config.cmake
@@ -454,7 +454,7 @@ config_string(
 )
 
 config_string(
-    KernelStaticMaxBudgetUs KERNEL_STATIC_MAX_BUDGET_US
+    KernelStaticMaxPeriodUs KERNEL_STATIC_MAX_PERIOD_US
     "Specifies a static maximum to which scheduling context can have \
     either its period or budget configured."
     DEFAULT 0
diff --git a/configs/ARM_MCS_verified.cmake b/configs/ARM_MCS_verified.cmake
index da918649a..89ac01840 100755
--- a/configs/ARM_MCS_verified.cmake
+++ b/configs/ARM_MCS_verified.cmake
@@ -22,5 +22,5 @@ set(KernelPrinting OFF CACHE BOOL "")
 set(KernelNumDomains 16 CACHE STRING "")
 set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "")
 set(KernelIsMCS ON CACHE BOOL "")
-set(KernelStaticMaxBudgetUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
+set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
 include(${CMAKE_CURRENT_LIST_DIR}/seL4Config.cmake)
diff --git a/configs/RISCV64_MCS_verified.cmake b/configs/RISCV64_MCS_verified.cmake
index 856fc8fcd..9889a45a6 100644
--- a/configs/RISCV64_MCS_verified.cmake
+++ b/configs/RISCV64_MCS_verified.cmake
@@ -25,7 +25,7 @@ set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "")
 set(KernelRootCNodeSizeBits 19 CACHE STRING "")
 set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
 set(KernelIsMCS ON CACHE BOOL "")
-set(KernelStaticMaxBudgetUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
+set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
 set(KernelClzNoBuiltin ON CACHE BOOL "")
 set(KernelCtzNoBuiltin ON CACHE BOOL "")
 include(${CMAKE_CURRENT_LIST_DIR}/seL4Config.cmake)
diff --git a/include/kernel/sporadic.h b/include/kernel/sporadic.h
index 401f41051..c1569feb7 100644
--- a/include/kernel/sporadic.h
+++ b/include/kernel/sporadic.h
@@ -33,11 +33,11 @@
  * at least this much budget - see comment on refill_sufficient */
 #define MIN_BUDGET_US (2u * getKernelWcetUs() * CONFIG_KERNEL_WCET_SCALE)
 #define MIN_BUDGET    (2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE)
-#if (CONFIG_KERNEL_STATIC_MAX_BUDGET_US) != 0
-#define MAX_BUDGET_US (CONFIG_KERNEL_STATIC_MAX_BUDGET_US)
+#if (CONFIG_KERNEL_STATIC_MAX_PERIOD_US) != 0
+#define MAX_PERIOD_US (CONFIG_KERNEL_STATIC_MAX_PERIOD_US)
 #else
-#define MAX_BUDGET_US getMaxUsToTicks()
-#endif /* CONFIG_KERNEL_STATIC_MAX_BUDGET_US != 0 */
+#define MAX_PERIOD_US getMaxUsToTicks()
+#endif /* CONFIG_KERNEL_STATIC_MAX_PERIOD_US != 0 */
 
 /* Short hand for accessing refill queue items */
 static inline refill_t *refill_index(sched_context_t *sc, word_t index)
diff --git a/src/object/schedcontrol.c b/src/object/schedcontrol.c
index 80122339c..ccb5cec8a 100644
--- a/src/object/schedcontrol.c
+++ b/src/object/schedcontrol.c
@@ -116,19 +116,19 @@ static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, w
         return EXCEPTION_SYSCALL_ERROR;
     }
 
-    if (budget_us > MAX_BUDGET_US || budget_ticks < MIN_BUDGET) {
+    if (budget_us > MAX_PERIOD_US || budget_ticks < MIN_BUDGET) {
         userError("SchedControl_ConfigureFlags: budget out of range.");
         current_syscall_error.type = seL4_RangeError;
         current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
-        current_syscall_error.rangeErrorMax = MAX_BUDGET_US;
+        current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
         return EXCEPTION_SYSCALL_ERROR;
     }
 
-    if (period_us > MAX_BUDGET_US || period_ticks < MIN_BUDGET) {
+    if (period_us > MAX_PERIOD_US || period_ticks < MIN_BUDGET) {
         userError("SchedControl_ConfigureFlags: period out of range.");
         current_syscall_error.type = seL4_RangeError;
         current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
-        current_syscall_error.rangeErrorMax = MAX_BUDGET_US;
+        current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
         return EXCEPTION_SYSCALL_ERROR;
     }