University of Minnesota
Software Engineering Center

You are here

David Greve

Recent Publications

Model Checking Information Flow

Information flow modeling describes how information can be transferred between different locations within a software and/or hardware system. In this chapter, we define a notion of information flow based on traces that is useful for describing flow relations for synchronous dataflow languages such as SimulinkĀ® and SCADEā„¢ that are often used for hardware/software co-design. We then define an automated method for analyzing information flow properties of Simulink models using model checking. This method is based on creating a flow model that tracks information flow throughout the model.