meta data for this page
  •  

Differences

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

Link to this comparison view

Next revision		Previous revision
public:dugc:sys-spec-impl [2015/07/08 15:49] – created anupreetpublic:dugc:sys-spec-impl [2020/06/05 02:36] (current) – external edit 127.0.0.1
Line 20: Line 20:
  
 ------------------------------- -------------------------------
-Course Name: [Topics in] System Specification and Implementation +Course Name: [Topics in] System Specification and Implementation\\ 
-Credit Structure: 3 0 0 6+Credit Structure: 3 0 0 6\\
 Prerequisite: Some course in logic or formal methods. Prerequisite: Some course in logic or formal methods.
  
Line 33: Line 33:
 following topics will be covered in different offerings: following topics will be covered in different offerings:
  
-High Level Concepts: +High Level Concepts:\\ 
-Modeling: Abstract models of physical reality +Modeling: Abstract models of physical reality\\ 
-Specification: What is it that we want +Specification: What is it that we want\\ 
-Validation: Are we building/wanting the right thing+Validation: Are we building/wanting the right thing\\
 Verification: Are we implementing what has been specified Verification: Are we implementing what has been specified
  
-Technical Details:+Technical Details:\\
 Specification Languages: Formally specifying what we want our system to Specification Languages: Formally specifying what we want our system to
 do. One of the specification languages from ASM (Abstract State Machine), do. One of the specification languages from ASM (Abstract State Machine),
 VDM (Vienna Development Model), B and Event-B, Alloy, Spec# etc. will be VDM (Vienna Development Model), B and Event-B, Alloy, Spec# etc. will be
-covered.+covered.\\
 Mathematical Objects: Sets, Finite Sequences, Finite Trees, Well founded Mathematical Objects: Sets, Finite Sequences, Finite Trees, Well founded
-Relations.+Relations.\\
 State Machines: Specifying the State, specifying the Operations, State Machines: Specifying the State, specifying the Operations,
-Termination.+Termination.\\
 Proof Obligations: Weakest Precondition Calculus, Invariants, Variants. Proof Obligations: Weakest Precondition Calculus, Invariants, Variants.
 Refinement: Starting with an abstract system and converting it into an Refinement: Starting with an abstract system and converting it into an
Line 53: Line 53:
 refinements. refinements.
  
-Tools:+Tools:\\
 Static Analyzers, Proof Obligation Generators, Proving tools (automatic Static Analyzers, Proof Obligation Generators, Proving tools (automatic
 and interactive), Animators, Model Checkers. The course will focus on and interactive), Animators, Model Checkers. The course will focus on
 using these tools and will not discuss how to build such tools. using these tools and will not discuss how to build such tools.
  
-Texts/References:+Texts/References:\\
 1. Modeling in Event-B: System and Software Engineering, J. R. Abrial, 1. Modeling in Event-B: System and Software Engineering, J. R. Abrial,
-Cambridge, 2010.+Cambridge, 2010.\\
 2. Abstract State Machines: A Method for High Level System Design and 2. Abstract State Machines: A Method for High Level System Design and
-Analysis, Borger and Stark, Springer, 2003.+Analysis, Borger and Stark, Springer, 2003.\\
 3. Modeling Systems: Practical Tools and Techniques in Software 3. Modeling Systems: Practical Tools and Techniques in Software
-Development, Second edition, Fitzgerald and Larsen, Cambridge, 2009.+Development, Second edition, Fitzgerald and Larsen, Cambridge, 2009.\\
 4. The B-book: Assigning Programs to Meanings, J. R. Abrial, Cambridge, 4. The B-book: Assigning Programs to Meanings, J. R. Abrial, Cambridge,
-1996.+1996.\\
 5. Software Abstractions: Logic, Language, and Analysis, Daniel Jackson, 5. Software Abstractions: Logic, Language, and Analysis, Daniel Jackson,
-MIT Press, 2006.+MIT Press, 2006.\\
  
 ------------------------------- -------------------------------