It's my face

Natasha Jarus

Currently working on a Ph.D in Computer Engineering in the SeNDeComp research group, advised by Dr. Sahra Sedigh Sarvestani.




: Abstract Interpretation of Cyber-Physical System Models

transformation diagram

When designing or analyzing a complex system, several models of that system must be created and evaluated. Generating these models is a labor-intensive and error-prone process. Furthermore, as the system's architecture evolves through the design process, each model must be updated to reflect the latest changes. Model transformation tools can simplify this process by automating some or all of the model creation and update process.

We view models as partial syntactic representations of a system, much as source code is a syntactic representation of a program. Through this lens, we can apply program analysis techniques to system analysis. Abstract Interpretation is one of these techniques. Originally developed as a static program analysis tool, Abstract Interpretation sidesteps the issue of the halting problem in program analysis by providing syntactic transformations between a program's source code and a properties domain that describes a property of the program we want to analyze. The transformation process is guaranteed to be correct, but it may sacrifice specificity in order to produce a result. For example, if we want to know whether a program outputs a negative or positive number, Abstract Interpretation may inform us that either outcome is possible.

To transform models with Abstract Interpretation, we first define a properties domain that captures the relevant aspects of cyber-physical systems we are concerned with. Then we define transformation operations for each modeling domain we desire to operate on, allowing us to abstract system properties from these models and to concretize models from a given collection of system properties. This process can be proven to be correct; furthermore, we can improve the specificity of our results through the properties of the structures used in this transformation process.