Formal Methods & Specification: Languages, Models & Validation

TAKEAWAYS:

• Formal specifications use mathematical notation (e.g., Z, B) to define software behavior unambiguously, unlike natural language.
• Model-based validation (e.g., state machines, Petri nets) lets you simulate and verify systems before implementation.
• Theorem provers (e.g., Coq, Isabelle) automatically check proofs of correctness for safety-critical code.
• Refinement bridges abstract specs to executable code while preserving correctness properties.
• Case studies: NTC’s network routing specs (Z), eSewa’s transaction contracts (B), and NEPSE’s trading rules (finite state machines).
• Trade-offs: Formal methods add upfront cost but catch errors early—critical for systems like banks or medical devices.

Core Concepts: What Is Formal Specification?

Formal specification is the precise, mathematical description of a software system’s requirements, interfaces, or behavior. Unlike informal docs (e.g., "the system shall handle payments"), formal specs use:

• Notation: Logical symbols, set theory, or temporal logic.
• Semantics: Clear rules for interpretation (e.g., "∀x ∈ Accounts • balance(x) ≥ 0").
• Tools: Editors, provers, or model checkers to validate specs.

Why Use Formal Methods?

A flowchart showing: Requirements → Formal Spec (Z/B) → Model (FSM/Petri) → Proof/Simulation → Code → Testing.

1. Formal Specification Languages

Three languages dominate formal specs: Z, B, and VDM. Each targets different needs.

A. Z Notation: Schema Calculus

Z uses set theory and predicate logic to define:

• States (e.g., Account = [name : String, balance : ℕ]).
• Operations (e.g., Withdraw ≡ ΔAccount ∙ balance' = balance − amount ∧ amount ≤ balance).
• Invariants (e.g., balance ≥ 0).

Worked Example: eSewa Transaction

stateDiagram-v2
    [*] --> Init: balance = 0
    Init --> Withdraw: amount ≤ balance
    Withdraw --> Init: balance' = balance - amount
    Init --> Deposit: amount > 0
    Deposit --> Init: balance' = balance + amount
    state Init {
        [ ] : balance ≥ 0
    }

Z Notation schema calculus example: Account state transitions with invariant Z Schema for Withdraw:

Withdraw
  ΔAccount
  amount : ℕ
  amount ≤ balance ∧ balance' = balance − amount

Real Tie: eSewa’s "deduct fee before refund" rule could be specified in Z to avoid disputes.

B. B Method: Refinement-Centric

B focuses on stepwise refinement from abstract specs to executable code. Key features:

• Machines: Encapsulate state and operations (e.g., ACCOUNT machine).
• Refinement: Proves each step preserves correctness (e.g., ACCOUNT → IMPLEMENTED_ACCOUNT).
• Prover: Automatically checks proofs (used in railway signaling).

Example: NTC’s Network Node

B Machine Snippet (pseudo-B):

MACHINE ROUTER
VARIABLES routes
INVARIANT
  routes ∈ IP → Port
OPERATIONS
  FORWARD(p) =
    PRE p.dst ∈ dom(routes)
    THEN routes(p.dst) ← p
    END

C. VDM: Vienna Development Method

VDM emphasizes pre/postconditions and data modeling. Example:

types
  Account = [balance : nat]
operations
  Withdraw : Account × nat → Account
  Withdraw(a, amount) ==
    if amount ≤ a.balance then
      a with balance := a.balance − amount
    else
      a  -- unchanged
    endif

Real Tie: NEPSE’s trading system could use VDM to specify "order matching" rules.

2. Model-Based Approaches

Models let you simulate and verify behavior before coding.

A. Finite State Machines (FSMs)

Define systems as states + transitions. Used for:

• Protocols (e.g., TCP handshake).
• Workflows (e.g., Daraz order status: Placed → Shipped → Delivered).

Example: Pathao Rider App

stateDiagram-v2
    [*] --> Idle: No ride
    Idle --> Accepted: Rider accepts order
    Accepted --> PickedUp: Rider confirms pickup
    PickedUp --> Delivered: Rider marks delivery
    Delivered --> Idle: Order complete

FSM for Pathao’s Rider State:

B. Petri Nets

Extend FSMs with tokens to model concurrency (e.g., NTC’s call routing).

Real Tie: NTC’s IVR system uses Petri nets to balance call loads.

C. Temporal Logic (LTL/CTL)

Specifies properties over time, e.g.:

• LTL: "After every Withdraw, the balance must not go negative." G(Withdraw → X(F(balance ≥ 0)))
• CTL: "There exists a path where the account is never overdrawn." E[](balance ≥ 0)

Example: Bank Loan Repayment

3. Theorem Proving and Model Checking

A. Theorem Provers (Coq, Isabelle)

Prove properties mathematically (e.g., cryptography, compilers).

• Example: WhatsApp’s Signal Protocol uses Coq to verify key exchange.
• Nepalese Use Case: Ncell’s SIM authentication could be formally verified.

B. Model Checkers (SPIN, NuSMV)

Exhaustively test finite-state systems for errors.

• Example: Check if NTC’s routing table can cause loops.

Model Checker Query: "Does a path exist where a packet cycles infinitely?"

4. Refinement: From Spec to Code

Refinement preserves correctness while adding detail. Example:

1. Abstract Spec (Z): balance' = balance − amount ∧ amount ≤ balance
2. Refined Spec (Pseudocode):

   def withdraw(account, amount):
       if amount > account.balance:
           raise Error("Insufficient funds")
       account.balance -= amount
   

3. Executable Code (Python):

   class Account:
       def __init__(self, balance=0):
           self.balance = balance
       def withdraw(self, amount):
           assert amount <= self.balance, "Insufficient funds"
           self.balance -= amount
   

Real Tie: eSewa’s "reverse transaction" logic could be refined from a B spec to actual code.

5. Tools and Workflow

In the Real World

1. eSewa’s Transaction Contracts

   • Idea Used: B Method to specify "deduct fee before refund" rules.
   • How: A B machine defines Transaction states (Pending, Processed, Refunded) with invariants like fee_deducted → refund_allowed. The prover ensures no double-refunds.

2. NTC’s Network Routing

   • Idea Used: Z Notation for interface specs.
   • How: NTC’s routers use Z schemas to define RouteTable operations (e.g., AddRoute ≡ ΔRouteTable ∙ new_entry ∈ allowed_ips). Model checking verifies no loops.

3. NEPSE’s Trading System

   • Idea Used: Finite State Machines for order lifecycle.
   • How: Orders transition Placed → Matched → Executed → Settled. FSMs catch invalid states (e.g., Settled → Matched).

4. Ncell’s SIM Authentication

   • Idea Used: Theorem Proving (Coq).
   • How: The SIM card’s challenge-response protocol is verified in Coq to prevent replay attacks.

Worked Example: Kathmandu Traffic Light Controller

Problem: Design a traffic light system with 3 states (Red/Yellow/Green) and timers. Use Z to specify, then refine to code.

Step 1: Z Specification

TRAFFIC_LIGHT
  state : {RED, YELLOW, GREEN}
  timer : ℕ
INVARIANT
  timer ≤ MAX_TIME
OPERATIONS
  Tick ≡
    state = RED ∧ timer = MAX_TIME ⇒ state' = GREEN ∧ timer' = 0
    ∨ state = GREEN ∧ timer < MAX_TIME ⇒ state' = state ∧ timer' = timer + 1
    ∨ state = GREEN ∧ timer = MAX_TIME ⇒ state' = YELLOW ∧ timer' = 0
    ∨ state = YELLOW ⇒ state' = RED ∧ timer' = 0

Step 2: Refinement to Pseudocode

class TrafficLight:
    def __init__(self):
        self.state = "RED"
        self.timer = 0
        self.MAX_TIME = 30

    def tick(self):
        if self.state == "RED" and self.timer == self.MAX_TIME:
            self.state = "GREEN"
            self.timer = 0
        elif self.state == "GREEN":
            self.timer += 1
            if self.timer == self.MAX_TIME:
                self.state = "YELLOW"
                self.timer = 0
        elif self.state == "YELLOW":
            self.state = "RED"
            self.timer = 0

Step 3: Model Checking

Use SPIN to verify:

• No state is skipped (e.g., GREEN → RED is invalid).
• Timer resets correctly.

Real Tie: Kathmandu’s traffic lights could use this spec to avoid deadlocks.

Advantages and Limitations

Exam Tip

1. Define Formal Specs Clearly

   • Start with: "Formal specification is a mathematical description of a system’s requirements using [language, e.g., Z/B] to eliminate ambiguity."
   • Must-mention: Notation, semantics, and tools (e.g., "Z uses schemas and predicate logic").

2. Compare Languages

   • Z: Best for data-centric specs (e.g., databases).
   • B: Best for refinement (e.g., safety-critical systems).
   • VDM: Best for algorithmic specs (e.g., sorting).
   • Example Answer:

     "Z is ideal for specifying NEPSE’s account invariants (e.g., balance ≥ 0) because its schema calculus clearly separates state and operations. In contrast, B’s refinement approach would suit NTC’s routing protocols, where we start with abstract RouteTable specs and refine to executable code."

3. Model-Based Questions

   • For FSMs/Petri nets:
     • Draw the diagram.
     • Label states/transitions clearly.
     • Explain one invariant (e.g., "No two transitions can lead to Delivered without PickedUp").
   • For theorem proving:
     • Show a small proof sketch (e.g., "Assume P → Q and Q → R; then P → R by transitivity").

4. Real-World Links

   • Nepalese Context: Always tie to eSewa (contracts), NTC (routing), or NEPSE (trading).
   • Example:

     "Like eSewa’s transaction system, a formal spec for a bank loan would use Z to define Loan states (Approved, Disbursed, Repaid) and operations like Repay with preconditions (e.g., amount ≤ outstanding)."

5. Avoid Common Pitfalls

   • ❌ "Formal methods are always better." → Correct: "They are cost-effective for safety-critical systems but may be overkill for simple apps."
   • ❌ Vague diagrams → Draw mermaid/figures with labeled arrows/states.
   • ❌ Ignoring tools → Mention Atelier B for B, SPIN for Petri nets.

Final Checklist for Full Marks:

• Defined formal spec + compared Z/B/VDM.
• Showed one worked example (e.g., eSewa/Z or traffic light).
• Included real-world ties (Nepalese tech + how specs apply).
• Drew at least 3 visuals (FSM, Z schema, refinement steps).
• Discussed tools (e.g., Coq for proving, SPIN for checking).
• Balanced pros/cons with exam-relevant trade-offs.