Seminar in Computer Science: Formal Verification

Objectives

In this seminar, the participants learn how to write a scientific paper and how to prepare and give a scientific talk. Therefore, recent literature of active research fields is inquired.

Slides of the preparatory lecture

Workflow

Each participant (groups consisting of 2 students are also possible) selects one of the proposed topics (see below), performs a small literature study on this topic, and outlines the most important results in a written survey, which are finally presented to the other participants at the end of the term. The concrete workflow of this seminar is as follows.

Note: If you want to write a bachelor's thesis in the context of this seminar, please inform the advisor when you select your topic.

1. Topic selection. Please select one of the proposed topics and send an email to the advisor. In case of questions also contact the advisor. If you prefer to register personally, please keep the appointment for personal registration as announced below.

2. Presentation of the first concept. During this meeting, you present the overall structure of your paper, i.e., the table of content, together with a short outline of each section (some keywords are sufficient) and (per person) at least two other related references which will be used in your paper to the advisor. Furthermore, open questions shall be answered and the outline of the work shall be either confirmed or clarified. The appointment for this meeting is arranged individually. Please submit your concept within the submission deadline for the concept as stated below.

3. Submission of the paper. The paper (formatted in Springer LNCS; llncs2e.zip contains the files for the Springer LNCS style) has to be submitted via email. You will receive feedback (appointment is set up individually via email) which you have to incorporate in the final version of your paper. We encourage you to use LaTex. The structure of your paper shall be similar to the structure proposed in the article How to Write an Informatics Paper.

4. Submission of the slides. The slides which you will present in your talk have to be submitted via email. You will receive feedback via email which you have to incorporate in the final version of your slides. Infos on how to prepare and give a good talk may be found in the Presentation Primer.

5. Oral presentation. Finally, your work is presented to the other participants of the seminar. The talk should have a length of max. 20 minutes.

Grading

The grading is based on the quality of the submitted material and the given talk. Active participation during the meetings is expected.

The default language of the seminar is English. Papers and talks in English are particularly appreciated, but not required.

Contact

In case of questions or problems please contact Martina Seidl (Martina.Seidl@jku.at).

Deadlines and Appointments (mandatory)

Please note that all appointments must be kept and all deadlines must be met in time for obtaining positive grade.

The advisor may be contacted any time if problems occur.

Topics

In the following, a list of possible topics with a short the description is provided. If you are interested in one of the topics, please contact the advisor for additional information and for related literature.

• The semantics of semantics in the context of UML.

  A (modeling) language is specified in terms of syntax and semantics defining the notation and meaning of the language's elements. In the context of modeling languages this specification is usually provided by a metamodel. In this work, the term “semantics” shall be elaborated explaining its role in the definition of modeling languages with special focus on UML.

• Semantics for UML Diagrams.

  The UML standard (the UML Superstructure) is almost entirely formulated in natural language and does not provide a formal semantic definition for UML. Consequently, a lot of work has been spent in providing such semantics to UML using various formalisms. In this work, selected formalisms for one of the following diagrams shall be elaborated.

  • Class Diagrams.

  • State Machines.

  • Sequence Diagrams.

  • Activity Diagrams.

• Lack of clarity in the semantics of UML.

  The language of UML is defined in the UML Superstructure. Over the years, several open questions on UML, which are not answered by the Superstructure, have been identified. A written report on this topic shall give an overview of such unclarities.

• Formalization of model evolution.

  Like any software artifact, models are subject to evolution, i.e., models are changed multiple times during their lifetime for optimizations, corrections, and extensions. This is of particular importance in the context of model-driven engineering (MDE) where executable programs are generated out of models. In order to develop methods for managing and controlling evolution in MDE processes, profound research on the basic concepts of evolution is indispensable. Currently, many different efforts in managing evolution have been made spanning a very heterogeneous research landscape. In this work, techniques supporting model evolution shall be reviewed.

• Checking UML models.

  As in traditional programs, also in models errors are not eligible. Unfortunately, the number of possibilities to flaw a model is huge: non-conformance to the metamodel, inconsistencies, unintended execution behavior are just a few severe problems having negative impact on the quality of a model. Consequently, several techniques have been proposed to ensure certain properties. In this work, selected techniques shall be reviewed which support ensuring certain properties of a model.

• Correctness of refactorings.

  Refactorings are operations applied on models or programs for improving their internal structure with respect to for example readability and reusability without changing their externally visible behavior. Put in other words, the refactored program/model shows the same behavior as the original program/model. In this work, techniques shall be reviewed and presented which ensure that the application of refactoring operations does not change the behavior of a program/model.