622.050 (09W) Specification and Verification

Wintersemester 2009/10

Registration deadline has expired.

First course session
06.10.2009 08:00 - 10:00 HS 1 On Campus
... no further dates known

Overview

Lecturer
Course title german Spezifikation und Verifikation
Type Lecture
Hours per Week 2.0
ECTS credits 2.0
Registrations 57
Organisational unit
Language of instruction English
Course begins on 06.10.2009

Time and place

List of events is loading...

Course Information

Teaching methodology including the use of eLearning tools

Classroom instruction with conventional lecture, supported by associated lab course

Distance learning info

---

Course content

An introduction to the formal specification of software systems, using the specification language Z

Topics

  • Introduction
  • Sets, Constants, and State-Spaces
  • Predicates, Schemata, Schema-Calculus
  • Relations, Functions, Sequences, Bags
  • Free Types, Schemata as Types
  • Application (Pipe & Filter Architecture-Spec)
  • Theorem Prover
  • Rigourous Proofs, Sequent -Calculus (Propositional Logic)
  • Predicate Logic
  • Immanent Reasoning
  • Reification
  • Floyd-Hoare Logic
  • Predicate Transformers

Teaching objective

Acquiring the capability of reading and writing formal specifications.

Prior knowledge expected

Basic knowledge in software engineering and discrete mathematics (set theory, propositional and predicate logic)

Other materials

Course notes, to be found in the associated MOODLE-folder

Literature

Antoni Diller Z: An Introduction to Formal Methods, 2nd ed. John Wiley & Sons Ltd., Chichester, 1994

Teaching methodology including the use of eLearning tools

Classroom instruction with conventional lecture, supported by associated lab course

Distance learning info

---

Course content

An introduction to the formal specification of software systems, using the specification language Z

Topics

  • Introduction
  • Sets, Constants, and State-Spaces
  • Predicates, Schemata, Schema-Calculus
  • Relations, Functions, Sequences, Bags
  • Free Types, Schemata as Types
  • Application (Pipe & Filter Architecture-Spec)
  • Theorem Prover
  • Rigourous Proofs, Sequent -Calculus (Propositional Logic)
  • Predicate Logic
  • Immanent Reasoning
  • Reification
  • Floyd-Hoare Logic
  • Predicate Transformers

Teaching objective

Acquiring the capability of reading and writing formal specifications.

Prior knowledge expected

Basic knowledge in software engineering and discrete mathematics (set theory, propositional and predicate logic)

Other materials

Course notes, to be found in the associated MOODLE-folder

Literature

Antoni Diller Z: An Introduction to Formal Methods, 2nd ed. John Wiley & Sons Ltd., Chichester, 1994

Examination information

Im Fall von online durchgeführten Prüfungen sind die Standards zu beachten, die die technischen Geräte der Studierenden erfüllen müssen, um an diesen Prüfungen teilnehmen zu können.

Examination topic(s)

Material covered in the course as well as chapters 1 - 15 of the textbook.

Assessment criteria / Standards of assessment for examinations

written exam

Examination topic(s)

Material covered in the course as well as chapters 1 - 15 of the textbook.

Assessment criteria / Standards of assessment for examinations

written exam

Grading scheme

Grade / Grade grading scheme

Position in the curriculum

  • Teacher training programme Computer Sciences and Computer Sciences Management (Secondary School Teacher Accreditation) (SKZ: 884, Version: 04W.7)
    • Stage two
      • Subject: Angewandte Informatik (LI 2.3) (Compulsory subject)
        • Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
          • 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
  • Bachelorstudium Informatik (SKZ: 521, Version: 09W.3)
    • Subject: Spezifikation und Verifikation (Compulsory elective)
      • Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
        • 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
  • Bachelor's degree programme Informatics (SKZ: 521, Version: 03W.1)
    • Subject: Spezifikation und Verifikation (Compulsory subject)
      • Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
        • 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
  • Masterstudium Informatik (SKZ: 921, Version: 09W.1)
    • Subject: Spezifikation und Verifikation (Compulsory subject)
      • Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
        • 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
  • Master's degree programme Informatics (SKZ: 921, Version: 03W.1)
    • Subject: Spezifikation und Verifikation (Compulsory subject)
      • Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
        • 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
  • Diploma programme Informatics (SKZ: 880, Version: 02W)
    • Stage two
      • Subject: Angewandte Informatik inkl. Vertiefungsfach (Compulsory subject)
        • Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
          • 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
  • Diploma programme Informatics (SKZ: 880, Version: 02W)
    • Stage three
      • Subject: Angewandte Informatik und Vertiefungsfach (Compulsory subject)
        • Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
          • 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)

Equivalent courses for counting the examination attempts

Wintersemester 2023/24
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2022/23
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2021/22
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2020/21
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2019/20
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2018/19
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2017/18
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2016/17
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2015/16
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2014/15
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2013/14
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2012/13
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2011/12
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
Wintersemester 2010/11
  • 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)