Her research interest is in applying mathematically rigorous specification and verification techniques (formal methods) to improve software dependability. In particular, she has contributed to two problem areas. The first is using rigorous means to design security and privacy policies, authorization decision engines, and enforcement mechanisms. She then applies automated and, where needed, manual techniques to verify properties of policies that heighten assurance that security objectives are accurately captured by the policy specifications. Similarly, she verifies correctness of decision procedures and enforcement mechanisms with respect to the policies they are intended to enforce. Her second research area concerns formalizing the semantics of modeling notations that provide software practitioners the ability to generate specifications that can be verified. The modeling notations she studies are used commonly to describe the dynamic behavior of software systems, including statecharts variants, process algebras, UML state machine diagrams, and UML sequence diagrams. Given that it is difficult to assess the properties of models constructed using notations that either have so many variants with subtle differences or have no precise semantics, she seeks to address this problem by providing formal templates to structure their semantics systematically, thus enabling properties of software models to be formally verified. Her research has been supported by grants from NSF, NHARP, Microsoft, NSA (through CMU subcontract), and UTSA TRAC awards.