Skip to content
STIMSMITH

Model-Based Verification

Technique WIKI v1 · 5/30/2026

Model-Based Verification is a verification technique that checks an implementation against high-level behavioral models or model-derived properties. Evidence here covers software, cyber-physical, automotive, and RISC-V processor contexts: models can be derived from Java bytecode, transformed from EAST-ADL/Simulink/Stateflow into UPPAAL-family models, or used as golden/reference models for trace comparison in CPU verification.

Overview

Model-Based Verification uses an explicit behavioral model, or a model derived from an implementation, as the basis for checking whether a system satisfies intended correctness conditions. In software analysis, the technique is described as a way to express behavioral correctness conditions—such as valid execution states, variable bounds, and timing—at a high level of abstraction and then affirm that those conditions are satisfied by the software system.

The model may be hand-authored in a domain-specific modeling language, generated from program artifacts, or embodied as a reference implementation used for comparison. The common theme is that verification is driven by a model-level description of expected behavior rather than only by ad hoc tests.

Typical workflow

A model-based verification flow usually includes some combination of the following steps:

  1. Create or derive a model. Evidence includes a framework that automatically derives behavioral models from Java bytecode using EMF/ECore technology, then transforms them into timed automata for model checking.
  2. Translate the model into a verifiable formalism. In cyber-physical and automotive examples, EAST-ADL, Simulink, and Stateflow models are transformed into UPPAAL or UPPAAL-SMC models.
  3. State correctness properties. Properties may cover functional behavior, non-functional constraints, execution-state validity, variable boundaries, timing, or probabilistic/stochastic behavior.
  4. Analyze the model or compare implementation behavior against it. Model checkers such as UPPAAL, UPPAAL-SMC, and Simulink Design Verifier are used in the cited public context. In processor verification, a generated test can be executed on both a golden model and a processor under development, with divergences found by comparing execution traces.
  5. Reduce or explain failures. TestRIG-related evidence describes shrinking and simplification of failing RISC-V instruction sequences so that counterexamples are easier to understand.

Relationship to formal verification

Model-Based Verification often overlaps with Formal Verification when the model is translated into a formal representation and analyzed by a model checker. For example, one cited autonomous-vehicle workflow transforms Simulink/Stateflow behavior, constrained by EAST-ADL, into UPPAAL models with stochastic semantics and then applies formal statistical analysis techniques. Another cited software-analysis workflow emits timed automata that can be processed by a model checker such as UPPAAL.

Examples from the evidence

Software model derivation

A public source describes a model-derivation framework for Java programs. The framework creates an initial model from Java bytecode, applies transformations that simplify the model, and eventually outputs a timed-automata model suitable for model checking. The stated goals include keeping models consistent with software, making the derivation process extensible, scaling to real-sized programs, and preserving model expressiveness.

Cyber-physical and automotive systems

A public source on autonomous-vehicle verification describes a model-based verification and validation flow for cyber-physical systems. It extends EAST-ADL constraints, integrates Simulink/Stateflow in a tool chain, transforms models into UPPAAL models with stochastic semantics, and performs analysis of functional and non-functional properties using Simulink Design Verifier and UPPAAL-SMC.

RISC-V processor verification with TestRIG

In the TestRIG evidence, generated RISC-V test programs can be executed on both a golden model and a processor in development, with divergences detected by comparing execution traces. TestRIG’s Verification Engine can stimulate one or more RVFI-DII-compatible RISC-V implementations, use an internal RISC-V model, or drive two independent implementations and compare their RVFI traces. The same evidence also notes that instruction sequences may be loaded from disk, generated randomly, or produced through interactive architecture-driven state-space exploration.

TestRIG-related evidence also describes practical counterexample handling: once QCVEngine finds a counterexample, QuickCheck shrinking and additional smart-shrinking transformations remove irrelevant instructions or simplify the sequence while preserving the failure. Sequences can also include assertions, making it possible to fail without a divergence and to test limits of implementation-defined behavior.

Benefits and trade-offs

Model-Based Verification can raise the level of abstraction for correctness arguments and can connect implementation behavior to explicit models, model checkers, or golden-reference traces. The cited sources emphasize benefits such as high-level property expression, automated model derivation, translation into model-checker input, analysis of functional and non-functional properties, and reduction of failing counterexamples.

The cited sources also show practical challenges: expressive models can be difficult to create and maintain by hand, generated counterexamples can be long or convoluted, and test-generation or reduction frameworks may need special support for branches, trace comparison, and reusable interfaces.

LINKED ENTITIES

3 links
TestRIG USES
JasperGold USES
formal verification USES

CITATIONS

8 sources
8 citations
[1] Model-based verification expresses behavioral correctness conditions such as execution-state validity, variable bounds, and timing at a high level of abstraction and checks that software satisfies them. A Model-Derivation Framework for Software Analysis
[2] A Java software-analysis workflow can derive models from bytecode, simplify them through transformations, and output timed automata for a model checker such as UPPAAL. A Model-Derivation Framework for Software Analysis
[3] An autonomous-vehicle workflow transforms EAST-ADL/Simulink/Stateflow models into UPPAAL models with stochastic semantics and analyzes functional and non-functional properties using Simulink Design Verifier and UPPAAL-SMC. Model-based Verification and Validation of an Autonomous Vehicle System
[4] In RISC-V verification, generated test programs can be executed on both a golden model and a processor in development, with divergences detected by comparing execution traces. Randomized Testing of RISC-V CPUs using Direct
[5] TestRIG uses a Verification Engine that can stimulate RVFI-DII-compatible RISC-V implementations, use an internal RISC-V model, or compare RVFI traces from two independent implementations. Randomized Testing of RISC-V CPUs using Direct
[6] TestRIG instruction sequences may be loaded from disk, generated randomly, or produced with interactive architecture-driven state-space exploration. Randomized Testing of RISC-V CPUs using Direct
[7] QCVEngine and QuickCheck use shrinking and smart-shrinking transformations to simplify failing RISC-V instruction sequences while preserving counterexamples. Randomized Testing of RISC-V CPUs using Direct
[8] TestRIG-style sequences can include assertions, enabling failures without tandem-verification divergence and supporting tests of implementation-defined behavior. Randomized Testing of RISC-V CPUs using Direct