Differences

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

--- start [2015/03/04 02:51] – jonathan
+++ start [2015/05/07 21:29] (current) – jonathan
@@ Line 34: / 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.