There is a <hi> required scheduled Lab on Wednesday 4 September in LAS1006, 5.30pm to 6.30pm </hi>. This is Lab0 and the material is available on the SVN once you logon. There will be Labtest on this material Wednesday 11 September.

Please login at the bottom of this page before proceeding.

← Please subscribe to and read from the forum regularly for course updates.

See the Resources Tab for information on the required Textbook, the TLA+ and PVS tools, private Educational Github repositories and Predicate Logic and Set Theory.

Lectures are on Tuesdays and Thursdays at 4pm in LAS105.

• Lectures: Tuesdays & Thursdays 4pm-5.30pm
  • Tuesday lectures are to be held in: LSB 105.
  • Thursday lectures are to be held in: LSB 105.
• Labs: There is a formal Lab every Wednesday in LAS1006, from 5.30pm to 6.30pm. Labs start right away on the first day of class (with Lab0). Login to this Wiki with your Prism account, and go to the SVN tab (on the left).
• Labtests: There is a graded Labtest (using multiple choice) each week during the Lab, starting on WEdnesday 13 September. The Labtest will be on all the work up to (but not including that day).

Self-paced Learning, PVS and Text Books

Software requirement engineers are experts at eliciting the needs of their customers, translating customer needs into a precise requirements documents (that describes what – not how – customer needs shall be satisfied), and providing systematic evidence-based methods to validate the requirements and verify that the final software product satisfies the requirements. Precise software requirements documents are especially needed in safety critical cyber-physical systems (e.g. nuclear reactors, medical devices and transportation systems) and mission critical business systems (e.g. banking systems, health provision and cloud systems). At the end of the course, students will be able to

• Elicit customer requirements by analyzing customer goals and needs
• Write precise requirements documents. To do this students will be able to:
  • Develop the system overview, identify the system boundary and draw a context diagram
  • Identify the monitored variables and events and controlled variables
  • Identify the environmental assumptions and constraints
  • Describe the functional requirements using tabular expressions (function tables) that specify the mathematical relation between the monitored variables and events and the controlled variables
  • Describe the non-functional requirements
  • Prove that the functional requirements are complete, disjoint and well-defined
  • Provide a complete set of use cases and corresponding acceptance tests so that each requirement is a verifiable contract of customer needs
  • Validate the functional requirements by proving that they preserve safety properties (derived from such methods as hazards analysis) and prove that the use cases satisfy the function tables

A work-intensive project will allow students to apply their knowledge to a small but non-trivial example.

Lassonde Link