| Date | Speaker | Affiliation | Title |
| 21.04.2009 | Martin Wirsing | Ludwig-Maximilians-Universitaet Muenchen | What is a Multi-Modeling Language? |
| Abstract: In large software projects often multiple modeling languages are used in order to cover the different domains and views of the application and the language skills of the developers appropriately. Such "multi-modeling" raises many methodological and semantical questions, ranging from semantic consistency of the models written in different sublanguages to the correctness of model transformations between the sublanguages. We provide a first formal basis for answering such questions by proposing semantically well-founded notions of a multimodeling language and of semantic correctness for model transformations. In our approach, a multi-modeling language consists of a set of sublanguages and correct model transformations between some of the sublanguages. The abstract syntax of the sublanguages is given by MOF meta-models. The semantics of a multi-modeling language is given by associating an institution, i.e., an appropriate logic, to each of its sublanguages. The correctness of model transformations is defined by semantic connections between the institutions. | |||
| 17.03.2009 | Wolfgang Schreiner | Johannes Kepler University | Computer-Assisted Proving for the Analysis of Systems and Specifications |
| Abstract: Nowadays the formal methods landscape is dominated by model checking, an approach to the verification of programs/systems that is fully automatic but limited in its scope, in particular with respect to verifiable properties. In this talk, we discuss the alternative and more general direction of computer-assisted interactive proving which in the last decade (due to the development of automatic "Satisfiability Modulo Theories" solvers as supporting components) has made tremendous progress; consequently practical formal reasoning on more general system models and system properties has become viable. Furthermore, while not fully automatic and depending on human assistance, this approach has the potential of increasing a programmer's understanding (why is a system correct or what are the fundamental reasons of its failure) much more than the plain yes/no answers and counterexample executions produced by fully automatic model checkers. As an example of this direction, we present the "RISC ProofNavigator", an interactive proving assistant developed for education in reasoning about programs and specifications. Finally, we argue why modern computer science curricula should teach the use of proving assistants for formal specification and verification as an integral part of developing correct software. | |||
| 16.12.2008 | Daniel L. Moody | University of Twente | Evaluating the Visual Syntax of UML: Improving the Cognitive Effectiveness of the UML Suite of Diagrams |
| Abstract: UML is a visual language. However surprisingly, there has been very little attention in either research or practice to the visual notations used in UML: both academic analyses and revisions to UML have focused almost exclusively on semantic issues, with little debate about or modification to the visual notations. We believe that this is a major oversight and that for this reason, UML's "visual development" is lagging behind its "semantic development". The lack of attention to visual aspects is particularly surprising given that the form of representations is known to have a comparatively greater effect on understanding and problem solving performance than their content. The UML visual notations were developed in a bottom-up manner, by reusing and synthesising existing notations. There is little or no justification for choice of graphical conventions, with decisions based on "expert consensus" rather than scientific evidence. This paper evaluates the UML family of diagrams using a set of predefined principles for visual notation design, which are based on theory and empirical evidence from communication, semiotics, graphic design, visual perception, psychophysics and cognitive science. This is the first comprehensive analysis of the UML visual language and covers all diagram types, constructs and symbols in the latest release of UML (2.1.2). The paper identifies some serious design flaws in the UML visual notations together with practical recommendations for improvement. The conclusion from the analysis is that radical surgery is required to the UML visual notations for them to be cognitively effective. We believe that the time is right for a major revamp of the UML visual notations now its semantics (the UML metamodel) is relatively complete and stable. | |||
| 11.11.2008 | Jeff Magee | Imperial College London | Software Architecture for Self-Managed Systems |
| Abstract: Self-management is put forward as one of the means by which we could provide systems that are scalable, support dynamic composition and rigorous analysis, and are flexible and robust in the presence of change. In the talk, we focus on architectural approaches to self- management, not because the language-level or network-level approaches are uninteresting or less promising, but because we believe that the architectural level provides the required level of abstraction and generality to deal with the challenges posed. A self-managed software architecture is one in which components automatically configure their interaction, in a way that is compatible with an overall architectural specification, to achieve the goals of the system. The objective is to minimise the degree of explicit management necessary for construction and subsequent evolution whilst preserving the architectural properties implied by its specification. The talk discusses some of the current promising work and presents an outline three-layer reference model as a context in which to articulate some of the main outstanding research challenges. In addition, the talk will describe a prototype system being developed at Imperial College that conforms to this model. | |||
| 17.10.2008 | Hannu Jaakkola | Tampere University of Technology | Discussion topics in Software Process Improvement (SPI) - Research, Training and University level Education |
| Change of time: This seminar takes place on Friday, October 17th at 10:40AM in S4 | |||
| Abstract: The aim of the presentation is to introduce shortly the activities going on CoSE (Center of Software Expertise) Institute, which is a part of the Tampere University of Technology (Pori). The university itself is the second biggest technical university in Finland. It has a satellite faculty in the City of Pori as a part of University Consortium of Pori. CoSE Institute covers academic education, industry oriented training and research in the area of software systems. In research the focus of CoSE is in the problems of software development organisations - taking into account the quality and productivity. A special attention is given in the operations of small software organisations, which suffer from very much different improvement needs than the bigger ones. In addition, the well managed growth path of small software organisations (less than 10 employees) towards the category small / medium size (up to 50 employees) is not well known. There is also reasonable little amount of studies focusing in the problems of offshoring and well managed software processes in a distributed development organisation. The presentation introduces the work done by CoSE in the research area described above. The other academic activities of the organisation are introduced shortly, too. After the presentation discussion on co-operation activities between Charles University and Tampere University of Technology is possible. | |||
| 07.10.2008 | Apostolos N. Papadopoulos | Aristotle University of Thessaloniki | An Introduction to Top-k and Skyline Computation |
| Change of place and time: This seminar takes place at 3:40PM in S3 | |||
| Abstract: Preference queries are very important to users, since they return the "best" objects according to some criteria. In this talk, we discuss the fundamental issues regarding Top-k and Skyline computation, which constitute the most important methods for determining the objects that best match users' preferences. More specifically, we study the fundamental research contributions by Ronald Fagin towards Top-k processing and an efficient Skyline algorithm. Moreover, we provide the necessary background material (e.g. R-trees) and give application examples where preference queries are of enormous interest. Additionally, we touch some advanced topics and briefly discuss research directions in the area. | |||
| 07.10.2008 | Tomas Pitner | Masaryk University | Web 2.0 -- Core Concepts, Applications, Implications |
| This seminar takes place in the regular time and place Hence at 2PM in S4 as usual | |||
| Abstract: Web 2.0 represents the recent evolutionary shift towards more user-oriented and user-driven web. The presentation will try to distil the essence of this concept -- identify the distinguishing characteristics of the new web, illustrate them on successful services, and comment on the trends. As a specific topic, the phenomenon of integrated services -- "mashups" -- will be discussed, pointing out its crucial issues including technological as well as legal and business aspects. | |||
| 20.5.2008 | Vaclav Rajlich | Wayne State University | Concept location |
| Abstract: Concept location in source code is an evolution activity that identifies where a software system implements a specific concept. While it is well accepted that concept location is essential for the maintenance of complex procedural code like code written in C, it is much less obvious whether it is also needed for the maintenance of the Object-Oriented code. After all, the Object-Oriented code is structured into classes and well-designed classes already implement concepts, so the issue seems to be reduced to the selection of the appropriate class. The objective of our work is to see if the techniques for concept location are still needed (they are) and whether Object-Oriented structuring facilitates concept location (it does not). | |||
| 12.05.08 | Alex Borgida | Rutgers University | Visions of Data Semantics: Another (and another) Look |
| Change of time: This seminar takes place on MONDAY May 12th, at 2PM (in S4 as usual) | |||
| Abstract: The problem of data semantics is establishing and maintaining a correspondence between a data source (e.g., a database, an XML document) and its intended subject matter. We review the (relatively minor) role data semantics has played in Databases under the term "semantic data models", its more prominent place in ontology-based information integration, and then outline two new views: (i) Semantics as a composition of mappings between models, and (ii) Attaching intentional aspects (stakeholder goals) to Information Systems. (Joint work with John Mylopoulos and others at Univ. of Toronto) | |||
| (Organized jointly by DSE Colloquium and the project Intelligent Models, Algorithms, Methods and Tools for the Semantic Web Realisation) | |||
| 26.11.07 | Andrew Tanenbaum | VU University Amsterdam | MINIX 3: A Reliable and Secure Operating System |
| Change of time and place: This seminar takes place on MONDAY November 26th, at 2PM in refectory 1st floor | |||
| Abstract: Most computer users nowadays are nontechnical people and have a mental model of what they expect from a computer based on their experience with TV sets and stereos: you buy it, plug it in, and it works perfectly for the next 10 years. Unfortunately, they are often disappointed as computers are not very reliable when measured against the standards of other consumer electronics devices. A large part of the problem is the operating system, which is often millions of lines of kernel code, each of which can potentially bring the system down. The worst offenders are the device drivers, which have been shown to have bug rates 3-7x more than the rest of the system. As long as we maintain the current structure of the operating system as a huge single monolithic program full of foreign code and running in kernel mode, the situation will only get worse. While there have been ad hoc attempts to patch legacy systems, what is needed is a different approach. In an attempt to provide much higher reliability, we have created a new multiserver operating system with only 4000 lines in kernel and the rest of the operating system split up into small components each running as a separate user-mode process. For example, each device driver runs as a separate process and is rigidly controlled by the kernel to give it the absolute minimum amount of power to prevent bugs in it from damaging other system components. A reincarnation server periodically tests each user- mode component and automatically replaces failed or failing components on the fly, without bringing the system down and in some cases without affecting user processes. The talk will discuss the architecture of this system, called MINIX 3, The system can be downloaded for free from www.minix3.org | |||
| 13.11.07 | Kokichi Futatsugi | JAIST Japan Advanced Institute of Science and Technology | Verifying Specifications with Proof Scores in CafeOBJ |
| Abstract: Verifying specifications is still one of the most important undeveloped topics in software engineering. It is important because quite a few critical bugs are caused at the level of domains,requirements, and/or designs. It is also important for the cases where no program codes are generated and specifications are analyzed/ verified only for justifying models of problems in real world. In this talk, a survey of our research activities in verifying specifications is given. After explaining fundamental issues and importance of verifying specifications, the proof score approach in CafeOBJ and its applications to several areas are described. | |||
| 30.10.07 | Rolf Hennicker | LMU Muenchen | Modeling and Architecture of an Integrative Environmental Simulation System |
| Abstract: We describe the concepts and design principles of an environmental simulation system which supports the study and analysis of water-related global change scenarios in the Upper Danube Basin. The system provides a Web-based platform integrating the distributed simulation models of all socio-economic and natural science disciplines taking part in the GLOWA-Danube project which is part of the German programme on global change in the hydrological cycle. Crucial aspects of the system development concern the specification of interfaces between simulation models, the treatment of the simulation space, the modeling of socio-economic actors and the coordination of coupled simulations for which we have developed a coordination framework. To ensure the correctness of the synchronization of concurrently running simulation models we have applied formal methods of process algebra. | |||
| 16.10.07 | Peter Eklund | The University of Wollongong | Enterprise Content Management |
| Abstract: We deal with Enterprise Content Management and some of the tough computing issues that are faced in that domain. This mostly draws on my experience working with my secondment company, www.objective.com, and is a mixed bag of problems: database replication, information retrieval, object caching, security and access control. | |||
| 19.06.07 | Hanspeter Moessenboeck | Johannes Kepler University Linz | Automatic Feedback-Directed Object Inlining in the Java HotSpot(TM) Virtual Machine |
| Change of place: This seminar takes place in the room S1 | |||
| Abstract: Object inlining is an optimization that embeds certain referenced objects into their referencing objects. It reduces the access costs of those objects by eliminating unnecessary loads of references. We change the order of objects in the heap in such a way that objects that are frequently accessed together are placed next to each other in memory so that their distance is fixed, i.e. these objects are colocated. This allows field loads to be replaced by address arithmetic. We implemented this optimization for Sun Microsystems' Java HotSpot VM. The necessary analysis is performed automatically at run time, requires no actions on the part of the programmer and supports dynamic class loading. We use read barriers to detect the most frequent references between objects, i.e. the ones that are worth being optimized. If an object A has a field f referencing an object B the loading of f can be safely eliminated if A and B are colocated and if the following two preconditions are satisfied: A and B must be allocated together, and f must not be changed later. These preconditions are checked by the just-in-time compiler avoiding a global data flow analysis. The garbage collector ensures that groups of colocated objects are not split: it copies groups as a whole to their new locations. The evaluation shows that our dynamic approach successfully identifies and optimizes frequently accessed fields for several benchmarks. The average peak performance speedup of 9% for SPECjvm98 (with a maximum speedup of 51%) justifies the startup overhead of 3% on average (with a maximum slowdown of 11%) that is caused mainly by the read barriers and the additional compilation of methods. | |||
| 29.5.2007 | Vaclav Rajlich | Wayne State University | Teaching Evolution of Open-Source Projects in Software Engineering Courses |
| Change of place: This seminar takes place in the room S1 | |||
| Abstract: In the traditional software engineering courses, the students develop small programs from scratch. This does not correspond to industry practice where programmers spend most of their time evolving medium to large systems. In order to narrow this gap, we developed a course where students practice software evolution through the implementation of change requests on medium-sized open-source software systems. The results of the course show that this type of software engineering course gives students a more realistic experience than traditional software engineering courses. In the survey at the end of the course, the students expressed a higher level of satisfaction with both rating the course and assessing how much they learned. Additionally, the resources required by such a course are not excessive. | |||
| 15.5.2007 | Petr Tuma | DSE | On Teaching |
| Abstract:The seminar will present a collection of various general issues related to teaching, mostly along the lines of what is the purpose of teaching, what are the common misconceptions of teaching among teachers, what is useful and what is useless to do when trying to improve teaching. The sources used include work by Paul Ramsden on university teaching and work by Joseph Novak on understanding knowledge. | |||
| 24.4.2007 | Nicolas Rivierre | France Télécom | Composite Contracts |
| Abstract:Abadi and Lamport established a general theorem for composing specifications. Based on an assume-guarantee principle, it enables one to prove the specification of a composite system from the ones of its components. In this talk, I'll investigate how this result can be exploited to leverage an existing contracting framework for hierarchical software components, in which contracts are first-class objects during configuration and run times. This framework already associates specifications and responsibilities to software components, within the traditional horizontal form of composition. We will show here how the vertical one can be made operational using the theorem as a sound formal basis. | |||