Read the Forum and Course Outline for more information.
TrainGate.pdf (see same folder where slides are kept) is a sample Requirements Document to help you with Phase1. The Document was prepared using Latex (see the readme file; latex source provided), but you may use any document preparation system such as MS Office or Open Office, provided the result has a professional look as in the example. In the Papers folder (see same folder where slides are kept) there are two papers by well-known companies that do Requirements Engineering with advice on how to write a Requirements Document. This is not required reading but you might find it useful. There is also a paper on the use of formal methods (mathematically precise specification methods) which is applicable to our use of Spin for specifications.