Glossary

Verification

Verification is the process of analyzing the correctness, safety and liveness of a modeled system.

Verification is the process of analyzing the correctness, safety, and liveness of a modeled system before deployment. It ensures that the system behaves as expected, e.g. that it is free from deadlocks, livelocks, starvation and other undesired states and inconsistencies, and that it meets certain standards. Verification is separate from "validation".

Correctness

Checking correctness involves ensuring that the process does what it is supposed to do, according to its goals and requirements, e.g. that an Order is always moved through specific desired stages and is always eventually Fulfilled (or ends up in some other desired terminal state, such as Cancelled).

Safety

There are also things that we want processes to not do, and safety requirements specify what states we do not want a process to end up in. For example, creating a Refund for an Order without any Payment Confirmation. Some rules about what must or must not happen in in the system can be defined as either correctness conditions that must hold at all times ("invariants"), or negatively as safety requirements that must not be violated.

Liveness

Part of model verification involves checking that nothing is unexpectedly blocking progress, and that something desired eventually happens ("liveness"). Several things can prevent this.

Livelocks

A livelock occurs when a process is constantly active but makes no real progress—it keeps executing but never reaches completion, e.g.

→
A process keeps looping due to incorrect conditions, e.g. a loop checks for an approval condition but never exits if the condition is never met.
→
Two processes keep retrying an action that fails (e.g. because they are in competition for the same resource) instead of resolving a conflict.

Deadlocks

A deadlock happens when a process gets stuck indefinitely with no activity, e.g.

→
if a process requires manual approval but no user completes it
→
because two or more tasks are waiting for each other to complete
→
technical deadlocks such as two tasks waiting on each other to release a lock on a database row

Potential solutions include:

→
timeouts and escalation paths for user tasks
→
avoid mutual dependencies between tasks
→
strategies to avoid database deadlocks, e.g.
- →
  use optimistic locking, or
- →
  (if the system requires pessimistic locking) consistent ordering of lock acquisition (i.e. make sure that Task A and Task B will always attempt to lock the same rows in the same order, so they can’t end up in a situation where one locks X then waits for Y, and the other locks Y then waits for X)

Starvation

Resource starvation happens when a transaction or process waits indefinitely because it can’t get access to a resource due to other higher-priority tasks always taking precedence.

Verification in HASH

Processes (Flows)

Processes in HASH are represented as what mathematicians call "Petri nets". Unlike many representations of process models, Petri nets can be formally verified, which means we can check their integrity in a number of different ways, including by looking at properties such as:

→
Reachability

→
A state is considered reachable if it can be achieved from an initial marking by firing a sequence of transitions.
→
Helps determine if a process can get stuck or fail to reach a goal state.
→
Example: Can an order-processing system always reach the "Order Completed" state?
→
Verification: Construct a reachability graph and uses state-space exploration to check if any given target state can be reached.

→
Boundedness (Safeness)

→
A Petri net is k-bounded if no place contains more than k tokens at any time.
→
A 1-bounded net (Safe Petri Net) ensures that places hold at most one token, preventing overflow issues.
→
Helps prevent resource exhaustion in concurrent systems.
→
Verification: Analyze the incidence matrix and state-space exploration to check if any place can exceed k tokens.

→
Liveness

→
A Petri net is considered live if all transitions remain potentially fireable (i.e. no part of the system permanently stops working).
→
Ensures that no process is permanently blocked (e.g. there are no deadlocks).
→
Example: In an order-processing workflow, if all necessary conditions are satisfied (e.g., payment confirmed, stock available) but the "Dispatch Order" transition still never fires, there is a liveness problem. This could indicate a deadlock or some other form of blocking that prevents the system from progressing.
→
Verification: Uses a reachability graph to check if every transition is eventually fireable. Repeating execution cycles that fail to progress are indicative of livelocks, and a state from which no further transitions are possible deadlocks.

→
Fairness

→
Ensures that all transitions have a chance to fire, avoiding starvation.
→
Important in concurrent and distributed systems, where some processes should not dominate resource usage.
→
Example: In a ticketing system, fairness ensures that all users eventually get service rather than some requests being delayed indefinitely.
→
Verification: Check reachability properties to detect transitions which are never executed.

Right now, process modeling in HASH is in beta, and we have not yet built in support for the above formal verification techniques, although hope to in the future.

Create a free account

By signing up you agree to our terms and conditions and privacy policy