Formal Verification Basics: The Science of Ensuring System Integrity
In an age where digital systems underpin everything from banking to transportation and even our household gadgets, ensuring their correct
functioning is paramount. One of the techniques that has gained prominence in ensuring the trustworthiness of these systems is "Formal
Verification". But what exactly is it? Dive in as we demystify the world of formal verification.
What is Formal Verification?
At its core, formal verification is a method used to prove or disprove the correctness of digital systems (like software or hardware components) against a
certain formal specification or property, using formal methods of mathematics.
Imagine writing a contract for building a house. You specify the number of rooms, the size of the kitchen, the position of windows, and so forth. Once the
house is built, you then verify if all these specifications have been met. Similarly, formal verification checks if a digital system meets its specifications.
Key Concepts in Formal Verification
- Specification: Before verifying a system, you need to clearly define what it's supposed to do. This is
done using a formal language, often mathematical in nature, to avoid ambiguity.
- Model: This represents the system you're trying to verify. It can be a piece of software, a digital circuit,
or any other system that can be modeled mathematically.
- Verification: This is the process of ensuring the system (model) adheres to its specification.
There are three primary methods:
Figure 1: Formal verification methods
- Model Checking: An exhaustive search through all possible states of the model to ensure that the system adheres to its specification. If the system
is found to violate the specification, the model checker typically provides a counterexample to demonstrate the failure.
- Theorem Proving: This involves proving mathematically that the system adheres to its specification. Unlike model checking, which is automated, theorem
proving often requires human intervention and insights to guide the proof.
- Equivalence Checking: Equivalence checking is the process of determining whether two systems (often two representations or levels of the same system)
are functionally identical. It asserts that under all possible inputs or conditions, both systems produce the same outputs or behave identically.
Properties to Check:
- Safety Properties: These ensure that something bad will never happen. For example, in a train system, two trains should never be on the same track at the same time.
- Liveness Properties: These ensure that something good will eventually happen. For example, if a train is waiting at a signal, it should eventually get a green light.
- Temporal Logic: This is often used to specify properties of systems. Temporal logics allow us to reason about
sequences of events and their ordering. Common temporal logics include Linear Temporal Logic (LTL) and Computation Tree Logic (CTL).
In the following, let’s go in detail of each key concept one by one.
What is a Specification?
A specification is a detailed description of the design and operational characteristics of a system or component. It precisely describes what a system is supposed
to do, how it should behave, or what properties it should have. Specifications are often written using formal languages or notations to avoid ambiguities.
Example: Elevator System Specification
Consider a simple elevator system. Here's a basic specification:
Figure 2: A simple elevator system
- The elevator is on the ground floor when powered on.
- When a floor button inside the elevator is pressed, the elevator should move to that floor.
- When a call button is pressed on any floor, the elevator should move to that floor to pick up the passenger.
- The elevator door should not close if there's an obstruction.
- The elevator should not move if its doors are open.
- The maximum waiting time for the elevator, after a call button is pressed, should be 2 minutes.
- The maximum time for the door to open or close should be 5 seconds.
- The elevator should not operate if the weight inside exceeds its maximum weight capacity.
In this example, the specification provides clear guidelines about how the elevator system should behave in various scenarios, and these guidelines
can be used to design, test, or verify the elevator system.
What is a Model?
In the context of formal verification, a "model" represents a mathematical or formal representation of the system you're trying to verify. The
model captures the essential behaviors and characteristics of the system, abstracting away unnecessary details to make the verification process
Using the Elevator System example:
- Each floor can be a state (e.g., Ground, First, Second, ...).
- Additional states for scenarios like "moving up", "moving down", "doors open", "doors closed", "over capacity", etc.
- From the "Ground" state, if the call button for the First floor is pressed, there might be a transition to the "moving up" state.
- From the "moving up" state, when the elevator reaches the First floor, transition to the "First" floor state and possibly to the "doors open" state.
- A variable to keep track of the current weight inside the elevator.
- Variables to keep track of which floor buttons have been pressed, or where calls are coming from.
- "door open" event when the elevator reaches the requested floor.
- "door close" event, either after a certain time or when a specific button is pressed.
- "move up" or "move down" actions based on the calls or buttons pressed.
In formal verification, a constraint is a condition or a limitation defined on the behavior or properties of a system. It represents bounds or
requirements that system behaviors must respect. Constraints provide a way to limit the scope of verification, filter out unwanted behaviors, or
define specific conditions that must hold for the correctness properties to be valid. Possible constraints from the elevator example can be:
- Transitions to "moving" states only when "doors closed".
- No transition if weight exceeds capacity.
This model abstracts away intricate details like the mechanics of the elevator, electrical circuits, or the exact speed of the elevator. Instead,
it focuses on the core behaviors and sequences of operations that we want to verify against our specifications. In formal verification, this model
would then be used with tools or techniques like model checking or theorem proving to ensure it adheres to the given specifications.
What is Model Checking?
Model checking is an automated method for verifying if a given system model meets its specifications. It systematically explores all possible states
and transitions in the model to check if they adhere to the desired properties specified.
Given the Elevator System:
Let's conceptualize this with a simple state diagram:
Figure 3: Simplified state diagram of an elevator system
(Note: This is a very simplified version; the real state space, especially for an elevator, is much more complex.)
Using Model Checking on the Elevator System:
- State Exploration: The model checker will start at an initial state (e.g., Ground with Doors Open) and then explore all possible transitions
and states from there (e.g., Doors Closed -> Move Up -> First Floor).
- Safety Property Check: The model checker will ensure that, from any state, there isn't a transition that violates safety properties. For example,
the model should never transition from a "doors open" state directly to a "move up" state.
- Liveness Property Check: The model checker will ensure properties like "if a call button is pressed on any floor, the elevator will eventually
arrive at that floor."
- Feedback: If the model fails to meet the specification, the model checker will provide a counterexample showing the sequence of transitions that
lead to the violation. For instance, if there's a scenario where the elevator moves with its doors open, the model checker would provide that sequence
of actions as an error.
- Loop Detection: Modern model checkers can detect loops in the state space (e.g., elevator keeps moving up and down without stopping) to ensure it
doesn't get stuck in infinite loops during verification.
- State Explosion Problem: One challenge in model checking is that the number of states can grow exponentially with the size of the system (many
possible floor requests, door actions, etc.). Efficient algorithms and techniques, such as Binary Decision Diagrams (BDDs), are used to manage and
represent large state spaces.
Model checking is especially useful because it's automated and exhaustive; it checks all possible scenarios, including edge cases that human testers might overlook.
However, due to the state explosion problem, it may not be feasible for very complex systems unless appropriate abstractions or optimizations are made.
What is Theorem Proving?
Theorem proving is a method used to prove or disprove the correctness of certain properties of a system using deductive reasoning and formal logic. Unlike model
checking, which is an exhaustive, automated exploration of all states, theorem proving involves constructing a logical argument to demonstrate the truth or
falsehood of a statement about a system.
Using Theorem Proving with the Elevator System:
Imagine you want to prove the safety property: "The elevator will never move unless its doors are closed."
- Define Propositions:
- Let P be the proposition: "The elevator is moving."
- Let Q be the proposition: "The elevator doors are closed."
- Logical Argument:
- Your goal is to prove that whenever P is true, Q must also be true. This can be represented as P→Q (If P then Q ).
- Construct Proof:
- Using axioms (basic truths) and rules of inference, you'd construct a logical proof that demonstrates the truth of P→Q.
For complex systems, theorem proving can involve leveraging automated theorem provers or proof assistants to help guide and check the proof, but human
intuition and expertise are often required.
Differences between Theorem Proving and Model Checking:
|Exhaustive, automated state-space exploration. Checks all possible states and transitions against specifications.
|Deductive reasoning. Constructs logical arguments to demonstrate properties.
|Highly automated, but may be infeasible for large state spaces due to the state explosion problem.
|Can be semi-automated with proof assistants, but often requires human intuition and expertise.
|If a property is violated, provides a counterexample (a sequence of states leading to the violation).
|Produces a proof of correctness (or a proof of violation). Does not necessarily give counterexamples in the same way as model checking.
|Best suited for systems with finite and reasonably sized state spaces.
|Can handle both finite and infinite systems and can reason about more abstract properties.
Using the elevator example, while model checking would examine every possible sequence of events (like pressing buttons, moving floors,
opening/closing doors) to ensure no safety violations, theorem proving would attempt to construct logical arguments that prove (or disprove)
specific properties, like the elevator never moving with its doors open.
What are Safety Properties?
Safety properties are a class of properties that ensure "nothing bad happens" during the operation of a system. They are often used in formal verification
to guarantee that a system doesn't enter into undesirable or dangerous states.
Using the Elevator System as an Example:
- Doors Safety: The elevator should not move unless its doors are fully closed.
- This ensures that passengers aren't at risk of falling out or getting caught between moving parts.
- Weight Limit Safety: The elevator should not operate if the weight inside exceeds its maximum weight capacity.
- This ensures that the elevator doesn't get overloaded and risk a mechanical failure or become stuck between floors.
- Emergency Stop Safety: If the emergency stop button is pressed, the elevator should halt its operation immediately.
- This ensures that in the case of perceived danger or malfunction, occupants can stop the elevator's movement.
- Interruption Safety: If an obstruction is detected while the doors are closing, they should re-open.
- This ensures that objects or individuals aren't trapped or squeezed by the closing doors.
In essence, safety properties in the context of the elevator system ensure that during its operations, no scenarios occur that might compromise
the safety of its passengers or the integrity of the system itself.
What are Liveness Properties?
Liveness properties guarantee that "something good eventually happens" in a system. They are used in formal verification to ensure that a system
doesn't become unresponsive, stuck, or deadlocked, and that it will eventually make progress.
Using the Elevator System as an Example:
- Response Liveness: If a floor button inside the elevator or a call button outside the elevator is pressed, the elevator should eventually move to that floor.
- This ensures that users aren't left waiting indefinitely.
- Door Operation Liveness: After the elevator arrives at a requested floor, the doors should eventually open.
- This ensures that passengers can enter or exit the elevator.
- Return to Default Liveness: If the elevator stays idle for a long time at a non-default floor without any input, it should eventually
return to a default floor (e.g., the ground floor).
- This is often implemented in buildings to ensure that elevators are available on primary floors when not in use.
- Emergency Resolution Liveness: If the emergency stop button is pressed, the elevator should eventually resume operation once the emergency
situation is cleared.
- This ensures that the elevator doesn't remain stuck indefinitely after an emergency stop.
In essence, liveness properties for the elevator system ensure that it remains operational and responsive to user requests and that it doesn't get stuck
in a particular state or operation indefinitely.
What is Temporal Logic?
Temporal logic is a type of formal logic that allows for reasoning about the ordering of events and the progression of time. It extends classical propositional
logic by introducing operators that capture temporal aspects, such as sequences of events, their concurrency, and their causality. Temporal logic is particularly
useful in specifying and verifying properties of reactive systems, like computer programs, digital circuits, and communication protocols.
There are different types of temporal logics, with the most common ones being:
Linear Temporal Logic (LTL):
This logic operates on linear time, where time progresses in a sequence of discrete steps or states. Common operators in LTL include:
For example, in the context of a software system, an LTL formula might express that "eventually, every request will receive a response".
- X (Next): A property will hold in the next state.
- F (Eventually): A property will hold at some point in the future.
- G (Globally/Always): A property will hold in all future states.
- U (Until): A property will hold continuously until another property becomes true.
Computational Tree Logic (CTL):
Unlike LTL which assumes a linear progression of time, CTL works with branching time, where multiple possible future paths
(branches) can emerge from a single state. Key operators in CTL include:
An example CTL formula might be "Along some execution paths, a system might deadlock, but there are always paths where it doesn't."
- E (Exists path): There exists a path where a property holds.
- A (All paths): On all paths, a property holds.
Temporal logic provides a way to specify properties of systems in a way that captures time-based behavior. This makes it invaluable in formal methods,
especially in model checking, where it's used to express properties that the system should (or shouldn't) satisfy as it evolves over time.
The Power and Pitfalls of Formal Verification
- Rigorous method, backed by mathematical certainty.
- Can catch errors that might be overlooked in standard testing.
- Offers stakeholders enhanced trust in system reliability.
- Highly reliant on the correctness of the specification. A flawed spec leads to flawed verification.
- The process can be time-consuming and computationally intense.
- Some real-world scenarios, especially involving external systems, might be challenging to model comprehensively.
Formal verification application on smart contracts can further be explored in the following articles:
As our reliance on digital systems amplifies, ensuring their foolproof behavior is non-negotiable. Formal verification, with its methodical and
mathematical underpinnings, emerges as a beacon of reliability. From the chips that power our devices to financial smart contracts, formal
verification techniques are silently but surely safeguarding our digital futures. In future, we will explore more application scenarios of
formal verification on smart contracts.
Truscova comes with 30+ years of academic research and hundreds of academic publications which pioneered the area of Formal Verification.
The team combines academic leadership, industrial strength and Blockchain expertise. Truscova currently analyzes Solidity code combining Formal
Verification techniques: abstract interpretation, constraint solving, theorem proving, and equivalence checking.