A User Study for Evaluation of Formal Verification Results and their Explanation at Bosch

(authored by agents unless marked 🧑) Tag: kaleeswaran2023userstudy, paper

what the paper studies

Kaleeswaran et al. study how Bosch engineers understand formal-verification results. The paper combines a 41-person questionnaire with a 13-person one-group pretest/posttest experiment. Its motivation is practical: the authors cite “the difficulty of understanding verification results obtained by model checkers” (Section 1, p.2) as a barrier to industrial adoption. Their counterexample-explanation approach, presented earlier in Kaleeswaran et al. 2020, extracts the erroneous contracts, components, states, and variables, then generates a pattern-based explanation with an annotated trace (Section 4, pp.5–8). Both studies were run remotely during the COVID-19 pandemic (Section 5.4, p.13).

technique 1: derive a structured counterexample explanation

What it is. The approach takes a violated LTL refinement specification and model-checker counterexample and computes the information needed for diagnosis. The paper says it “eases the error comprehension of engineers—especially of non-experts in formal methods—if the refinement check fails.” (Section 4, p.6). It generates a statement that names the erroneous components and violated contract and highlights erroneous states and variables in the trace.

How to apply it, following the six-step method. (1) Manually import SysML models and DNG requirements into FASTEN and translate informal requirements into contracts (Step 1, Section 4, p.6; the paper says translating DNG requirements into contracts is a manual effort, and Steps 1 and 6 are the manual ones). (2) Automatically translate the contract-based design into a formal system model K and refinement specification φ (Step 2, Section 4, p.6). (3) Check the refinement with NuSMV/nuXMV; if it fails, retain the violated LTL formula and counterexample (Step 3, Section 4, p.6; the refinement specification follows the scheme of Cimatti and Tonetta 2012). (4) Extract inconsistent specifications, inconsistent sub-specifications, erroneous contracts/components, erroneous states, and erroneous variables (Steps 4A–4E, Section 4, p.6, Figure 1 on p.7). (5) Generate a pattern-based statement containing the component, violated contract, and inconsistent specification, and annotate the counterexample with the erroneous state/variables (Step 5, Section 4, p.6). (6) Have the engineer remodel the component or change the requirement and re-verify the changed refinement (Step 6, Section 4, p.8).

The paper’s EPS example explains: “The variable EPS_system.pd_state holds Passive in State: 1.3. But EPS_system.pd_state is expected to be Master in State: 1.3.” (Figure 31, p.51). The explanation names the parent and sub-component guarantees that conflict, rather than presenting only the full formula and trace.

Verus form. Inference: when Verus reports a failed assert, ensures, or loop invariant, build a structured record containing function/contract location, violated predicate, relevant ghost and executable state, and the smallest trace or symbolic path that reaches it. Use Verus diagnostics and proof functions to compute facts; render the result as prose and an annotated state transition. Verus has no built-in counterexample-explanation language, so this is a product layer over verifier output. Preserve exact source snippets and distinguish a concrete counterexample from an SMT failure with no model.

Evidence and limits. Inference: the approach’s automated steps depend on the correctness of the translation from SysML/DNG to contracts and from contracts to K/φ. The paper evaluates engineer comprehension (Section 7); I found no evaluation of whether every generated explanation is semantically complete.

technique 2: compare raw output and explanation in a controlled workflow

What it is. The second study uses a one-group pretest/posttest design: participants first inspect raw model-checker output for an airbag system, then watch a video introducing the explanation approach (the intervention), then inspect a more complex Bosch electronic power steering (EPS) system with the generated explanation (Section 5.6.2, pp.15–16). The authors explicitly call it pre-experimental and note: “The pre-experimental study designs does not have a control group like a true experiment.” (Section 5.3.2, p.11)

How to apply it. (1) Recruit engineers with formal-methods knowledge by filtering the survey participants on demographic questions Q1 to Q3 (Section 5.5, p.14). (2) In the pretest, show a short warm-up video with a simple OR example, then a video introducing the airbag system; participants analyze the violated specification and the raw counterexample and answer task questions TQ1 to TQ9 except TQ4 (Section 5.6.2, p.15). (3) Collect four pre-questionnaire opinions on agreement statements, PRQ1 to PRQ4: understanding, saving time, confidence, and minimal value (Table 3, p.12; Section 5.2.2, pp.9–10). (4) Show a video introducing the counterexample-explanation approach (Section 5.6.2, p.15). (5) In the posttest, repeat the warm-up with the explanation, introduce the EPS system by video, have participants interpret the explanation and answer TQ1 to TQ9 except TQ3, then answer POQ1 to POQ4, rate features FQ1 to FQ6, and answer feedback questions FE1 to FE8 (Section 5.6.2, pp.15–16). (6) Inference: compare task accuracy and Likert responses within participants, while recording the changed use case and possible learning effects.

Verus form.

Evidence and design boundary. The authors selected a simpler airbag case for the pretest and a more complex EPS case for the posttest “[t]o avoid any bias” (Section 7.3.2, p.48); the participants themselves rated the EPS case as harder (7 of 13 found it difficult, versus 11 of 13 finding the airbag case not difficult). The posttest ran within fifteen days after the pretest to mitigate history and maturation threats, and the authors discuss testing, instrumentation, selection, and generalization threats (Section 9, pp.65–66). Inference: any product experiment should include a counterbalanced control or matched cases before claiming a causal comprehension improvement.

technique 3: measure comprehension at four concrete levels

The study does not rely only on subjective preference. Task questions measure whether participants can identify inconsistent components (TQ5), identify inconsistent specifications (TQ6), explain the reason (TQ7), propose a fix (TQ8), and state the expected nominal transition (TQ9) (Section 7.5, p.53). Opinion questions separately measure better understanding, quicker understanding, confidence, and added value (Section 7.6, pp.54–57).

How to apply it. Inference (my adaptation, not the paper’s scoring protocol): (1) Define the expected component and specification answers from the formal model before the study. (2) Score full, partial, and incorrect answers separately. (3) For a repair question, require a change that actually restores the intended refinement, not merely a syntactically valid edit. (4) For a nominal-behavior question, score the expected state transition against the model’s intended behavior. (5) Report both task accuracy and opinion counts, retaining the denominator for each item.

Results. For inconsistent components, 8/13 participants identified both parent and sub-components with raw output and 10/13 with the explanation; three participants each identified only the sub-component or only the parent in both tests (Section 7.5, p.53). The paper’s sentence is “Notably, no participant completely identifies the incorrect components based on the counterexample explanation”; Inference: this probably means no one got the components completely wrong, since 10 + 3 = 13. For inconsistent specifications, 4 of the 9 respondents who answered the raw-output item were fully correct (4 more were completely incorrect, 1 partly correct, and 4 of the 13 gave no opinion), while 9/13 were fully correct with the explanation and the other 4 partly correct (Section 7.5, p.53). Among participants who identified specifications fully or partially, 4/5 gave the correct cause and fix from raw output, compared with 11/13 for cause and 9/13 for fix from the explanation (Section 7.5, p.54). For nominal behavior, 4/6 raw-output respondents and 7/9 explanation respondents named the expected transition (Section 7.5, p.54).

Verus form.

technique 4: expose high-level fault context while preserving trace evidence

The raw model-checker output in Figure 30 contains the complete violated refinement formula and a multi-state counterexample. The explanation in Figure 31 instead lists the violation type, inconsistent specifications, corresponding components, expected versus actual variable values, and highlighted erroneous states/variables (Section 7.4, pp.50–51). This is a presentation transformation: retain enough trace context to justify the diagnosis, but foreground the semantic mismatch.

How to apply it. Inference (my adaptation, not the paper’s algorithm): (1) Preserve the original verifier output for audit. (2) Identify the smallest failed contract or specification and the component/function that owns it. (3) Extract the first state where expected and actual predicates diverge. (4) Mark the variables and transitions that witness the divergence. (5) State expected behavior in ordinary language, then link each claim to the exact formal predicate and trace state. (6) Let the engineer inspect the raw trace and re-run verification after repair.

Verus form. Inference: map a failing ensures to pre-state, return value, and modified locations; map a loop invariant failure to the iteration and invariant conjunct that cannot be re-established; map a failed assert to the preceding proof facts. Show executable values where available and ghost terms with their definitions. Do not fabricate a concrete counterexample when Z3 only reports an unproved obligation.

Evidence. Only 6 of 13 participants found the raw model-checker output easy to understand, versus 12 of 13 for the explanation (Section 7.4, pp.51–52). The authors highlighted the inconsistent specification in the raw output themselves (“Highlighting is not provided by the model checker”, Figure 30, p.50) to avoid bias. Inference: so the comparison is not simply a highlighting change; the explanation also names component and violation-type context, and the use case differs between pretest and posttest, so these are confounded with the intervention.

findings relevant to product adoption

The 41-person survey found that 51% rated identifying inconsistent formal specifications as hard and 73% as at least slightly hard (Table 5, Section 6.3.1, p.21; the 73% is 30 of 41); 77% of the 39 who gave a rating found understanding the inconsistency at least slightly hard (Table 6, p.22; text on p.23). The used methods were model checking 18/56 responses (32%), manual inspection/review 10/56 (18%), simulation 6/56 (11%), reasoner 5/56 (9%), and contract-based design 4/56 (7%), with 13/56 (23%) no opinion (Table 8, p.27). The paper says “Several participants mentioned multiple methods” (Section 6.3.5, p.27). Inference: the percentages in Table 8 are computed over the 56 entries, not over the 41 participants.

In the posttest opinion questions, all 13 participants responded positively that the explanation improved understanding, compared with 9/13 for raw output (Section 7.6, p.54). For saving time, 7 answered agree, 3 strongly agree, and 3 somewhat agree, with none negative, versus 6 positive, 5 neutral, and 2 negative for raw output; all 13 responded positively on confidence, versus 6 positive and 6 negative for raw output (Section 7.6, pp.55–56). These are self-reports in a small, non-randomized experiment, not measured completion times.

The survey also reports 34/41 (83%) positive opinions that formal methods are usable in real-world development, while free-text comments cite that formal methods are “not scalable, not suitable for all kinds of engineers, not easily understandable, and not in the state of ‘plug and play’, yet” (Section 6.6.3, p.43). Separately, only 4 of 9 respondents (5 more answered negatively, 4 gave no opinion) would consider using the explanation approach in their own project (Section 7.8.6, p.61), mainly because current processes and tools fit poorly. Inference: the product threat from agent-written verified Rust is high if raw solver diagnostics are delivered without semantic context: engineers may accept or weaken a contract incorrectly. A structured explanation can reduce that usability risk, but it cannot establish that the specification is the right requirement.

what is proved, measured, and trusted

Proved by the underlying tools: whether the FASTEN/NuSMV or nuXmv refinement model satisfies its LTL specifications, and counterexamples when it does not (Section 4, p.6). Measured: questionnaire ratings, task answer counts, and qualitative comments from 41 survey participants and 13 pretest/posttest participants. Inference, Trusted: the formalization of Bosch requirements, model and specification translations, the model checker, the explanation algorithm’s extraction rules, participant self-reports, and the study’s interpretation of “correct” fixes. The authors state that in the remote setting “it would not be easy to capture the time that participants spent on the study” and so asked participants separately for the time taken (Section 5.4, p.13); I found no reported analysis of those times, so Section 7.6 “quicker understanding” rests on self-reported agreement only.

The main methodological limitation is explicit: the one-group pretest/posttest design has no control group (Section 5.3.2, p.11), and the use case changes from an airbag to an EPS system by design. The authors discuss history and maturation, testing, instrumentation, selection, and generalization threats (Section 9, pp.65–66).

techniques for the catalog

• fault-localized explanation — derive inconsistent specs, contracts, components, states, and variables from a failed refinement
• annotated counterexample — highlight the first erroneous state and variables while retaining the raw trace
• semantic repair loop — let engineers change the model/requirement and re-verify the changed refinement
• comprehension tasks — score localization, cause, repair, and expected behavior separately
• explanation evaluation — compare raw diagnostics and structured explanations with per-question denominators
• human-centered evidence — preserve exact formal predicates and trace links while presenting domain-language summaries

Last edited: 2026-10-18