|
Courses and Workshops
|
| Title: | Temporal logic for systems validation |
| Lecturer(s): | Holger Schlingloff (Humboldt University / Fraunhofer FIRST) |
| Type: | Introductory Course |
| Section: | Logic and Computation |
| Week: | Second | | Time: | 9.00-10.30 (Slot 1) |
| Webpage: | http://www.informatik.hu-berlin.de/~hs/index_e.html
|
| Reader: | Course will not have a reader | | Room: | A2 |
Description In this course we discuss the use of temporal logics in the verification
and validation of computational systems. In particular, we focus on new
developments in model checking, automated test case generation and
specification-based debugging of software. We will introduce not only
classical linear and branching time logics, but also monadic second
order calculi, hybrid logics, and real-time logics. In the course we
will cover foundational issues (semantics, decidability and complexity)
of the logics involved, demonstrate how the logics can be used in the
specification of computational systems, and explain the algorithms which
are used to analyse software with them. Throughout the course, we will
give examples from industrial projects where the techniques have been
applied for actual systems in aerospace, railway control, and webservices.
|
© 2003, 2004 LORIA, Carlos Areces. |
2003-11-20
| |
