Moses - Quantitative Verification and Timed Automata

Display language

Diese Modulbeschreibung gilt nicht im aktuellen Semester.

Die Modulbeschreibung gilt nur für den Zeitraum WS 2015/16 - WS 2016/17. Die Version für das aktuelle Semester (SoSe 2024) finden Sie hier: Modulbeschreibung des SoSe 2024

Module / Version:
#40664 / #2

Validity:
WS 2015/16 - WS 2016/17

Default display language:
English

Module title:
Quantitative Verification and Timed Automata

Credits:
3

Responsible person:
Kreutzer, Stephan

Grading:
benotet

Type of exam:
Portfolioprüfung

Zugehörigkeit

Faculty:
Fakultät IV

Institute:
Institut für Softwaretechnik und Theoretische Informatik

Area of expertise:
34352200 FG Logik und Semantik

Prüfungsausschuss:
No information

Kontakt

Office:
TEL 7-3

Contact person:
No information

E-mail address:
stephan.kreutzer@tu-berlin.de

Website:
No information

Learning Outcomes

Successful participants are familiar with the principles of verification under time-constraints, in particular the automata theoretical and logical foundations. They are able to read research papers, present the content in written form and in an oral presentation.

Content

Model-checking has become a widely used and successful method for verifying reactive systems - such as hardware systems, controllers or communication protocols - and is increasingly used in the verification of software systems as well. Many current model-checkers focus on deciding whether a process meets a certain requirement such as responsiveness, fairness and similar properties which can either be true or false. However, for many applications it is not only enough to verify that certain error states cannot be reached, but timing constraints become equally important. A typical example is the verification of electronic brake systems: it is not enough to certify that every time the driver uses the break pedal of his car, the car will eventually engage the breaks. Instead we usually want to verify that the break is engaged within a certain time span after the pedal has been pressed. In this reading course we will study the fundamental methods developed for such verification tasks. More specifically, we will study automata models incorporating time constraints and associated timed logics. We will study the various models of time that can be used and the effects this has on complexity and applicability of quantitative model-checking.

Module Components

Pflichtteil:

All Courses are mandatory.

Course Name	Type	Number	Cycle	Language	SWS	VZ
Quantitative Verification and Timed Automata	SEM	0432 L675	WiSe/SoSe	No information	2

Workload and Credit Points

Quantitative Verification and Timed Automata (SEM):

Workload description	Multiplier	Hours	Total
Präsenzzeit	15.0	2.0h	30.0h
Vor-/Nachbereitung	15.0	4.0h	60.0h
			90.0h(~3 LP)

The Workload of the module sums up to 90.0 Hours. Therefore the module contains 3 Credits.

Description of Teaching and Learning Methods

Students participating in the reading course are assigned a research paper each. They study the paper and its context. They present the contents of the paper in a talk given to all participants of the course and in addition prepare their own paper. Depending on students’ preferences the module can be given in English or German. The research papers given to students will be in English.

Requirements for participation and examination

Desirable prerequisites for participation in the courses:

Interest in theoretical computer science. Knowledge of foundations of logic and automata as covered by the modules TheGI2 and TheGI3, for instance, are expected.

Mandatory requirements for the module test application:

This module has no requirements.

Module completion

Grading

graded

Type of exam

Portfolio examination

Type of portfolio examination

No information

Language

English

Test elements

Name	Points/Weight	Categorie	Duration/Extent
Paper	50	No information	No information
Talk	50	No information	No information

Grading scale

No information

Test description (Module completion)

No information

Duration of the Module

The following number of semesters is estimated for taking and completing the module:
1 Semester.

This module may be commenced in the following semesters:
Winter- und Sommersemester.

Maximum Number of Participants

The maximum capacity of students is 14.

Registration Procedures

To enlist for this course, see http://www.las.tu-berlin.de.

Recommended literature
The papers studied in the course will be announced at the beginning of the module.

Assigned Degree Programs

Semester:

Zeige auch ausgelaufene Studiengänge und StuPOs

This module is used in the following Degree Programs (new System):

	Studiengang / StuPO	StuPOs	Verwendungen	Erste Verwendung	Letzte Verwendung
This module is not used in any degree program.

Miscellaneous

No information

Quantitative Verification and Timed Automata

Zugehörigkeit

Kontakt

Learning Outcomes

Content

Module Components

Pflichtteil:

Workload and Credit Points

Quantitative Verification and Timed Automata (SEM):

Description of Teaching and Learning Methods

Requirements for participation and examination

Desirable prerequisites for participation in the courses:

Mandatory requirements for the module test application:

Module completion

Grading

Type of exam

Type of portfolio examination

Language

Test elements

Grading scale

Test description (Module completion)

Duration of the Module

Maximum Number of Participants

Registration Procedures

Recommended reading, Lecture notes

Lecture notes

Electronical lecture notes

Literature

Assigned Degree Programs

This module is used in the following Degree Programs (new System):

Miscellaneous