Differences

This shows you the differences between two versions of the page.

--- start [2014/12/29 18:24] – jonathan
+++ start [2015/05/07 21:29] (current) – jonathan
@@ Line 15: / Line 15: @@
   *See bottom** ↓** of this page for login with your Prism password. Slides are available from the SVN repository (see link in the sidebar, once you have logged on).
-  * The Labs to be done each week are available at [[[[protected:project:labs|Labs]].
+  * The Labs to be done each week are available at [[[[protected:labs|Labs]]. Lab0 must be completed in the first week of classes.
   *Read the course outline regularly.  It is important to read all the required readings (not all of which are discussed in class). It is important to do the suggested exercises.
@@ Line 21: / Line 21: @@
   * In the SVN → Docs, you will find the Rodin 2.8 Manual. Please familiarize yourselves with all the material in the manual, during the first week of classes.
+  * Suggested Text: Jean-Raymond Abrial, //Modeling in Event-B: System and
+Software Engineering//, Cambridge 2010. Available in Steacie. See SVN for notes. [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:eventb:start|Event-B Information]]
 ===== Calendar Description  =====
@@ Line 32: / Line 34: @@
 After successful completion of the course, students are expected to be able to:
-  *Understand the nature of formal methods and evaluate their suitability.
-  *Understand user requirements documents and the distinction between environmental constraints as opposed to functional and safety descriptions.
+  *Document requirements organizing them into appropriate categories such as environmental constraints versus functional properties (safety and progress).
   *Construct high level, abstract mathematical models of a system (consisting of both the system and its environment) amenable to formal reasoning.
-  *Use set theory and predicate logic to express functional and safety properties from the requirements as events, guards, system variants and invariants of a state-event model.
+  *Apply set theory and predicate logic to express functional and safety properties from the requirements as events, guards, system variants and invariants of a state-event model.
-  *Understand how to use models to reason about and predict their safety and liveness properties.
+  *Use models to reason about and predict their safety and progress properties.
-  *Construct a sequence of refinements from abstract high-level specifications to implemented code and the proof obligations for showing that a concrete system refines the abstract system.
+  *Plan and construct a sequence of refinements from abstract high-level specifications to implemented code.
-  *Know the theory underlying state-event systems, refinements and their proof obligations.
+  *Prove that a concrete system refines an abstract model.
   *Apply the method to a variety of systems such as sequential, concurrent and embedded systems.
   *Use practical tools for constructing and reasoning about the models.
-  *Compare the theory with classical Hoare Logic and the Dijkstra weakest precondition calculus .
+  *Use Hoare Logic and Dijkstra weakest precondition calculus to derive correct designs
 Chapters 1, 2, 3, 4, 5, 9 and 15 from the text [[http://www.event-b.org/abook.html|Modeling in Event-B: System and Software Engineering]], Jean-Raymond Abrial (Cambridge) makes this a possible textbook for the course.