Short Bio:
Marina Egea is holding a posdoctoral position at IMDEA Software Institute.
Previously she held a posdoctoral position in the Information Security Group at ETH Zurich.
She received her doctoral degree in Computer Science at the University Complutense of Madrid in 2008.
Her thesis proposes an executable formal semantics
for a significant subset of OCL, which is based on a novel mapping from UML
models with OCL expressions to equational theories which are proved to be
Church-Rosser and terminating and are shown to allow rigourous analysis and
validation of the corresponding model.
She received her bachellor degree in Mathematics from the University of Granada in 2001,
and her Master Thesis from the University Complutense of Madrid in 2005 by the Department of Computer Science.
Her research focuses on the use of formal methods for improving the quality of software engineering products.
She is actively involved in the development of a research line on
rigorous, tool-supported modeling and validation of software systems. In this context,
some of her recent and current research (in collaboration with other authors)
is focused
- on the integration of security policies in system design
models, and on the automatic analysis of the resulting security-design models,
in a semantically precise and meaningful way, either by using OCL queries over
the metamodels of the modeling languages involved
or by mapping OCL constraints to first order logic in order to check their satisfiability;
-
on the automatic transformation of system design models along with their security properties in order to automatically generate redundant security integrated in the application code
at the persistent and backend layers,
and at the frontend layer;
-
on providing a formal semantics for model-to-model transformations languages in order to automatically verify their correctness
with respect to pre- and post-conditions;
-
on bridging the gap between the software design and deployment phases by helping the fully automation of the code generation process
with proposing and implementing a mapping from OCL to SQL.
In this manner, the database is automatically made aware of the constraints discovered early, in the analysis phase, and a flexible and accurate modeling of the access to data is enabled
which is made part of the final functionality of the system automatically, as an output of the code generation process.
The results of this research has been implemented
in various tools for modeling and validating security-design
models and for its automated transformations. For further information see "Software Systems" below.
Keywords:
Model driven software engineering.
Model transformations.
System design, analysis, validation and verification.
Security models, transformation and enforcement.
Formal methods.
Code generation.