The problem
BMS protection logic has many interacting conditions: debounce timers, latching, hysteresis, priorities between faults and mode-dependent behaviour. Simulation tests explore only the scenarios someone thought to write. Formal verification can prove that a property holds for all inputs, or produce a counterexample that shows exactly how it fails. Its practical value and limits for real BMS logic are worth measuring rather than assuming.
Objectives
- Model BMS protection and contactor logic in Stateflow with realistic structure.
- Express safety requirements as provable properties, including timed ones.
- Prove properties and analyse counterexamples with Simulink Design Verifier.
- Compare formal verification with simulation testing on seeded defects.
- Study scalability with model size and timer lengths.
What you need
Tools and toolboxes
- Stateflow — BMS protection, contactor sequencing and fault-latching logic.
- Simulink Design Verifier — Property proving with Proof Objective and Assumption blocks, design error detection and test generation.
- Simulink — Property-specification blocks, verification subsystems and simulation of counterexamples.
- Simulink Test — Requirement-based simulation test baseline for comparison.
- Requirements Toolbox (optional) — Linking properties and tests to requirements.
Software
- MATLAB R2023b or later
- Simulink
- Stateflow
- Simulink Design Verifier
- Simulink Test
Extra parts and data
None beyond the software above.
Key concepts
- Property proving
- The verifier searches the model's state space to prove that a property is always true, given assumptions on inputs, or returns a counterexample input sequence that violates it.
- Temporal properties
- Properties involving time, such as 'if cell voltage exceeds the limit for more than 50 steps, charging is disabled within one step'. They are built with Detector, Extender or similar temporal-operator blocks.
- Assumptions
- Constraints on inputs, such as voltage within a sensor range, that limit the proof to realistic behaviour. Too-strong assumptions can make a proof meaningless.
- State-space explosion
- Long timers and many interacting states increase the states to explore, so proofs can time out; abstraction and bounded proving are common responses.
Step-by-step guide
- 1
Define the logic and requirements
Specify BMS logic for an example 16-cell pack: per-cell over- and under-voltage with debounce, pack over-current, over-temperature with latching, a contactor sequence (precharge, then main) with timeouts, and priorities among faults. Write numbered safety requirements such as 'main contactor never closes unless precharge has completed' and 'any latched fault opens contactors within 20 ms'. Write each requirement so it can be checked from observable outputs, since properties can only refer to signals the verification subsystem can see.
Checkpoint: A requirement list with at least ten safety requirements, including timed ones.
- 2
Model the logic
Implement the logic in Stateflow with parallel states for protections and a sequential chart for contactor control, at a 10 ms discrete step. Use counters for debounce rather than absolute-time temporal logic, which keeps proofs simpler. Use integer types for voltages and currents. Simulate a few nominal scenarios to confirm basic behaviour. Keep thresholds and debounce counts as named parameters so they can be varied later in the scalability study without editing the chart.
Checkpoint: Nominal scenarios simulate correctly: precharge completes, main closes, and an over-voltage fault opens contactors after its debounce.
- 3
Detect design errors
Run Simulink Design Verifier's design error detection on the model to find dead logic, unreachable states, integer overflow and division by zero. Review every finding: dead logic often indicates a requirement mismatch. Fix real defects and record them as the first set of findings. Also check that the model meets the verifier's compatibility check before running analyses, since unsupported blocks stop the analysis. Record the time each analysis takes.
Checkpoint: A design error detection report with every finding resolved or explained.
- 4
Write properties
Build a verification subsystem that observes model outputs and encodes each requirement with Proof Objective blocks, using Implies and temporal-operator blocks for timed requirements. Add Proof Assumption blocks for realistic input ranges, such as cell voltage between 0 and 5 V. Keep each property small and linked to one requirement. Write a short sentence beside each property restating it in plain words, which makes reviewing faithfulness to the requirement much easier.
Checkpoint: Every requirement encoded as a property, reviewed by a peer for faithfulness to the requirement text.
- 5
Prove properties
Run property proving with appropriate settings. For each property, record the result (valid, falsified or undecided) and run time. For falsified properties, simulate the generated counterexample harness and see the failing scenario in the chart animation. Decide whether the design, the property or the requirement is wrong. Keep a record of every falsified property and what it led to, since these counterexamples are among the most valuable results. Note the analysis settings used for each run.
Checkpoint: A table of property results with run time, and an analysis of each counterexample.
- 6
Handle undecided properties
If a proof times out, try bounded proving to a depth beyond the longest timer, reduce timer lengths through a parameter while preserving the logic structure, or split the property. Report clearly whether a result is a full proof or a bounded one, because they give different assurance. If you reduce timer lengths, argue clearly why the logic structure, and so the proof, carries over to the original values.
Checkpoint: Each property either proven, falsified with a counterexample, or bounded-proven to a stated depth.
- 7
Build a simulation-test baseline
Independently write requirement-based simulation tests in Simulink Test, as a typical test engineer would, aiming for MC/DC coverage. Ideally have a different person write them without seeing the properties, so the comparison is fair. Run them on the corrected model and confirm all pass. Record the effort spent writing the tests, in hours, so it can be compared with the effort spent writing properties, and keep the suite fixed before mutants are created.
Checkpoint: A passing simulation-test suite with recorded coverage.
- 8
Seed defects
Create a set of seeded defects in copies of the model: off-by-one debounce counts, missing latch, wrong priority, a transition missing a guard, wrong hysteresis threshold. Use 20 or more mutants spread across defect types. For each, run both the simulation suite and the property proofs and record which detect it. Generate mutants systematically, for example one per type per protection function, rather than choosing ones you expect a method to catch.
Checkpoint: A detection matrix of mutants against method.
- 9
Analyse results
Compute detection rates per method and defect type. Look for defects found only by formal verification, often timing corner cases, and those found only by tests, often where properties were too weak or assumptions too strong. Measure effort: time to write properties versus tests, and run times. Present results as a matrix and as rates, and discuss individual interesting mutants in detail.
Checkpoint: Detection rates and effort figures with discussion of the defects each method missed.
- 10
Study scalability
Scale the model: more cells, longer debounce timers, more fault types. Record proof times and how many properties stay decidable. Plot run time against model size. This shows where the approach becomes impractical and which abstractions help. Run each size at least twice to confirm timings are repeatable, keep the analysis time limit the same for every run, and record the machine specification used, so other researchers can compare their own results fairly.
Checkpoint: A scalability plot with the point where proofs start timing out marked.
- 11
Write up
Present the logic, properties, proof results, counterexamples, comparison with testing, mutation results, scalability and threats to validity (property faithfulness, assumption strength, mutant representativeness). Release models, properties and mutants. Avoid claiming that formal proofs make the BMS safe: they prove the model meets the stated properties. Include representative counterexamples as figures, since they show concretely what formal verification found that testing did not.
Checkpoint: A paper-style chapter with results and a threats-to-validity section.
Testing & validation
- Design error detection findings resolved.
- Every requirement encoded as a peer-reviewed property.
- Proof results classified as full, bounded or falsified with counterexamples analysed.
- Seeded-defect detection compared between formal proofs and simulation tests.
- Proof time measured against model size.
Expected results
A formally verified Stateflow BMS protection model with documented proofs and counterexamples, and a quantitative comparison of formal verification against simulation testing on seeded defects, including effort and scalability.
Research angle for your PhD
Research questions: which classes of BMS logic defects does model-level formal verification find that requirement-based testing misses, at what effort, and where does it stop scaling? Metrics: detection rates by defect class, effort to write properties and tests, proof times, fraction of properties fully proven. Baselines: MC/DC-targeted simulation testing and automatically generated tests. Validity depends on faithful properties, realistic assumptions and representative mutants. A rigorous empirical comparison on realistic BMS logic, with released artefacts, is a credible contribution to automotive software verification venues.
Take it further
- Use Design Verifier test generation and compare with hand-written tests.
- Verify the generated code with a code-level static analyser.
- Add cell-balancing logic and its properties.
- Apply contract-based compositional verification to scale further.
Viva and review questions
What does a proven property guarantee?
That the model satisfies that property for every input sequence allowed by the assumptions; it says nothing about requirements that were not encoded, or behaviour outside the assumptions.
Why use counters rather than absolute-time temporal logic?
Counters keep the state space discrete and explicit, which makes proofs faster and the generated code simpler for a fixed-rate task.
How could an assumption make a proof meaningless?
If it is too strong, for example excluding the input values that trigger a fault, the property is proven only for situations where the logic is never tested.
Learn it at DIYguru
These DIYguru courses and programmes teach what this project needs.