University of Minnesota
Software Engineering Center

You are here

Lucas Wagner

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.

Development of Security Software: A High-Assurance Methodology

This paper reports on a project to exercise, evaluate and enhance a methodology for developing high assurance software for an embedded system controller. In this approach, researchers at the National Security Agency capture system requirements precisely and unambiguously through functional specifications in Z. Rockwell Collins then implements these requirements using an integrated, model-based software development approach. The development effort is supported by a tool chain that provides automated code generation and support for formal verification.