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
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
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.