meta data for this page
Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
public:dugc:sys-spec-impl [2015/07/08 15:49] – created anupreet | public: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: | Prerequisite: | ||
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: | + | Specification: |
- | Validation: Are we building/ | + | Validation: Are we building/ |
Verification: | Verification: | ||
- | 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: | Proof Obligations: | ||
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), | and interactive), | ||
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/ | + | Texts/ |
1. Modeling in Event-B: System and Software Engineering, | 1. Modeling in Event-B: System and Software Engineering, | ||
- | 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, | + | Development, |
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: | 5. Software Abstractions: | ||
- | MIT Press, 2006. | + | MIT Press, 2006.\\ |
------------------------------- | ------------------------------- |