Common Requirement Patterns

Common Requirement Patterns

This document maps common natural-language requirement patterns to TLA+ property definitions.

Table of Contents

1. State Invariants
2. Safety Properties
3. Liveness Properties
4. Ordering Properties
5. Resource Management
6. Concurrency Properties
7. Temporal Constraints

State Invariants

Pattern: Value Range Constraint

Requirement: "Variable X must always be between MIN and MAX"

TLA+ Property:

RangeInvariant == /\ X >= MIN
                  /\ X <= MAX

Alternative:

RangeInvariant == X \in MIN..MAX

Pattern: Set Membership

Requirement: "The status must always be one of: idle, running, or done"

TLA+ Property:

ValidStatus == status \in {"idle", "running", "done"}

Pattern: Non-Negative Constraint

Requirement: "The counter can never be negative"

TLA+ Property:

NonNegative == counter >= 0

Alternative:

NonNegative == counter \in Nat

Safety Properties

Pattern: Mutual Exclusion

Requirement: "At most one process can be in the critical section at any time"

TLA+ Property:

MutualExclusion ==
    \A p1, p2 \in Processes :
        (p1 # p2) => ~(pc[p1] = "critical" /\ pc[p2] = "critical")

Alternative (counting):

MutualExclusion ==
    Cardinality({p \in Processes : pc[p] = "critical"}) <= 1

Pattern: Buffer Overflow Prevention

Requirement: "The buffer must never exceed its capacity"

TLA+ Property:

NoOverflow == Len(buffer) <= CAPACITY

Pattern: Resource Bounds

Requirement: "The total allocated resources must not exceed the available resources"

TLA+ Property:

ResourceBound ==
    (\A r \in Resources : allocated[r]) <= available

Pattern: Deadlock Freedom

Requirement: "The system must never deadlock"

TLA+ Property:

NoDeadlock ==
    [](\E p \in Processes : ENABLED Action(p))

Pattern: Data Consistency

Requirement: "All replicas must have consistent data"

TLA+ Property:

Consistency ==
    \A r1, r2 \in Replicas : data[r1] = data[r2]

Liveness Properties

Pattern: Eventual Completion

Requirement: "Every started task eventually completes"

TLA+ Property:

EventualCompletion ==
    \A task \in Tasks :
        (task.status = "started") ~> (task.status = "completed")

Pattern: Guaranteed Response

Requirement: "Every request eventually receives a response"

TLA+ Property:

GuaranteedResponse ==
    \A req \in Requests :
        (req.sent) ~> (req.responded)

Pattern: Termination

Requirement: "The algorithm eventually terminates"

TLA+ Property:

Termination == <>(terminated = TRUE)

Alternative (all processes done):

Termination ==
    <>(\A p \in Processes : pc[p] = "done")

Pattern: Progress

Requirement: "The system makes progress (doesn't get stuck)"

TLA+ Property:

Progress == []<>(state_changed)

Alternative (with fairness):

Progress == WF_vars(Next)

Pattern: Eventual Stability

Requirement: "The system eventually reaches a stable state and stays there"

TLA+ Property:

EventualStability == <>[](stable)

Ordering Properties

Pattern: Happens-Before

Requirement: "Event A must happen before event B"

TLA+ Property:

HappensBefore ==
    [](event_B_occurred => event_A_occurred_before)

With timestamps:

HappensBefore ==
    [](event_B.occurred => event_A.timestamp < event_B.timestamp)

Pattern: FIFO Ordering

Requirement: "Requests are processed in first-in-first-out order"

TLA+ Property:

FIFOOrder ==
    \A req1, req2 \in Requests :
        (req1.arrival_time < req2.arrival_time /\
         req2.status = "completed")
            => (req1.status = "completed")

Pattern: Causal Ordering

Requirement: "If operation A causally precedes B, A must be applied before B"

TLA+ Property:

CausalOrder ==
    \A a, b \in Operations :
        (CausallyPrecedes(a, b) /\ Applied(b))
            => Applied(a)

Resource Management

Pattern: Resource Acquisition

Requirement: "A process can only use a resource if it has acquired it"

TLA+ Property:

ProperAcquisition ==
    \A p \in Processes, r \in Resources :
        (Using(p, r)) => (Holds(p, r))

Pattern: No Resource Leaks

Requirement: "Every acquired resource is eventually released"

TLA+ Property:

NoLeaks ==
    \A p \in Processes, r \in Resources :
        (Acquired(p, r)) ~> (Released(p, r))

Pattern: Bounded Resources

Requirement: "At most N processes can hold resource R simultaneously"

TLA+ Property:

BoundedAccess ==
    Cardinality({p \in Processes : Holds(p, R)}) <= N

Concurrency Properties

Pattern: Atomicity

Requirement: "Operation X executes atomically (no interleaving)"

TLA+ Property:

Atomicity ==
    [](OperationStarted(X) => <>OperationCompleted(X))
    /\ ~(\E p1, p2 \in Processes :
            p1 # p2 /\ InOperation(p1, X) /\ InOperation(p2, X))

Pattern: No Starvation

Requirement: "Every waiting process eventually gets access"

TLA+ Property:

NoStarvation ==
    \A p \in Processes :
        (Waiting(p)) ~> (Granted(p))

Pattern: Bounded Waiting

Requirement: "A waiting process gets access within N steps"

TLA+ Property:

\* Requires auxiliary counter variable
BoundedWaiting ==
    \A p \in Processes :
        [](Waiting(p) => <>(Granted(p) \/ wait_count[p] > N))

Pattern: Fair Scheduling

Requirement: "All processes get fair access to the CPU"

TLA+ Property:

FairScheduling ==
    \A p \in Processes :
        WF_vars(Schedule(p))

Temporal Constraints

Pattern: Conditional Execution

Requirement: "If condition C holds, action A must eventually execute"

TLA+ Property:

ConditionalExecution ==
    [](C => <>A)

Pattern: Persistent Condition

Requirement: "Once condition C becomes true, it stays true"

TLA+ Property:

Persistent ==
    [](C => []C)

Alternative (stability):

Stable == <>[](C)

Pattern: Recurrence

Requirement: "Condition C holds infinitely often"

TLA+ Property:

Recurrence == []<>C

Pattern: Response Time

Requirement: "If event E occurs, response R happens within T time units"

TLA+ Property:

\* Requires clock variable
ResponseTime ==
    \A e \in Events :
        [](e.occurred => <>(e.responded /\ clock - e.time <= T))

Complex Patterns

Pattern: Two-Phase Commit

Requirement: "All participants must agree before commit"

TLA+ Property:

TwoPhaseCommit ==
    /\ [](Committed => (\A p \in Participants : Prepared(p)))
    /\ \A p \in Participants : (Prepared(p)) ~> (Committed \/ Aborted)

Pattern: Leader Election

Requirement: "Eventually exactly one leader is elected"

TLA+ Property:

LeaderElection ==
    /\ <>(\E p \in Processes : IsLeader(p))
    /\ [](\A p1, p2 \in Processes :
            (IsLeader(p1) /\ IsLeader(p2)) => (p1 = p2))

Pattern: Consensus

Requirement: "All correct processes eventually agree on the same value"

TLA+ Property:

Consensus ==
    /\ <>(\A p \in CorrectProcesses : Decided(p))
    /\ [](\A p1, p2 \in CorrectProcesses :
            (Decided(p1) /\ Decided(p2)) => (decision[p1] = decision[p2]))

Pattern: Eventual Consistency

Requirement: "After updates stop, all replicas converge to the same state"

TLA+ Property:

EventualConsistency ==
    ([]<>(~UpdateOccurred))
        => <>[](\A r1, r2 \in Replicas : state[r1] = state[r2])

Requirement Keywords to TLA+ Mapping