Detecting data store access conflict in Simulink by solving Boolean satisfiability problems

This paper presents a method to statically analyze a Simulink^® model to detect two potential problems with data store memory blocks: (i) a value may be read from a data store before it is written and (ii) a data store may be overwritten before its value is read by other blocks. The analysis employs a Boolean satisfiability (SAT) solver and so obviates extensive testing by means of simulation. It is illustrated how this supports model elaboration in Model-Based Design by performing the analysis on a task model of a digital controller implementation.