Nancy
Day
last updated November 27, 1998
| |
Nancy
Day
last updated November 27, 1998
|
| formalWARE
project
formalWARE
formalWARE
|
Nancy Day is currently a
postdoctoral research associate at the
Oregon Graduate Institute.
She completed her Ph.D.
in the UBC Department of Computer Science in October 1998.
Her Ph.D. supervisor was Dr. Jeff Joyce and
her thesis supervisory committee included
Dr. Paul Gilmore (UBC), Dr. Mark Greenstreet (UBC), Dr. Alan Hu (UBC),
Dr. Nancy Leveson (University of Washington and UBC) and Dr. Gail Murphy
(UBC). Day received her M.Sc. in Computer Science at UBC in 1993 and her
B.Sc. from the University of Western Ontario in 1991.
She was also an instructor for the
Certificate
in Software Engineering offered by Continuing Studies at UBC.
Her research investigates the use of specification notations that have been accepted by industry such as statecharts and tables. Specifically her work focuses on techniques for systematically analysing specifications. Analysis methods include simulation, prototyping, checking for completeness and consistency, and model checking. Model checking allows the user to query the specification to see if it has certain desired properties. To test her ideas, Day is building a framework in which multiple notations can be used to describe different parts of a system, but integrated to create an overall model of the system's behaviour for analysis. She has found that using an explicit formal definition of the meaning of the notations makes it possible to do this integration. This formal definition can then be used to drive the analysis. It also allows the existing structure of the specification to be used to reduce the size of the search space that must be explored in analysis. These tools have been used in prototype applications by engineers at Hughes. Day's thesis proposal was accepted for
presentation at the Doctoral Consortium of the International Conference
on Software Engineering (ICSE) in May, 1997. Also, in collaboration with
Hughes personnel, she has prepared a full report on the formal specification
and analysis of a public domain standard for separation minima between
aircraft in the North Atlantic Region.
formalWARE Publications:J.H. Andrews, N. A. Day and J. J. Joyce, Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network. Presented at FORTE/PSTV'97 (1997 IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocal Specification, Testing, and Verification), Osaka, Japan, November 18-21, 1997.Nancy Day, Jeff Joyce and Gerry Pelletier. Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region: Complete Specifications and Analysis Results. Technical report 97-12, Department of Computer Science, UBC, October, 1997. Nancy Day, Jeff Joyce and Gerry Pelletier. Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region. Presented at the 4th NASA Langley Formal Methods Workshop, Hampton Virgina, USA, September 10-12 1997. Jeffrey J. Joyce and Nancy Day and Michael
R. Donat. S: A Machine Readable Specification
Notation based on Higher Order Logic. In Lecture Notes in Computer
Science 859, Higher Order Logic Theorem Proving and Its Applications, 7th
International Workshop, (T.F. Melham, J. Camilleri Eds.), Springer-Verlag,
1994.
formalWARE Presentations:November 10, 1997 "Specification and Tool-based Analysis of an Aircraft Separation Minima" at Hughes Aircraft of Canada, Richmond, BC.Abstract | Presentation Slides October 8, 1997
"Formal Validation of System Specifications" at formalWARE's Open House,
Cecil Green House, UBC.
formalWARE Examples:Aeronautical Telecommunications Network(ATN)Separation
Minima for Aircraft in the North Atlantic Region
Further Information:For more information on Day's research, see her home page at http://www.cse.ogi.edu/~nday/. She can be contacted by email at day@cse.ogi.edu. |
