Sofa Seminar (Spring 2013)

 
Overview
The Sofa Seminar is a more or less formal seminar of the Software Engineering Section of DTU Informatics, where we share ideas, visions, and research results. There is a fixed slot for the Sofa Seminar every Tuesday at 1400 in the breakfast room on the first floor in building 322 (322.121).

 

If you would like to have a slot for your ideas, please contact Ekkart Kindler (). You can see the available slots in the schedule below.

 

You can find the programme of (some) earlier Sofa Seminars in this archive.

 

Schedule
  5. February 2013, 1400, 322.121: none

 

12. February 2013, 1400, 322.121: Ekkart Kindler: The Event Coordination Notation: Concepts, Tool, Vision

 

The Event Coordination Notation (ECNO) is a notation for modelling the behaviour of a software system on top of some object-oriented data model. ECNO has two main objectives: On the one hand, ECNO should allow modelling the behaviour of a system on the domain level; on the other hand, it should be possible to completely generate code from ECNO and the underlying object-oriented domain models.

 

Today, there are several approaches that would allow to do this. But, most of them would require that the data models and the behaviour models are using the same technology and the code is generated together. By contrast, ECNO can be used for modelling the behaviour on top of any object-oriented model -- or even on top of manually written object-oriented code. This way, it is easy to integrate ECNO models with other technologies, to use ECNO on top of code generated by other technologies or with code that was written manually.

 

In this talk, I will give an overview of the motivation of the ECNO, its main concepts, the current tool support, as well as on the future steps.

 

19. February 2013, 1400, 322.121: SE Section:
Reserved for the research brainstorming of the Software Engineering Section on this afternoon 1400–1600.

 

26. February 2013, 1400, 322.121: Joseph Kiniry: Validating Semantics

 

In our group, we do applied formal methods. This means that we develop new mathematical theories to solve unsolved problems, primarily in the area of software verification, and then build tools that show off these theories.

 

In the vast majority of cases, we mechanically formalize our theories in first-order or higher-order logics using automated and interactive reasoning frameworks. Performing this mechanization can take an enormous amount of time and energy. Moreover, the mechanization of a theory tells us little about if the theory can be realized in practice---declaratively mechanizing a theory does not guarantee that an algorithm exists, can be found, or is efficient to reason with or about theory. Meaning, even if we mechanize, we cannot guarantee that we can build a tool to show off the theory.

 

Sometimes we do not mechanically formalize a theory. This is either due to a lack of time or because a non-mathematician defined the new theory. In either case, what hope do we have in getting the theory right?

 

Note that, these latter situations are typical in the world of software tools. Most tools, either explicitly or implicitly, are based upon some underlying theories, whether their authors know it or not. How do we have any confidence that their tools work correctly? Or complementarily, how do we know that the theory which they are based upon is correct?

 

  5. March 2013, 1400, 322.121: Alexander Knapp (Augsburg University):
On the Correctness of the SIMT Execution Model of GPUs (joint work with Axel Habermaier and Gidon Ernst)

 

GPUs are becoming a primary resource of computing power. They use a single instruction, multiple threads (SIMT) execution model that executes batches of threads in lockstep. If the control flow of threads within the same batch diverges, the different execution paths are scheduled sequentially; once the control flows reconverge, all threads are executed in lockstep again. Several thread batching mechanisms have been proposed, albeit without establishing their semantic validity or their scheduling properties. To increase the level of confidence in the correctness of GPU-accelerated programs, we formalize the SIMT execution model for a stack-based reconvergence mechanism in an operational semantics and prove its correctness by constructing a simulation between the SIMT semantics and a standard interleaved multi-thread semantics. We briefly discuss an implementation of the semantics in the K framework and a formalization of the correctness proof in the theorem prover KIV. We also demonstrate that the SIMT execution model produces unfair schedules in some cases.

 

12. March 2013, 1400, 322.121: NN
available

 

19. March 2013, 1400, 322.121: NN
available

 

26. March 2013
Easter holidays

 

  2. April 2013, 1400, ??: NN
available

 

  9. April 2013, 1400, ??: NN
available

 

16. April 2013, 1400, ??: NN
available

 

23. April 2013, 1400, ??: NN
available

 

30. April 2013, 1400, 322.121: Vlad Acretoaie:
Delivering the Next Generation of Model Transformation Languages and Tools

 

Model transformations lie at the core of Model Driven Engineering (MDE), and as such have received significant attention. Several relatively mature model transformation languages are available today, including the Query/View/Transformations (QVT) standard, the Atlas Transformation Language (ATL), and the Epsilon Transformation Language (ETL), to name just a few. Most are textual languages, based to a certain extent on OCL, and focused on maximizing expressiveness rather than usability. Consequently, users of these languages must possess a strong technical background and command of OCL. However, models may also be created and manipulated by domain experts, while research shows that OCL leaves plenty to be desired in terms of usability.

 

Model Transformation By-Example (MTBE) aims to make the specification of model transformations accessible to non-technical modelers, such as domain experts. The core principle of MTBE is that a transformation can be specified by demonstrating its intended effects on a series of small sample models, without requiring a dedicated transformation language – be it textual or visual. This significantly reduces the learning curve and increases the usability of model transformations facilities adopting this paradigm.

 

We intend to use the Visual Model Query Language (VMQL) as a starting point for creating a new MTBE language, tentatively called the Visual Model Transformation Language (VMTL). It will be applicable across modeling languages, and support features such as tracing and debugging. Our initial analysis also suggests that VMTL may easily surpass the expressiveness of existing MTBE approaches.

 

We will present the current state of our research, as well as a roadmap for the work to be carried out in the coming years.

 

  7. May 2013, 1400, ??: NN
available

 

14. May 2013, 1400, ??: NN
available

 

21. May 2013, 1400, ??: NN
available

 

28. May 2013, 1400, 322.121: Ekkart Kindler
Teaching UML: What can we learn from language teachers and linguists?

 

When discussing with people teaching software engineering and, in particular, UML, we often realize that students do not know or are not able to apply some concepts that we think we had taught them. There might be different reasons for that. In this Sofa Seminar, I will take the extreme position which puts the blame on us, the teachers: maybe, we are not teaching UML in the right way, or at least, there might be better ways of teaching it.

 

As the "L" in the acronym UML indicates, UML is a "language", and, after teaching software engineering for many years now, I got the feeling that learning UML is very much like learning a language. Linguists have studied for a long time how language acquisition works (or does not work), which principles govern this process, and what that means for teaching languages (unfortunately, not all of that knowledge made it into language curricula at schools). In this Sofa Seminar, I will try to informally discuss some of the principles of language teaching and how they might relate to teaching UML.

 

There are no formal conclusions yet, but I will try to convince ourselves that taking up the principles of language teaching when teaching UML might be a way to improve our teaching of UML. I am looking forward to a lively discussion.

 

  4. June 2013, 1400, 322.121: Maciej Kucharek (MSc student of Harald's)
Re-Engineering RED (RED-4)

 

The Requirements Editor (RED) is a tool to support a great number of RE techniques. It has been designed primarily as a teaching device, supporting course 03364 "Requirements Engineering". RED is based on Eclipse-3, and has been created since 2011 by 3 MSc-theses. Due to this development history, RED has suffered from architectural decay, making it difficult to maintain and enhance. In fact, when trying to add features to support version control and group collaboration, we realised that a technological consolidation would be needed before more extensions could be made.

 

Thus, Maciej's original project was aborted, and re-focused to adress the issue of re-engineering RED to improve maintainability and extensibility. The overall goal is to transform the overall tool development project into an open source project that allows third parties to contribute. In more detail, we will need to establish a suitable development environment based on a repository, make-process, test automation, issue tracking, maintenance guide, and so on. Also, we want to port RED to the latest Eclipse release to be able to benefit from future platform developments. Finally, we will refactor the existing code base to achieve a more reliable and extensible code structure.

 

We plan to document our achievements by code quality metrics, and a case study.

 

11. June 2013, 1400, ??: NN
available

 

18. June 2013, 1400, 322.121: Jesper Jespen (MSc student of Ekkart's)
Realizing a Workflow Engine with the Event Coordination Notation — A Case-study

 

The Event Coordination Notation (ECNO) allows us to model behaviour of applications on top of UML class diagrams. ECNO can then generate complete executable code based on the structural and the behavioural models. ECNO has already been proven to work in small example projects -- such as a simple vending machine. This project aims at creating an “almost realistic” application with ECNO -- partly for the purpose of identifying the limitations in ECNO, and partly for gaining more experience on how to properly use ECNO. This experience should then help in developing a methodology for ECNO. In this project, ECNO is used for realizing an aspect oriented workflow engine.

 

This talk introduces ECNO, discusses the aspects of business process modelling and then presents the current state of a workflow engine implemented on top of an ECNO engine. The focus is on the structural meta-models and the behavioural models. The presentation will also include a live demonstration of the generated software as of now.

 

25. June 2013, 1400, ??: NN
available

 

 

Ekkart Kindler (), September 14, 2012 (latest update June 11, 2013)