Course Outline

The schedule and required readings (that you must do on your now), scheduled Labs and Quizzes are provided below.

You must be in the Lab during the scheduled Lab hour. There will be a weekly Quiz during the scheduled Lab hour that is graded.

Quiz Instructions

• Assignment is due Thursday November 10th, 12 noon.
• Project is due Wednesday November 30th, 12 noon.
• Exam: Tue, 13 Dec 2016 2pm-5pm

Each week you are required to study readings, on you own time, from:

• the WIFT-95 Tutorial Introduction to PVS (WIFT-PVS Tutorial). Try out all the examples in the PVS theorem prover.
• the required text: Requirements Engineering Management Handbook (REMH). Note that there are examples of how to write requirements documents in Appendix A, B,, C and D of this handbook. This allows you to see how the readings can be applied in practice.

The labs, quizzes, assignment, project and exam will be based on your knowledge of the required reading/study material, the Labs, as well as material presented in class.

At the beginning of each week (midnight Sunday), the Lab for that week will become available. A graded Quiz will take place every Thursday during the scheduled Lab. The Quiz will be on the Lab of the previous week (e.g. Quiz1 will be on Lab0) and on the readings and course work of the previous week.

At the beginning of each week you must start doing the Lab work for that week, and submit it by the Friday morning of that week. During the scheduled Lab you may ask questions on the Lab. While each Quiz is graded, the Labs are not given a grade. <hi cyan> However you must submit the completed Lab on time to obtain a grade for the Quiz of that week.</hi> If you miss a Quiz, you will not receive a grade for that Quiz.

DB = Victor Phillip Dahdela Building

• Eliciting customer needs and goals and identifying the stakeholders.
• The use of UML diagrams such as use case, sequence, class and statechart diagrams to help with the elicitation.
• Developing the system overview, system boundary and context diagram.
• Identifying the monitored variables and events and the controlled variables, their types ranges, precision and units.
• Identifying the environmental assumptions and constraints.
• Understanding the Parnas 4-variables model for writing requirements.
• Monitored Variables, Controlled Variables, Timing resolution and Response Allowance
• Developing the functional specification using tabular expressions (mathematical function tables)
• The use of specification and theorem proving tools (PVS) to describe the function tables and using the PVS tool to verify the completeness, disjointness and well- definedness of the functional requirements.
• PVS Specification of predicates using basic types, tuples, records, datatypes, functions, relations, sets, bags, etc. Reasoning about predicates in these types.
• How to use function tables to specify safety-critical real-time systems and cyber-physical systems and understanding, Timing Resolution and Response Allowances.
• Using function tables to specify business systems via monitored events and abstract states/controlled variables.
• Validation of use cases against the functional specifications and validation of the safety requirements.
• Describing non-functional and performance requirements.
• Deriving acceptance tests from the use cases and function tables.

Notes: There are some slides available on the course web site but much of the work is done on the blackboard. Instruction in the use of PVS for specification and validation is done mainly via the Labs and the associated Quizzes.