Seminars

Detecting Data Store Access Conflict in Simulink by Solving Boolean Satisfiability Problems
Zhi Han, MathWorks, Natick, Massachusetts

04/02/2010, 11am, GHC-6501

Abstract

In this talk I will discuss a method to statically analyze a Simulink model to detect two potential problems with the use of Merge block and 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.

Biography

Zhi Han is a former member of Specification and Verification Center at Carnegie Mellon University. He received his Ph.D. with prof. Bruce Krogh in ECE in December, 2005. He is currently a software developer at the MathWorks working on the execution engine of Simulink. He is currently maintaining the hybrid system verification tool CheckMate. His research interests include model based embedded system design and analysis, hybrid systems, large-scale system modeling and analysis.