Winter Term 2012/2013
Softwarepraktikum (Nicht für B.Sc. Informatik und B. Sc. ESE)
In diesem Praktikum soll ein Softwareentwicklungsprozess, beginnend bei Anforderungserhebung über Entwurfsphase bis hin zur Implementierung, die Organisation der Arbeit innerhalb einer Gruppe und der Umgang mit komplexen Systemen erlernt werden. Die Teilnehmer werden von den Betreuern in Gruppen eingeteilt und müssen eine bestimmte Aufgabenstellung realisieren. Hierzu müssen sie sich selbst organisieren, die Anforderungen definieren, Arbeit geschickt auf Gruppenmitglieder verteilen und neue Technologien selbstständig erlernen.
Design and Analysis of Cyber Physical Systems (Seminar)
The development of cyber physical systems (CPS) is considered to be the next computing revolution. Cyber physical systems are networked computational systems that interact with the physical world. Examples of such systems are autonomous cars, robots, intelligent energy-efficient buildings, embedded medical devices, etc. The systems like that require tight connection between discrete and continuous behavior. The design of CPS presents many challenges because of their complexity, safety requirements and real-time nature. Thus collaboration among people from different disciplines and between academics and industry is required to make progress in the area of CPS.
Cyber-Physical Systems I - Model Checking (Lecture)
Model checking is a technique for the automatic verification of hardware or software systems. Given such a system and a specification of its intended behaviour, a model checker finds out whether the system satisfies the specification. Model checking has made enormous progress since its invention in the 1980s; today it is possible to verify entire CPU designs, and so all major microprocessor companies use and develop tools for this purpose. Software verification is more challenging than hardware verification and an active research topic (pursued at the chair for Software Engineering, for instance!). Recent years have seen interesting progress in this area as well. The industry has already started using these techniques to check, e.g., safety-critical embedded systems, and software libraries; yet, many research challenges, both theoretical and practical, lie ahead of us.
Formal Methods for Java (Lecture)
Recently, formal methods have been successfully used to specify and verify large software system. A current example is the Verisoft project, whose goal is to create a fully verified processor, operating system and compiler. In this lecture we will investigate the exising methods for the language Java. The language Java was chosen because it is a mature language, with a semi-formal definition of its semantics (The Java Language Specification). However, to use mathematical reasoning, we need a precise definition of the semantics. Therefore, we will sketch the definition of an operational semantics for Java. Furthermore, we will investigate different formal methods for Java. The starting point will be the language extension JML that allows Design by Contract. This allows to add pre- and postconditions to methods and invariants to classes and loops. These assertions can be checked during runtime and this is the purpose of the JML runtime assertion checker (jmlrac). On the other hand, there are static methods, e.g., ESC/Java and Jahob, that automatically provide mathematical proofs that the Java code ensures the post-condition for each possible pre-condition. If these proofs cannot be find automatically, one can also use theorem provers that assists finding a proof manually. In this lecture, we will present the different approaches for verification of Java code. In the exercise you can investigate different tools on small practical examples.
Software Design, Modelling, and Analysis in UML (Lecture)
The model-driven approach to software and systems development proposes to address quality and complexity issues in the development process. The usage of modelling languages not only for documentation, but, e.g., for automated analysis, test generation, and code generation is gaining momentum in particular in the context of (safety) critical software development. The necessary pre-requisites are a semantically founded modelling language and methods and tools for analysis. We will take the Unified Modelling Language (UML) as an example and demonstrate how to equip a relevant sublanguage (sometimes referred to as executable core) with a precise meaning in line with the official standard documents. To complement these discussions, we provide access to a contemporary UML modelling tool and use it for some of the exercises.
Software Testing (Seminar)
This seminar covers important achievements in the area of Automated Black-box and White-box Testing.
Testverfahren für Softwaretechnik (Proseminar)
Grundlagen des Softwaretestens, Testen im Softwarelebenszyklus, Statischer Test, Dynamischer Test, Testmanagement, Testwerkzeuge.