Professor Day's research is in developing techniques and methodologies to ensure correct system behaviour for software and hardware systems. Her focus is on the use of formal methods, which often uncover subtle bugs that are very difficult to discover using conventional techniques. For example, in the analysis of a separation minima used by air traffic controllers over the North Atlantic Region, Professor Day and her colleagues uncovered three inconsistencies in the specification. Formal methods involve the analysis of mathematically precise descriptions of how systems behave. Formal methods have an advantage over techniques based on testing or simulation in that they examine all possible behaviours of the system.
Professor Day has worked on applications of formal methods ranging from air traffic control systems to microprocessors. In common amongst these diverse applications is the use of high-level models of system behaviour to conquer the complexity of the problem. The use of appropriate system descriptions is often critical to integrating formal methods into existing system development processes. Professor Day's recent work involves the development of configurable model-driven development tools to support the automatic generation of tool support for notations with customizable semantics.
She has experience developing both automated and interactive formal methods tools. Automated tools face limits on the size of the system that can be analyzed. Interactive techniques require more expertise, but make it possible to handle the complexity through decomposition. Future methodologies will build on the strengths of both approaches. Professor Day is a founding member of the Waterloo Formal Methods Lab (WatForm). She is also a member of Waterloo's Software Engineering Lab.
Degrees and Awards
BSc (UWO), MSc (UBC), PhD (UBC)
Industrial and Sabbatical Experience
Professor Day's research has involved collaboration with GM Canada and Critical Systems Labs on the detection of feature interactions in advanced automobiles, AT&T on analysis of a telecommunications protocol, and Intel on microprocessor verification. In the past, she has worked with Raytheon Systems Canada and MacDonald Dettwiler Associates to study applications of formal methods to the Canadian Automated Air Traffic System (CAATS). She also consults on the analysis of system safety.
During her graduate studies, she spent time working with SRI International in Cambridge, UK and Nortel Networks in Ottawa. After completing her PhD, she spent two years as a Postdoctoral researcher at the Oregon Graduate Institute (OGI) in Portland, Oregon.
Amirhossein Vakili and Nancy A. Day, Verifying CTL-live Properties of Infinite State Models using an SMT solver. To appear in Proceedings of ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2014.
Amirhossein Vakili and Nancy A. Day, Reducing CTL-live Model Checking to First-Order Logic Validity Checking. To appear in Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2014.
Adam Prout, Joanne M. Atlee, Nancy A. Day, Pourya Shaker, Code Generation for a Family of Executable Modelling Languages. Software & Systems Modeling 11(2) : 251-272. Springer. 2012.
Amirhossein Vakili and Nancy A. Day, Temporal Logic Model Checking in Alloy. In Proceedings of Abstract State Machines, Alloy, B, VDM, and Z Lecture Notes in Computer Science Volume 7316, pp 150-163, 2012.
Shahram Esmaeilsabzali and Nancy A. Day. Semantic Quality Attributes for Big-Step Modelling Languages. In Proceeding of Fundamental Approaches to Software Engineering (FASE). Lecture Notes in Computer Science Volume 6603, pp 65-80, 2011.
Shahram Esmaeilsabzali, Nancy A. Day, Joanne M. Atlee, and Jianwei Niu, Deconstructing the Semantics of Big-Step Modelling Languages. Requirements Engineering Journal 15(2) : 235-265. Springer. 2010.