This is a list of past D3S Seminars. If you are looking for scheduled (future) seminars, please go to the main D3S Seminar page.

October 2018

2018-10-16 14:00 in S5: Effective and User-friendly Specification of Multi-Robot Missions

Patrizio Pelliccione

Mobile robots are increasingly used in everyday life to autonomously realize missions such as exploring rooms, delivering goods, or following certain paths for surveillance. The current robotic market is asking for a radical shift in the development of robotic applications where missions specification is performed by robotic users that are not highly qualified and specialized in robotics or ICT. To this aim, we first present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems, each of which detailing the usage intent, known uses, relationships to other patterns, and—most importantly—a template solution in temporal logic. The patterns originate from 245 realistic textual mission requirements extracted from the robotics literature, and they are evaluated upon a total of 449 real-world mission requirements.Then, we propose a Domain Specific Language (DSL) that enables nontechnical users to specify missions for a team of autonomous robots in a user-friendly and effective way. The DSL contains a set of atomic tasks that can be executed by robots and a set of operators that allow the composition of these tasks in complex missions. Mission specification can be performed through a textual and a graphical interface. While the DLS support is provided by a standalone tool and can be integrated within a variety of frameworks, the current implementation has been integrated with a software platform that provides a set of functionalities, including motion control, collision avoidance, image recognition, SLAM, planning, etc. Our DSL has been successfully validated with both simulation and real robots.

June 2018

2018-06-20 09:00 in S6: Networking real-time multiplayer games

Filip Krijt

For multiplayer videogames, delivering an enjoyable experience requires minimizing stuttering and latency that would otherwise arise due to the underlying network infrastructure, as well as providing a line of defense against cheaters and hackers. This implies a set of architectural design decisions, some of which are obvious, some less so. This talk will provide a short overview of the problem, as well as present a common game network architecture pattern based on the Tribes series. Variants of this pattern are still used in recent big titles such as Overwatch.

2018-06-05 14:00 in S4: Performance Awareness in Agile Software Development (defence rehearsal)

Vojtěch Horký

Broadly, agile software development is an approach where code is frequently built, tested and shipped, leading to short release cycles. Extreme version is the DevOps approach where the development, testing and deployment pipelines are merged and software is continuously tested and updated. In this context our work focuses on identifying spots where the participants should be more aware of the performance and offers approaches and tools to improve their awareness with the ultimate goal of producing better software in shorter time. In general, the awareness is raised by testing, documenting, and monitoring the performance in all phases of the development cycle.

May 2018

2018-05-30 09:00 in S7: Data-Centric Computing

Martin Děcký (Huawei Technologies)

In recent decades, the majority of mainstream computer systems we designed as CPU-centric and memory-centric. All the data that the computer processed always passed through the main memory in one way or the other and the code running on the central processor(s) manipulated the data. DMA controllers, co-processors, GPUs and intelligent NICs were used mostly as slave peripherals, although with some degree of computational acceleration and off-loading in recent years. One of the reasons for keeping the same basic architecture despite its drawbacks such as the ever-widening memory barrier (i.e. the difference between the latency of the CPU and the RAM) was arguably its conceptual simplicity. However, trends for a major change in the status quo are emerging into the mainstream. There are new non-volatile memory technologies that promise to marry the benefits of byte-addressable volatile memory and block-addressable permanent storage. Approaches such as data-centric computing and near-data processing propose to turn an ordinary computer into a distributed system where the distinction between CPU/RAM and peripherals is much more blurry than today, with the possibility to autonomously compute within and interchange data between all the hardware components. This talk presents a brief overview of the concepts and discusses consequences for the design of the software running on top of this new hardware.

2018-05-29 14:00 in S5: Simplicitly: Foundations and Applications of Implicit Function Types

Vlastimil Dort

Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts, implicitly. Scala offers implicit parameters which are used pervasively, but which cannot be abstracted over. This paper describes a generalization of implicit parameters to implicit function types, a powerful way to abstract over the context in which some piece of code is run. We provide a formalization based on bidirectional type-checking that closely follows the semantics implemented by the Scala compiler.To demonstrate their range of abstraction capabilities, we present several applications that make use of implicit function types. We show how to encode the builder pattern, tagless interpreters, reader and free monads and we assess the performance of the monadic structures presented.

2018-05-23 09:00 in S5: Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel

Andrea Parri

Concurrency in the Linux kernel can be a contentious topic. The Linux kernel mailing list features numerous discussions related to consistency models, including those of the more than 20 CPU architectures supported by the kernel and that of the kernel itself. How are Linux programs supposed to behave? Do they behave correctly on exotic hardware? A formal model can help address such questions. Better yet, an executable model allows programmers to experiment with the model to develop their intuition. In this talk, we discuss a formal model for the Linux kernel, written in the Cat language and executable by the Herd simulator, its design principles and its validation, with particular focus on the Read-Copy-Update synchronisation mechanism.

2018-05-22 14:00 in S5: Performance Modelling of Smart Cyber-Physical Systems

Vladimír Matěna

Context: the dynamic nature of complex Cyber-Physical Systems (CPS) introduces new research challenges since they need to smartly self-adapt to changing situations in their environment. This triggers the usage of methodologies that keep track of changes and raise alarms whether extra-functional requirements (e.g., safety, reliability, performance) are violated. Objective: this paper investigates the usage of software performance engineering techniques as support to provide a model-based performance evaluation of smart CPS. The goal is to understand at which extent performance models, specifically Queueing Networks (QN), are suitable to represent these dynamic scenarios. Method and Results: we evaluate the performance characteristics of a smart parking application where cars need to communicate with hot-spots to find an empty spot to park. Through QN we are able to efficiently derive performance predictions that are compared with long-run simulations, and the relative error of model-based analysis results is no larger than 10% when transient or congestion states are discarded. Conclusion: the usage of performance models is promising in this domain and our goal is to experiment further performance models in other CPS case studies to assess their effectiveness.

2018-05-15 14:00 in S5: Generalizing Uncertainty Across Domains in Industrial Cyber-Physical Systems

Rima Al Ali

Cyber-physical systems (CPS) need to be designed to deal with various forms of uncertainty associated with data contributing to the system's knowledge of the environment. Dealing with uncertainty requires adopting an appropriate model which then allows making the right decisions and carrying out the right actions (possibly affecting the environment) based on imperfect information. However, choosing and incorporating a suitable model into CPS design is difficult, especially for non-experts, because it requires identifying the kind of uncertainty at hand as well as knowledge of suitable models and their applications. While inspiration can be found in other CPS designs, the details of dealing with uncertainty in another CPS can be confounded by domain-specific terminology, context, and requirements. To make this aspect of CPS design less daunting for non-experts, we aim at providing a generalized view of approaches dealing with uncertainty in the design of CPS targeting collective behavior. To this end, we present a systematic review of relevant projects and a synthesis of relations between system features, the kinds of uncertainty, and models and methods used to deal with it. The resulting model provides a generalized view of uncertainty across different domains and challenges.

2018-05-09 09:00 in S5: Smart Home in VDM

Natalia Cantavella Franch (Erasmus student)

A smart home is a residence that uses internet-connected devices to enable the remote monitoring and management of appliances and systems, such as lighting and heating. In this talk, details of a student work in this area will be presented.

2018-05-02 09:00 in S5: Python for Data Analysis

Iuliana Bocicor (Babeş-Bolyai University, Romania)

Artificial Intelligence and Machine Learning (ML) applications are ubiquitous and actively change so many aspects of our lives nowadays. One of the most used programming languages for machine learning applications is Python. Due to its simplicity and elegance, but mostly to its powerful numerical linear algebra and scientific computing libraries, Python is easy to use and thus many popular libraries that are widely used for ML tasks are written in Python. This talk describes how Python’s ML libraries can be employed for various ML tasks, with applications in medical data analysis and classification, as well as for studies and analyses on molecular biology data (DNA classification and protein dynamics).

April 2018

2018-04-24 14:00 in S5: Abstractions and refinements in bounded model checking of software

Martin Blicha

Assertions in a code can be viewed as specifications of safety properties for the program. In the context of bounded model checking, the bounded program with an assertion can be encoded as a logical formula where a safety violation corresponds to a satisfiable assignment of the formula. Traditionally, encoding to propositional logic was used to obtain a precise model of the program. To achieve better scalability, more abstract modelling languages can be used, such as logic of equality with uninterpreted functions or linear arithmetic. As a second, orthogonal, abstraction in an incremental scenario, function summaries obtained from previous successful verification runs can be used. With abstraction introduced, the counter-examples to safety found could be spurious. In case of a spurious counter-example, the abstractions need to be refined to eliminate it. Different refinement strategies can be employed and may be beneficial for different types of programs.

2018-04-18 09:00 in S5: Decentrally Coordinated Execution of Adaptations in Distributed Self-Adaptive Software Systems

Dominik Škoda

Software systems in domains like Smart Cities, the Internet of Things or autonomous cars are coined by a high degree of distribution across several independent computing devices and the requirement to be able to adjust themselves to varying situations in their operational environment. Self-adaptive software systems are a natural choice to implement such context-dependent software systems. A multitude of approaches already implement self-adaptive systems and some consider even distribution aspects. Yet, none of the existing solutions supports the coordination of adaptation operations spanning multiple independent nodes, which is necessary to ensure a consistent adaptation even in presence of network errors or node failures. This paper, tackle this challenge to execute adaptations in distributed self-adaptive software systems in a coordinated manner. It presents a protocol that enables the self-adaptive software system to execute correlated adaptations on multiple nodes in a transactional manner ensuring an atomic and consistent transition of the distributed system from its source to the desired target configuration. The protocol is validated to be free of deadlocks for any given adaptation at any point in time using a model-checking approach. The performance of the approach is investigated in experiments that emulate the protocol’s execution on real devices for different sizes of distributed applications and adaptation scenarios.

2018-04-17 14:00 in S5: Recent developments in (multi)agent deep reinforcement learning

Jiří Vinárek

Reinforcement learning is a kind of machine learning where an agent learns its ideal behavior without prior training data, purely via trial and error. Although the underlying concepts are not new, just recently they have been significantly improved by incorporation of deep neural networks. The talk will describe principles used in deep reinforcement learning, state-of-the art algorithms and their application to agent systems.

2018-04-11 09:00 in S5: Timing and Availability Analysis of Mixed-Criticality Dependent Tasks with AADL

Etienne Borde (CNRS/Telecom ParisTech)

In safety-critical systems, scheduling real-time tasks on multi-core architectures raises important challenges. This talk will start with an explanation of these challenges and existing solutions focusing on mixed-criticality systems: systems in which functions of different criticality share execution resources. I will then introduce a complementary view point on mixed-criticality systems, dealing with availability of lower criticality functions. This will lead to present a task model with a representation of dependencies among tasks. Scheduling dependent tasks with different criticality levels on multicore processor has received little contributions, but I will present our recent results on this topic. AADL model transformations in the RAMSES (Refinement of AADL Models for the Synthesis of Embedded Systems) platform will enable to illustrate step by step these solutions.

2018-04-10 14:00 in S5: Model Transformations and Management for Complex Systems Design with AADL and RAMSES

Dominique Blouin (Telecom ParisTech)

Developing complex embedded and cyber-physical systems with models makes intensive use of model transformations, model analysis and model management in order to ensure that the interplay between the models is managed properly, in addition to the activities on each individual model. Traditional model management approaches do not scale for current industrial settings made of large ecosystems of models and making use of rich languages such as the SAE Architecture Analysis and Design Language (AADL). In particular, current model transformations tools yet do not deliver appropriate performances in such context. In this talk, I will introduce our model-based engineering work with the AADL including automated code generation with our tool RAMSES (Refinement of AADL Models for the Synthesis of Embedded Systems). I will then present current scalability and model management issues and our agenda to tackle them based on incremental model transformations and synchronizations and megamodeling.

March 2018

2018-03-28 09:00 in S5: Adaptive Dispatch: A Pattern for Performance-Aware Software Self-Adaptation (WOSP-C'18 rehearsal)

Petr Kubát

Modern software systems often employ dynamic adaptation to runtime conditions in some parts of their functionality -- well known examples range from autotuning of computing kernels through adaptive battery saving strategies of mobile applications to dynamic load balancing and failover functionality in computing clouds. Typically, the implementation of these features is problem-specific -- a particular autotuner, a particular load balancer, and so on -- and enjoys little support from the implementation environment beyond standard programming constructs. In this work, we propose Adaptive Dispatch as a generic coding pattern for implementing dynamic adaptation. We believe that such pattern can make the implementation of dynamic adaptation features better in multiple aspects -- an explicit adaptation construct makes the presence of adaptation easily visible to programmers, lends itself to manipulation with development tools, and facilitates coordination of adaptation behavior at runtime. We present an implementation of the Adaptive Dispatch pattern as an internal DSL in Scala.

January 2018

2018-01-18 10:00 in S5: Database Programming – From Active Databases via NoSQL to Cloud Computing

Oracle Researchers

Introduction into database-side programming. How to do it? Discuss the challenges of effective/efficient implementation and integration with modern programming languages.

2018-01-17 10:00 in S5: Hack into Your Compiler!

Oracle Researchers

Project Graal (JIT compiler). Implementation of Java in Java. Tour over the Graal sources, how to edit/compile/debug them. Show how to write you personal compiler.

2018-01-16 14:00 in S5: Handling uncertainty in self-adaptive cyber-physical systems

Rima Al Ali

2018-01-16 10:00 in S5: Parallel Distributed Processing of Big Data,Graphs - Parallel Graph AnalytiX (PGX)

Oracle Researchers

PGX.D is distributed parallel in-memory graph analysis toolkit: SQL-like pattern matching, participate on standardization of PGQL, Extreme performance of standard graph algorithms, Weakly scalable. How do we achieve all this?

2018-01-10 09:00 in S5: Index Checker

Vlastimil Dort

2018-01-09 14:00 in S5: Adaptive Dispatch: A Pattern for Performance-Aware Software Self-Adaptation

Petr Kubát

December 2017

2017-12-13 09:00 in S5: Programming robot swarms in Buzz language

Jiří Vinárek

One of the problems in programming of swarm robotic systems is a lack of programming primitives that would allow reusable and predictable description of a team behavior. The current practice in development of swarm systems is to either use bottom-up approach where single-robot behavior is refined until swarm-level requirements are satisfied or to use top-down approach (often used in sensor networks and spatial computing) which often has a problem with excessive simplification of the system. The talk will present the Buzz programming language from Carlo Pinciroli standing in the middle and combining advangates of the both mentioned methods.

2017-12-06 09:00 in S5: Situational Aware (SiA) Cyber-physical systems (CPS)

Dominik Škoda

Situational Aware (SiA) Cyber-physical systems (CPS) harmoniously integrate computational and physical components to being aware of what is happening in the surroundings and using this information to decide and act. Architecture description of SiA-CPS can be a valuable tool to reason about the selected solutions, and to enable code generation and simulation. There is a paper that presents an architecture framework that automatically generates from a SiA-CPS architecture description, an executable code used to simulate the architecture model and evaluate it in terms of data traffic load, battery level and energy consumptions. The framework makes use of a model transformation approach where, three SiA-CPS domain-specific modeling views are automatically transformed into the input language of CupCarbon, an opensource tool supporting the simulation of sensor network architectures.

November 2017

2017-11-29 09:00 in S5: Sampling Invariants from Frequency Distributions

Grigory Fedyukovich (University of Washington)

Automated formal verification of programs handling unbounded loops is reduced to finding safe inductive invariants that over-approximate the sets of reachable states, but precise enough to prove unreachability of the error state. Successful solutions to this problem include Counterexample-Guided Abstraction Refinement and Property Directed Reachability, but they are not guaranteed to deliver appropriate invariants. We aim at learning inductive invariants in an "enumerate-and-check" manner, and in particular we exploit the syntactical constructions which appear in the source code to iteratively obtain partial invariants (called lemmas). We present a new SMT-based, probabilistic, syntax-guided method to discover numerical inductive invariants. The core idea is to initialize frequency distributions from the program's source code, then repeatedly sample lemmas from those distributions, and terminate when the conjunction of learned lemmas becomes a safe invariant. The sampling process gets further optimized by priority distributions fine-tuned after each positive and negative sample. The stochastic nature of this approach admits simple, asynchronous parallelization. We present an implementation and evaluation of this approach in a tool called FreqHorn which shows competitive performance on well-known linear and some non-linear programs.

2017-11-28 14:00 in S5: An Ensemble-based Approach For Scalable QoS in Highly Dynamic CPS

Vladimír Matěna

Modern cyber-physical systems (CPS) often involve distributed devices/components that closely interact with each other and their environment. In this context, operation conditions may constantly change and it is not always possible to guarantee quality of service (QoS), particularly, if resourcesdegrade or stop being available. In addition, sometimes, one would like QoS to scale up/down with operation conditions, e.g., maximize efficiency, minimize energy consumption, etc. without compromising safety. However, traditional design and development techniques fail to capture the dynamics of modern CPS, since they rather focus on individual components/devices, and are unable to provide such QoS guarantees. To overcome this problem, we propose a design methodology based on the concept of ensemble, i.e., a dynamic grouping of components, which allows for scalable QoS guaranties. We illustrate the utility of our approach based on a case study consisting of an intelligent production line and analyze the effect on performance as communication between components degrades. Finally, our methodology can be incorporated into existing ensemble-based tools such as DEECo, Helena or jRESP to generate executable code to be deployed onto distributed devices.

2017-11-14 14:00 in S5: Automated Repairing of Variability Models

Paolo Arcaini

Variability models are a common means for describing the commonalities and differences in Software Product Lines (SPL); configurations of the SPL that respect the constraints imposed by the variability model define the problem space. The same variability is usually also captured in the final implementation through implementation constraints, defined in terms of preprocessor directives, build files, build-time errors, etc. Configurations satisfying the implementation constraints and producing correct (compilable) programs define the solution space. Since sometimes the variability model is defined after the implementation exists, it could wrongly assess the validity of some system configurations, i.e., it could consider acceptable some configurations (not belonging to the solution space) that do not permit to obtain a correct program. The talk presents an approach that automatically repairs variability models such that the configurations they consider valid are also part of the solution space.

2017-11-07 14:00 in S5: Google On Campus!

Ondřej Šerý (Google), Daniel Marek (Google)

Come listen about how Google runs their clusters and what Borg has to do with it, how we do planet-wide atomic transactions with SQL and extreme scalability and why certain uncertainty is your friend, and also about how life at Google is and how to taste it as a software engineering intern.

October 2017

2017-10-24 14:00 in S5: Dynatrace - monitoring large scale production environment

Alexander Scheran (DynaTrace), Philipp Lengauer (DynaTrace)

Dynatrace enables full-stack monitoring for big production environments. In this talk, we will illustrate the challenges that arise when monitoring software in production and how we deal with them. We will also describe a novel approach on how to track object allocations on a per-path basis to minimize run-time overhead.

2017-10-17 10:40 in S510: Large scale complex, dynamic, and collaborative systems - present and future

Vasilios Andrikopoulos (University of Groningen)

The maturation of service choreographies empowers the creation and operation of complex distributed software systems with collaborative and adaptive characteristics. Such systems appear in different areas of interest, e.g. pervasive systems and scientific workflows. The availability of resources on demand through cloud computing allow for scaling the infrastructure required for their instrumentation. At the same time, however, a number of challenges arise related to the cloudification of the necessary middleware and the related trade-offs between cost and performance of such systems. In this talk we discuss our effort towards addressing these challenges, as well as present a vision for a next generation of widely distributed, large scale systems which combine different computing paradigms.

June 2017

2017-06-06 10:00 in S5: GPU System Calls

Ján Veselý (Rutgers University, USA)

We explore how to directly invoke generic system calls in GPU programs. We examine how system calls should be meshed with prevailing GPGPU programming models, where thousands of threads are organized in a hierarchy of execution groups: Should a system call be invoked at the individual GPU task, or at different execution group levels? What are reasonable ordering semantics for GPU system calls across these hierarchy of execution groups? To study these questions, we implemented GENESYS – a mechanism to allow GPU programs to invoke system calls in the Linux operating system. Numerous subtle changes to Linux were necessary, as the existing kernel assumes that only CPUs invoke system calls. We analyze the performance of GENESYS using micro-benchmarks and three applications that exercise the filesystem, networking, and memory allocation subsystems of the kernel. We conclude by analyzing the suitability of all of Linux’s system calls for the GPU.

2017-06-02 09:00 in S5: Satisfiability and Verification Modulo Non-Linear Arithmetic via Abstraction Refinement

Alberto Griggio (Fondazione Bruno Kessler, Italy)

We present a novel technique for Satisfiability Modulo the quantifier-free theory of nonlinear arithmetic with transcendental functions over the reals. The approach is based on an abstraction-refinement loop, in which the nonlinear functions are represented as uninterpreted in the abstract space, which is described in terms of the combined theory of linear arithmetic on the rationals with uninterpreted functions. Nonlinear functions are incrementally axiomatized by leveraging techniques from differential calculus, using a lemmas-on-demand approach. Besides presenting the basic solving procedure, we also discuss how to integrate it in state-of-the-art SMT based techniques for the verification of transition systems with nonlinear constraints.

May 2017

2017-05-30 14:00 in S5: Checker Framework

Vlastimil Dort

The seminar will introduce the Checker Framework developed at University of Washington. The framework provides type checking of pluggable type systems for Java. Each type system is defined in terms of a collection of Java type annotations, which can be applied to types in Java 8 code. The Framework also comes with various type systems and checkers designed to find and prevent common bugs such as null pointer dereferences, out-of-bounds array accesses or invalid format strings.

2017-05-16 14:00 in S5: Collective Adaptive Systems Use Cases in EU Projects

Rima Al Ali

April 2017

2017-04-25 14:00 in S5: Efficient Search for Concurrency Errors and Debugging

Pavel Parízek

2017-04-11 14:00 in S5: Communication in intelligent ensembles

Vladimír Matěna

2017-04-05 09:00 in S5: Scalable Constraint Solving

Antti Hyvärinen (USI Lugano)

Modeling systems and reasoning about their properties in an automatic and scalable way is increasingly important in a variety of modern applications. For such an approach to be successful it is necessary to find a compromise between the expressibility of the modeling language and the efficiency of the deduction engine. The Satisfiability Modulo Theories (SMT) framework integrates a modeling language with the solving machinery, but provides little support for automatically adjusting the language to fit the needs of a particular modeling task. The proposed research answers this challenge through a natural combination of SMT theories and techniques for over-approximating and refining the model based on counter-examples that is at the same time capable of adjusting to a computing environment with a high degree of parallelism.

March 2017

2017-03-14 14:00 in S5: Context-sensitive XSS

Antonín Steinhauser

Cross-site scripting bugs are not always caused by missing sanitization of user inputs. Sometimes the inputs are sanitized, but the sanitization is incompatible with output context of the sanitized value. That can leave the application vulnerable as if no sanitization was used, but it's impossible to discover these bugs with traditional taint tracking. We propose an extension of dynamic taint tracking for web applications that can successfully discover these context-sensitive cross-site scripting bugs.

2017-03-01 09:00 in S5: MutRex: a mutation-based generator of fault detecting strings for regular expressions

Paolo Arcaini

Regular expressions permit to describe set of strings using a pattern-based syntax. Writing a correct regex that exactly captures the desired set of strings is difficult, also because a regex is seldom syntactically incorrect, and so it is rare to detect faults at parse time. We propose a fault-based approach for generating tests for regexes. We identify fault classes representing possible mistakes a user can make when writing a regex, and we introduce the notion of distinguishing string, i.e., a string that is able to witness a fault. We provide a tool, based on the automata representation of regexes, for generating distinguishing strings exposing the faults introduced in mutated versions of a regex under test. The basic generation process is improved by two techniques, namely monitoring and collecting. Experiments show that the approach produces compact test suites having a guaranteed fault detection capability, differently from other test generation approaches.

February 2017

2017-02-22 09:00 in S5: Tutorial on formal methods II.

Jan Kofroň

The seminar will introduce the basic concepts and algorithms used in software verification and model checking to make the subsequent specialized seminars more comprehensible for people from outside this research area.

January 2017

2017-01-10 14:00 in S5: Tutorial on performance evaluation: comparing alternatives

Vojtěch Horký

The seminar will introduce the basic concepts of statistical evaluation of computer performance data. The focus will be on statistical methods that are useful for evaluation whether two data sets differ (e.g. to detect performance regressions). Practical behaviour of the statistical methods on real data will be reported.

August 2009

2009-08-25 14:00 in S5: When Opportunity Proceeds from Autonomy: A Tour-Based Architecture for Disconnected Mobile Sensors

Radim Bartos (University of New Hampshire, Durham)

We consider the case of sparse mobile sensors deployed to implement missions in challenging environments. This paper explores a notion of tour networks that is well suited to circumstances in which autonomous sensing agents cannot rely on standard networking abstractions and must create their own opportunities for communication and interaction. Tours are high-level building blocks that combine motion, communication and sensing and can be assembled to implement a broad class of autonomous sensing missions. They are supported by an architecture designed to deliver performance and robustness without compromising design abstraction.

June 2009

2009-06-23 14:00 in S5: Variable Granularity for Improving Precision of Impact Analysis

Vaclav Rajlich (Wayne State University, USA)

2009-06-17 09:00 in S5: Extracting Behavior Specification of Components in Legacy Applications

Tomach Poch, Frantisek Plasil

2009-06-16 14:00 in S5: MISR : a rigorous Methodology for Identifying Safety Requirements

Michel Lemoine (ONERA/DPRS/SAE)

In the aeronautical context, numerous regulations constraints both building A/C (Aircraft) and the way they are used. In the context of many European projects mainly supported by DG TREN (Directorate-General Energy and Transport) the underlying concepts either must be compliant with current regulations, or impact so much them that regulations must be updated. In the INOUI (Inovative Operational UAV Integration) European project, as Computer Scientists, we have developed and implement MISR, a methodology that performs compliance with air regulations (mainly CS25 from EASA and Annex II of ICAO). This methodology begins with specifying the concepts under consideration – A/C and UAVs – and the current regulations. UML is used as a rigorous notation. Class diagrams support the structural view of the integration of A/C and UAVs during the different phases of flights, whereas state-transition diagrams allow to describe the dynamic aspects of the concepts. MISR has been specifically developed to help deriving, from state-transition diagrams, the safety requirements that UAV must meet. The talk will present the methodology and the first available results.

2009-06-09 14:00 in S5: Deductive Verification of Safety-critical C Programs with Frama-C

Jens Gerlach (Fraunhofer-Institut für Rechnerarchitektur und Softwaretechnik, Berlin, Germany)

Frama-C is a collection of tools for the analysis of the source code of software written in C. Frama-C is developed in the context of the ES_PASS project at CEA LIST (France). The Jessie plug-in of Frama-C allows the deductive verification of C programs, whose behavior has been formally specified with the ANSI C Specification Language (ACSL). Frama-C can often automatically prove that a piece of C software corresponds to its ACSL-specification. At Fraunhofer FIRST we use Frama-C for the verification of safety-critical railway software. In my talk I will give an overview on ACSL and will explore opportunities and limits of deductive verification with Frama-C.

2009-06-08 09:00 in a lecture room announced later: Adaptive Random Testing (ART)

Tsong Chen (Swinburne University of Technology in Australia)

Random testing is a fundamental testing technique. Recently, we have proposed how to improve the fault-detection capability of random testing by enforcing a more even, well-spread distribution of test cases over the input domain. Such an approach is named as adaptive random testing. In this seminar, we will cover 1. the motivation; 2. failure pattern based testing; 3. various principles that could enforce an even spread of test cases, and the advantages and disadvantages of their corresponding ART implementations; 4. comparison of random testing and adaptive random testing with respect to various testing effectiveness measures; 5. applications of ART

May 2009

2009-05-27 09:00 in S5: A Self Introduction & A brief outline Of Education In India

Durga Prasana Sahoo

2009-05-20 09:00 in S5: topic to be announced

Peter Libic

2009-05-19 14:00 in S5: Engineering a State of the Art Software Model Checker: MoonWalker

Viet Yen Nguyen (RWTH Aachen)

Good model checkers are hard to engineer. State space explosion, unoptimised code and outdated algorithms easily lead to a poor performing model checker. This is our experience when we engineered MoonWalker, a model checker for .NET programs. It is the central topic in this talk. The talk is outlined as follows: First, we'll introduce MoonWalker and give a live demo where we use it to hunt for a hard-to-spot data-race. This is followed by an overview of its implementation, with a particular focus on its novel algorithms and techniques that it employs to effectively traverse the state space. The talk concludes on the engineering problems we encountered, how those inspired us to devise novel solutions and which challenges lay ahead for future work.

2009-05-13 09:00 in S5: Summary of the selected papers from ETAPS'09

Ondrej Sery

The talk will summarize the selected papers from the ETAPS'09 conference. The goal is to present the most recent advancements and currend trends in testing, verification, and model checking of code.

2009-05-12 14:00 in S5: Scade

Michal Malohlava

April 2009

2009-04-29 09:00 in S5: Summary of selected papers from ETAPS'09

Pavel Parizek

The talk will focus on papers that present application of formal methods in software development tasks.

2009-04-28 14:00 in S5: Overview of recent projects and activities

Michal Bečka

2009-04-22 09:00 in S5: Virtualization and VMware

Martin Decky, Pavel Jezek

2009-04-21 14:00 in S5: What is a Multi-Modeling Language?

Martin Wirsing (Ludwig-Maximilians-Universität München)

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.

2009-04-15 09:00 in S5: Summary of the selected papers from ETAPS'09

Ondrej Sery

The talk will summarize the selected papers from the ETAPS'09 conference. The goal is to present the most recent advancements and currend trends in testing, verification, and model checking of code.

2009-04-14 14:00 in S5: Service Architectures - Open Issues

Martin Necasky

In this presentation we will briefly introduce architectures based on services, concretely service-Oriented Architectures and Event-Oriented Architectures, and we will discuss some open research problems in this area. These problems include conceptual modeling, storage, integration, evolution and security. We will introduce our new results as well as our future research related to service architectures.

2009-04-08 09:00 in S5: Partial Order Reduction for State/Event LTL

Nikola Benes (Faculty of Informatics, Masaryk University, Brno)

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL incorporates both states and events to express important properties of component-based software systems. The main contribution of this work is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.

2009-04-07 14:00 in S5: Report on a tool: CHESS

Ondrej Sery

CHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved debugging. CHESS is available for both managed and native programs. []

2009-04-01 09:00 in S5: Modeling cache sharing

Vlastimil Babka


March 2009

2009-03-18 09:00 in S5: TBP vs. Code: Extraction and Verification

Pavel Parizek, Tomas Poch

2009-03-17 14:00 in S5: Computer-Assisted Proving for the Analysis of Systems and Specifications

Wolfgang Schreiner (Johannes Kepler University, Linz, Austria)

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.

2009-03-11 09:00 in S5: TBP vs. Code: Extraction and Verification

Pavel Parizek, Tomas Poch

2009-03-10 14:00 in S5: Parallel Verification of LTL(F,G) Properties

Jitka Kudrnacova

Computational complexity of model checking is the reason, why researchers are trying to find ways how to lower the amount of memory and time needed for the model checking procedure. When considering specification formulae for model checking only from the fragment LTL(F,G), there is a way how to translate the specification formula into a finite disjunction of formulae in special form called alpha-formulae. Then, instead of verifying the original formula, we verify every formula in the disjunction. The implementation of this translation of formulae from the fragment LTL(F,G) into the finite disjunction of alpha-formulae is the main objective of this thesis. Since every alpha-formula can be easily translated into a Büchi automaton and there is a strong probability that this automaton will be significantly smaller than the automaton obtained by traditional translation of LTL formulae into Büchi automata, the translation of alpha-formula into a Büchi automaton will be implemented as well. Afterwards, model checking of alpha-formulae will be evaluated within the DiVinE environment.

2009-03-04 09:00 in S5: Overview of recent projects and activities (GAMA, CASPAR, Unreal Engine...)

Viliam Šimko

February 2009

2009-02-25 09:00 in S5:

Mini-workshop - ADAM Team, Lille, France

2009-02-24 13:30 in S5:

Mini-workshop - ADAM Team, Lille, France

January 2009

2009-01-14 09:00 in S5: Unit checking for Java IDE

Michal Kebrt

Unit testing is a frequently used technique for ensuring quality of software during its development and maintenance. Frameworks (e.g., JUnit) exist that facilitate creation, execution, and evaluation of simple unit tests. With increasing popularity of software model checking and availability of tools (e.g., Java PathFinder), a question about the place of software model checking in the development cycle is discussed. One of the ideas is to employ model checking in a way similar to unit testing; i.e., to create simple scenarios for checking small portions of software—unit checking. The benefit lies in the ability of a model checker to exhaustively examine all possible executions (including random choices and all thread interleavings). We will present results that were collected in past months while working on a diploma thesis which aims at extending Java PathFinder to support JUnit tests checking. Problems that appeared both on JPF and JUnit sides will be shown. We will also introduce the Eclipse plugin that allows to run JUnit tests under JPF.

2009-01-13 14:00 in S5: Flexible component runtime

Tomas Bures, Michal Malohlava, Petr Hnetynka

2009-01-06 14:00 in S5: Entities and dynamic reconfigurations

T. Bures, P. Hnetynka, P. Jezek, M. Malohlava, T. Poch, O. Sery


December 2008

2008-12-16 14:00 in S5: Evaluating the Visual Syntax of UML: Improving the Cognitive Effectiveness of the UML Suite of Diagrams

Daniel L. Moody (University of Twente)

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.

2008-12-10 09:00 in S5: Protocol Conformance Checking -- Steps Towards Practical Applicability

Andreas Both and Wolf Zimmermann (Universität Halle, Germany)

Often academic approaches do not make it to industrial application for several reasons. We are very interested in verifying and improving our approach in an industrial setting. In this talk we will see, how we can use the approach presented in the first talk to solve real problems in component-based systems. To show this, we will give an overview of several properties and optimizations of the defined verification process, we are working on. Last we will show the corner marks of the case study we currently perform with our industrial partner and early results.

2008-12-09 14:00 in S5: Protocol Conformance Checking - Dealing with Recursion and Concurrency

Wolf Zimmermann and Andreas Both (Universität Halle, Germany)

Often, component-based systems describe their interfaces purely by signatures. Using type-checking it can be automatically checked whether components are used consistent with the signature. However, just checking signatures is not sufficient for checking the correct usage of components. General specifications (e.g. contracts) are more useful, but fully automatic support of checking preconditions cannot be expected. An intermediate approach of these two extremes is the protocol checking approach: These approaches assume that components implements interfaces, and that component protocols are described by finite state machines that describe legal sequences of procedure calls to a component. Checking conformance to a component protocol to check whether there is a sequence of procedure calls to the component that is not accepted by its protocol. Related work also use finite state machines to describe the use of a component and reduces the protocol checking problem to a language inclusion problem of two regular languages. The approaches can construct counterexamples, i.e. sequences of procedure calls to a component that violate the component's protocol. These finite state machine approaches can also deal with concurrent execution. However, we show that if recursion is present (e.g. due to recursive call-backs) then finite state machine approaches can lead to false positives: although the approaches confirm protocol conformance, there are protocol violations. Using pushdown machines for modeling the use of components, it is possible to avoid this problem. However, concurrency is not modeled with pushdown machines. Our main contribution is the extension of the above appoches for protocol conformance checking to recursion and concurrency. For modelling recursive procedure and concurrent execution we use process rewrite systems (Mayr 1997). We use his decidability results to show that the protocol conformance checking problem becomes now undecidable. Therefore we check use a conservative approach for checking protocol conformance. False negatives introduced due the conservative approximation might be improved by a CEGAR-approach (counter-example guided abstraction refinement) or by safely pruning the search for counter-examples. Finally, we show that process rewrite systems can be made compositional which enables their use for component systems without availability of the component's code.

2008-12-02 14:00 in S5: Optimization and Verification in Embedded Real-time Systems

Zdeněk Hanzálek (Faculty of Electrical Engineering, Czech Technical University in Prague)

2008-12-01 14:00 in a lecture room announced later: On the Observable Behaviour of Composite Components

Rolf Hennicker (Ludwig-Maximilians-Universität München)

The crucial strength of the component paradigm lies in the possibility to encapsulate behaviours. In this work, we focus on the observable behaviour of composite components which encapsulate the behaviour of (possibly large) assemblies of connected subcomponents. We first present our general component model which is equipped with a precise formal semantics allowing us to distinguish systematically different kinds of behaviours for ports, for components, and for component assemblies; technically we use UML2 notation for describing component structures and I/O-transition systems for behaviours. Then we investigate an efficient method for the computation of the observable behaviour of composite components which can circumvent the possibly infeasible intermediate computation of the usually complex behaviour of underlying assemblies if there are behaviourally neutral subcomponents. Finally, we utilise the fact that components are connected via ports such that checks for behavioural neutrality of components can be reduced to checks for behavioural neutrality of connected ports in the case of weakly deterministic port behaviours.

November 2008

2008-11-26 09:00 in S5: ADCSS 2008 - Report from ESA workshop

Pavel Ježek

2008-11-25 14:00 in S5: Ensuring Component Models’ Consistency by Means of Metamodel Level WFRs

Vladiela Petrascu (Babes-Bolyai University of Cluj-Napoca, Romania)

When designing a metamodel for a particular application domain, offering just the structural view of allowed concepts and relationships is not enough. Most often, there are additional constraints that must be enforced, which cannot be expressed in a graphical manner. These take the form of metamodel WFRs (Well Formedness Rules) and may be stated in either natural language or using a textual formalism, such as OCL. The latter approach is desirable, since it enables to take advantage from automatic tool support in checking models’ consistency with respect to the stated WFRs. We argue these ideas using a proposal for a component metamodel, together with the OCLE tool. Within the universe of OCL-supporting tools, OCLE distinguishes itself by the fact that it not only reports validation errors, but it also offers a valuable aid in identifying the failure reasons and correcting them in real time. Since, generally, the same WFR can be expressed by multiple equivalent OCL expressions, we show that the shape of such an expression is highly important from an evaluation perspective.

2008-11-19 09:00 in S5: Extraction of high-level behavior specification - Related work

Tomas Poch


2008-11-18 14:00 in S5: The Java Modeling Language

Viliam Holub

The Java Modelling Language (JML) is a design-by-contract formal specification language for Java. JML keeps close to Java's syntax, thus making the language easier to learn, but extends the language with special constructs when the original syntax lacks of expressiveness. In this talk, we will explain basic annotating constructs of Java classes and interfaces as well as more advanced constructs.

2008-11-12 09:00 in S5: A Component Framework for Java-based Real-Time Embedded Systems

Ales Plsek (INRIA, France)

The Real-Time Specification for Java (RTSJ) is becoming a popular choice in the world of real-time and embedded programming. However, RTSJ introduces many non-intuitive rules and restrictions which prevent its wide adoption. In this talk we extend our philosophy that RTSJ concepts need to be considered at early stages of software development, postulated in our prior work, in a framework that provides continuum between the design and implementation process. A component model designed specially for RTSJ serves here as a cornerstone. As the first contribution of this work, we propose a development process where RTSJ concepts are manipulated independently of functional aspects. Second, we mitigate complexities of RTSJ-development by automatically generating execution infrastructure where real-time concerns are transparently managed. We thus allow developers to create systems for variously constrained real-time and embedded environments. Performed benchmarks show that the overhead of the framework is minimal in comparison to manually written object-oriented applications, while providing more extensive functionality. Finally, the framework is designed with the stress on dynamic adaptability of target systems, a property we envisage as a fundamental in an upcoming era of massively developed real-time systems.

2008-11-11 14:00 in S5: Software Architecture for Self-Managed Systems

Jeff Magee (Department of Computing, Imperial College London)

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.

2008-11-05 09:00 in S5: Formal Specification and Verification of Distributed Components

Antonio Cansado (Sophia Antipolis, INRIA, France)

This seminar addresses behavioural specification of distributed components.We present a specification language that allows us to specify the behaviour of distributed components, and behavioural models that can be created from instances of the specification language. The specification language is close to Java, and provides a powerful high-level abstraction of the system. It deals with hierarchical components that communicate by asynchronous method calls, gives the component behaviour as a set of services, and provides semantics close to a programming language by dealing with abstractions of user-code. The benefits are twofold: (i) we can interface with verification tools, so we are able to verify various kinds of properties; and (ii), the specification is complete enough to generate code-skeletons defining the control part of the components.

2008-11-04 14:00 in S5: Specification and Verification Tools for Grid Component-based Applications

Eric Madelaine (Sophia Antipolis, INRIA, France)

The Oasis team develops methods for programming large scale Grid applications using (distributed) component-based technics. One important point in this approach is to provide formal models, and software tools, to garantee the properties of components, of their composition, and of application managment, including reconfiguration of the components. In this presentation, we will describe a behavioral model that is suitable for modelling such applications, and for reasonning about their behavioral properties. The model is called "Parameterized Networks of Synchronised Automata" (pNets), and is both expressive and compact (hierarchical and paramaterized by data variables). We will show how we generate pNets models for Fractal components (including their non-functional managment) and for distributed components. We will discuss abstraction methods for building finite abstract models preserving behavioral properties of our components. And we will describe our prototype tool platform Vercors, and show som eresults on a case-study.

October 2008

2008-10-22 09:00 in S5: A CBSE approach for the development of trustwothy systems

Mubarak Mohammad (Concordia University, Canada)

Developing trustworthy software systems that are complex, and used by a large heterogenous population of users is a challenging task. Component-based software engineering (CBSE) has many attractive features that can provide an effective solution to these challenging issues. However, the essential requirements of CBSE have not been met in the current approaches. Therefore, we present a CBSE approach that involves three contributions. The first contribution is a component model that defines the trustworthiness quality attributes as first class structural elements. This enables us to formally verify trustworthiness properties and demonstrate that a high level of trustworthiness has been achieved. In our approach, formalism is integrated into the various stages of the development process. So, our second contribution is a process model that plays this role. The third and final contribution is a development framework of comprehensive tool support. We describe the tools and justify their role in assuring trustworthiness during the different stages of software development.

2008-10-21 14:00 in S5: A formal component model and ADL for trustwothy systems

Mubarak Mohammad (Concordia University, Canada)

Existing architecture description languages mainly support the specification of the structural elements of the system under design. These languages have either only a limited support or no support to specify non-functional requirements. In a component-based development of trustworthy systems, the trustworthiness properties must be specified at the architectural level. Analysis techniques should be available to verify the trustworthiness properties early at design time. Towards this goal we present a meta-architecture that is based on formal foundataion and TADL, a new architecture description language suited for describing the architecture of trustworthy component-based systems. The TADL is a uniform language for specifying the structural, functional, and nonfunctional requirements of component-based systems. It also provides a uniform source for analyzing the different trustworthiness properties using unified methods. Also, we presents analysis techniques to generate behavior models and verify the trustworthiness properties by analyzing the TADL specification early at design time.

2008-10-15 09:00 in S5: Java Profiling

Peter Libic

Mainly presentation of paper by Georges A., Buytaert D. and Eeckhout L. from Department of Electronics and Information Systems, Ghent University, Belgium - Statistically Rigorous Java Performance Evaluation. Discussion of performance measurement methodologies and guidelines how to interpret results, so they are correct from statistical perspective. Main focus is for Java language, but the ideas are applicable in all languages.

2008-10-08 09:00 in S5: Resource Experiments in Q-Impress

Petr Tuma


2008-10-07 15:40 in S3: An Introduction to Top-k and Skyline Computation

Apostolos N. Papadopoulos (Aristotle University of Thessaloniki)

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.

2008-10-07 14:00 in S5: Web 2.0 -- Core Concepts, Applications, and Implications

Tomáš Pitner (Masaryk University, Brno)

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.

2008-10-01 09:00 in S5: INRIA Internship Experience

Michal Malohlava

The presentation describes experiences obtained during an internship in ADAM project-team in INRIA. It presents results of work which was done in the context of generation an execution infrastructure of RTSJ-based component systems. Except this research related information, the talk also mentions several notes about living and working in France.

September 2008

2008-09-23 14:00 in S5: Formal Verification of Components in Java

Pavel Parízek

Formal verification of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior specification and other properties like absence of concurrency errors. In this thesis, we focus on verification of primitive components implemented in Java against the properties of obeying a behavior specification defined in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core verification tool. We propose a set of techniques that address the key issues of formal verification of real-life components in Java via model checking: support for high-level property of obeying a behavior specification, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java bytecode and various heuristics. We have implemented all the techniques in the COMBAT toolset and evaluated them on two realistic component applications. Results of the experiments show that the techniques are viable.

2008-09-17 09:00 in S5: NIPS: Towards Reusable Components in Model Checking Tools

Michael Weber (University of Twente, Netherlands)

The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages. To evaluate the benefits of the proposed approach, several tools have been built around the VM implementation we developed, among them a model checker for Embedded Systems software.

2008-09-16 14:00 in S5: A Software Component Model with Encapsulation and Compositionality

Kung-Kiu Lau (University of Manchester, UK)

A software component model should define what components are and how they can be composed. Current models lack explicit composition operators with proper composition theories. In this talk we discuss a model we have defined. Our model has explicit composition operators that can be used in both the design phase and the deployment phase of the component life cycle. Composition operators themselves can be composed. Such composite composition operators are in fact design patterns. Furthermore, our model can also be specialised into domain-specific models by using domain models.

2008-09-02 14:00 in S5: Real-Time Java in Space On-Board Software

Martin Děcký

Results of evaluating the usability of two real-time Java implementations for space on-board software at SciSys UK Ltd. General properties of hard real-time systems used by the European Space Agency and Real-Time Java are also discussed. The other part of the talk is dealing with the big picture of using Java in space, especially concerning explicit architecture description (components), verification of correctness and other safety properties.

2008-09-23 14:00 in S5: Formal Verification of Components in Java

Pavel Parízek

2008-09-17 09:00 in S5: NIPS: Towards Reusable Components in Model Checking Tools

Michael Weber (University of Twente, Netherlands)

The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages. To evaluate the benefits of the proposed approach, several tools have been built around the VM implementation we developed, among them a model checker for Embedded Systems software.

2008-09-16 14:00 in S5: A Software Component Model with Encapsulation and Compositionality

Kung-Kiu Lau (University of Manchester, UK)

A software component model should define what components are and how they can be composed. Current models lack explicit composition operators with proper composition theories. In this talk we discuss a model we have defined. Our model has explicit composition operators that can be used in both the design phase and the deployment phase of the component life cycle. Composition operators themselves can be composed. Such composite composition operators are in fact design patterns. Furthermore, our model can also be specialised into domain-specific models by using domain models.

2008-09-02 14:00 in S5: Real-Time Java in Space On-Board Software

Martin Děcký

Results of evaluating the usability of two real-time Java implementations for space on-board software at SciSys UK Ltd. General properties of hard real-time systems used by the European Space Agency and Real-Time Java are also discussed. The other part of the talk is dealing with the big picture of using Java in space, especially concerning explicit architecture description (components), verification of correctness and other safety properties.

July 2008

2008-07-23 14:00 in S1: Performance Optimizations in High Performance Computing

Juan Ángel Lorenzo

Using hardware counters to improve performance of irregular code on FinnisTerae computing cluster.

2008-07-01 14:00 in S5: Computational Grid: Uniform remote access to HPC resources

Vladimír Mencl (Canterbury Christ Church University)

May 2008

2008-05-27 14:00 in S5: CoCoME in SOFA

Peter Hladký

CoCoME – The Common Component Modeling Example models a real trading system. The implementation of CoCoME serves as a benchmark for software modeling technologies, including performance modeling. The goal is to create a version of CoCoME suitable for performance modeling with hardware resource usage by individual parts of the application. The talk will be about technologies and procedures used to implement CoCoME in SOFA component model with components reflecting the existing SOFA CoCoME architecture.

2008-05-20 14:00 in S4: Concept location

Václav Rajlich (Wayne State University)

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).

2008-05-13 16:00 in Refektář: Otakar Smrž (ÚFAL), František Mráz (KTIML), Jan Kofroň (KSI), Zdeněk Hedrlín, Tomáš Bílý (KAM)


2008-05-12 14:00 in S4: Visions of Data Semantics: Another (and another) Look

Alex Borgida (Rutgers University)

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)

2008-05-07 09:00 in S5: Performance modeling with resource sharing using QPN

Vlastimil Babka

The talk gives an overview of our previous and recent work in performance prediction of component systems with resource sharing. In the past we have been using the LQN formalism for the performance model of the CoCoME system. The talk discusses the benefits of switching to the QPN formalism and first results of the work in progress, demonstrating the new possibilities of resource modeling.

2008-05-06 14:00 in S5: What is New in Windows Vista (Kernel)

Pavel Ježek

April 2008

2008-04-30 09:00 in S5: Extending Zing Models with Native .NET Code: Demo

Jiří Adámek

Demonstration of the native .NET Zing model extensions (a new feature in the Zing model checker for VS 2005).

2008-04-29 14:00 in S5: Best Programming Practices – Course Overview

Lubomír Bulej

The purpose of the talk is to provide basic overview of a new course called "Best Programming Practices" taught at the Department of Software Engineering. The goal of the course is to provide students with guidelines and techniques for writing quality code, attempting to fill the gap in the curriculum concerning this aspect of software development. In the talk, the motivation for introducing such a course will be presented, along with information on course structure and requirements, as well as brief outline of the contents along with a few examples.

2008-04-22 14:00 in S5: Modeling Component Environment in Presence of Callbacks and Autonomous Activities

Pavel Parízek

2008-04-17 14:00 in a lecture room announced later: Experimental work in explicit model checking

Radek Pelánek (FI MUNI)

We present BEEM (BEnchmarks for Explicit Model checkers) and experiments performed over this benchmark set, e.g., study of properties of state spaces, evaluation of error detection techniques, evaluation of techniques for reducing memory consumption of model checkers. We will also mention the model checker DiVinE and related research by verification group in Brno.

2008-04-16 09:00 in S5: Enhanced OSGi Bundle Resolution and Update – Component-based Simulation: First Thoughts

Přemysl Brada, Petr Zelenka (Západočeská Univerzita)

2008-04-09 09:00 in S5: Interact: A general contract model for the guarantee of components and services assemblies

Alain Ozanne (France Telecom R&D)

In industry as well as in research, commonly used component and service frameworks don't support tools that enable to reason in a generic way on the reliability and robustness of their architectural configurations. In this talk, I will present Interact a contracting framework that meets this need. I will show how it can guarantee an assembly of components or services by organizing in a generic way the verifications of their specifications. I will also explain how Interact can handle various formalisms and can be applied to different types of components and services.

2008-04-08 14:00 in S5: HelenOS IPC and Behavior Protocols

Martin Děcký

Overview of the features of HelenOS IPC mechanism and considerations about deploying Behavior Protocols as a formal base for run-time IPC communication checking.

2008-04-02 09:00 in S5: SOFA - internal mini-seminar

Michal Malohlava

2008-04-01 14:00 in S5: Typestate for Multiple Interacting Objects

Ondřej Lhoták (University of Waterloo)

Typestate is a formalism for specifying and verifying the temporal behaviour of an object. A finite automaton is associated with each object, and each operation is modelled by a transition of the automaton. However, the behaviour of an object-oriented system depends on interactions between multiple objects. We have extended typestate to collections of interacting objects. The intended behaviour is specified using a "tracematch", a temporal extension of an AspectJ pointcut. The behaviour can be checked dynamically or verified statically. A key challenge in verifying object behaviour is determining which objects are referenced by program variables at different times. This talk will present a precise static analysis that we have developed for verifying temporal safety properties of a system of interacting objects.

March 2008

2008-03-25 14:00 in S5: Report on the paper 'M.B. Dwyer, J. Hatcliff, Robby, C. S. Pasareanu, and W. Visser. Formal Software Analysis: Emerging Trends in Software Model Checking'

Pavel Parízek

2008-03-19 09:00 in S5: Q-ImPrESS

František Plášil

2008-03-18 14:00 in S5: Formalizing Threads in Behavior Protocols

Jan Kofroň

When reasoning about behavior compatibility of comunicating software components (e.g. in SOFA2), parallel processing of a method call may cause both appearance of an artificial error and hiding of a real one. In this talk, we will present a method of capturing the notion of thread within a behavior specification to face the problem. We will also discuss related issues and, since it is still work in progress, also the future work.

2008-03-11 14:00 in S5: Report about "Workshop on CBSE Life Cycle (22-23 January 2008, Manchester, UK)"

Petr Hnětynka

2008-03-10 14:00 in a lecture room announced later: Service Compositions: From Models to Self-Management

Howard Foster (Imperial College London)

The talk and demonstrations will illustrate a rigorous approach to the engineering of services for service-oriented architectures and in particular, web service compositions. We use formal model checking techniques to cover aspects of architecture, orchestration, choreography and deployment configurations for service compositions. A demonstration will illustrate our techniques using an Eclipse based tool, known as WS-Engineer. WS-Engineer is based upon the Labelled Transition System Analyser (LTSA) and provides mechanisms to assist engineers in developing and analyzing service compositions. The tool has also been adopted as part of academic courses in the teaching aspects of a services science. The talk is based on work in London Software Systems a grouping that includes academics at Imperial College London (the speaker, Jeff Magee, Jeff Kramer and Sebastian Uchitel) and at University College London (Wolfgang Emmerich, Anthony Finkelstein and David Rosenblum).<br><br>Howard Foster is currently a Research Fellow with the Department of Computing, Imperial College London. His research interests include services, compositions, choreography and model-based verification and validation techniques. He is also actively working in the area of software self-management and behavioral synthesis of software components. He obtained his PhD in 2006 at Imperial College London and has over 10 years industrial experience as a Principal Consultant for leading Business and IT Professional Service organizations.

2008-03-05 09:00 in S5: Behavior analysis with Blast

Ondřej Šerý

Status report on extending the Blast model checker to support checking C code against behavior specification. Presentation of the idea of encoding behavior specification as a separate CPA, summary of necessary changes in the Blast tool, demonstration of the prototype implementation and discussion on open issues and further directions.

2008-03-04 14:00 in S5: Behavior Extraction using Recoder

Tomáš Poch

Ensuring the compatibility between component behavior specification and implementation is an important part of the component behavior related reasoning puzzle. The presented approach seems to be an alternative to the technique combining the state spaces of implementation and specification. Instead of it, the latter one is abstracted from the former one. The abstraction is guided by the user to bridge the gap between the power of a general program and the limited expressivness of the specification language.

February 2008

2008-02-27 09:00 in S5: Configurable Software Verification

Grégory Théoduloz (École Polytechnique Fédérale de Lausanne)

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. In this talk, I shall present an algorithm that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool implementation take one or more abstract interpreters, such as a predicate abstraction, a shape analysis, or other abstract domains, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.

2008-02-26 14:00 in S5: Inter-Object and Intra-Object Concurrency in Creol

Jasmin Blanchette (University of Oslo)

In traditional object-oriented languages, method calls are synchronous. This suits tightly coupled systems but leads to unnecessary delays in distributed environments. Another problem shared by thread-based object-oriented languages is that control threads may interfere with each other. Creol is a language for concurrent objects that addresses these issues through two novel language constructs: asynchronous method calls and explicit processor release points. The language is gradually being extended to incorporate facilities for reflective programming, dynamic updates, and a coordination language based on behavioral interfaces.

2008-02-13 14:00 in S5: Modular Functional Specifications or: How to break down complex things to build them up properly

Bernhard Schätz (TU München)

The construction of reactive systems often requires the combination of different individual functionalities, thus leading to a complex overall behavior. To achieve an efficient construction of reliable systems, a structured approach to the definition of the behavior is needed. Here, functional modularization supports a separation of the overall functionality into individual functions as well as their combination to construct the intended behavior, by using functional modules as basic paradigm together with conjunctive and disjunctive modular composition. Combined with a notion of refinement including the treatment of partiality as well as non-determinism and supported by automatic proof mechanisms, a methodical construction of complex reactive behavior is achieved.

2008-02-12 14:00 in S5: Domain-Specific Languages for Industrial Automation

Dominik Hurnaus (Johannes Kepler Universität Linz)

January 2008

2008-01-22 14:00 in S5: Reo Networks and Symbolic Constraint Automata

Tobias Blechmann (TU Dresden)

Reo is a channel-based exogenous coordination language in which complex coordinators, called connectors, are compositionally built out of simpler ones. Constraint Automatas have been introduced as an operational model for connectors described in Reo. This talk introduces a symbolic representation for Constraint Automatas and addresses the problem of compositionally building them for given Reo connectors. Further it reports on techniques to efficiently minimize a given symbolic constraint automata or to check whether two given automatas show equivalent behavior.

2008-01-16 09:00 in S5: Performance Prediction using QPN Models: From Capacity Planning to Online Performance Management

Samuel Kounev (University of Cambridge)

2008-01-15 15:00 in S5: Components, Partitions, Networks: Our Approach to Use IMA Principles in Spacecraft On-board Applications

Marek Procházka (Space Sytems and Applications)

December 2007

2007-12-18 14:00 in S5: ProSave

Tomáš Bureš

2007-12-12 09:00 in S5: Miniseminar - Internal meeting

Petr Hnětynka

2007-12-11 14:00 in S5: Spec# and BoogiePL

Pavel Ježek

Spec# language is a research extension of the standard C# language. It adds specification of contracts to allow developers to write correct programs with less effort and with support of standard tools. BoogiePL is a language in the center of the Spec# platforms allowing using the platform to verify programs in other languages (like C, Java, Eiffel) and also to test different theorem provers (other than Microsoft's Z3). The presentation is a mixture of talks by K. Rustan M. Leino from Microsoft Research, Redmond (with minor updates to reflect current version of Spec#). Original version of his talks can be found at <a href=""></a>

2007-12-05 09:00 in S5: Java 7

Michal Malohlava

New version of Java language is extensively discussed in Java community. Many proposals of new features and language extensions exist, but only a few of them are really specified by JSR. This talk try to make a brief overview of main features and projects which can be expected to become a part of Java 7.

2007-12-04 14:00 in S5: Component-Based Design of Safe Real-Time Kernels for Embedded Systems

Jesper Berthing (University of Southern Denmark)

Real-time kernels are usually implemented as monolithic kernels, whereby the kernel is organized in a number of service layers that operate on shared data structures. The monolithic approach results in relatively large kernels, which are difficult to scale up or down to the requirements of specific embedded applications. Component-based design offers a solution to this problem by encapsulating data and system functions into subsystems implemented as reconfigurable components, which can be used to build various kernel configurations in accordance with application requirements. This presentation is about the HARTEX kernel framework, which defines kernel component and configuration models, and a formalized approach to component development and kernel configuration. It has been used to develop a repository of components that can be used to configure safe real-time kernels for hard-real-time embedded applications. In this framework, a component is defined as a self-contained unit encapsulating a kernel subsystem, such as task management, event management, resource management, etc. Complex components are decomposed into sub-components that implement an atomic functionality within the subsystem under consideration. Each component is specified in terms of public functions (primitives) and protected functions that are used by other components. Accordingly, kernel configurations are modelled by component call graphs that represent kernel components and their interactions. Configurations are actually developed by deriving a conformance class specification from the requirements specification of a real-time application, and then mapping it onto an appropriate subset of kernel components, augmented with relevant component dependencies. Kernel safety is enhanced by the rigorous design of kernel functions, using advanced algorithms that provide for very small overhead and constant execution time of kernel primitives, independent of the number of tasks involved.

November 2007

2007-11-27 14:00 in S5: SiSSy, Recoder, Java2PCM &ndash; tools (possibly) useful in Q-ImPrESS

Ondrej Mikle

SiSSy - Java/C++/Delphi to common metamodel transformation. Reporting on code structural flaws (bad code style, etc.). Recoder - Java framework for source code metaprogramming - Java analysis and transformation tools. Java source to AST, analyze/transform and write back as source. Java2PCM - reverse engineering tool for converting plain Java sources to Palladio Component Model SEFF diagrams.

2007-11-26 14:00 in S4: MINIX 3: A Reliable and Secure Operating System

Andrew S. Tanenbaum

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

2007-11-26 09:00 in a lecture room announced later: Behavior Protocols: Approaching code

Ondřej Šerý

Since checking the code is one of the crucial tasks necessary to succeed in our current projects, several extensions of EBP making the specification closer to code will be presented. Moreover, the resulting language could be beneficial for evaluating performance.

2007-11-21 09:00 in S5: Formal Subgroup Miniseminar

Frantisek Plasil

2007-11-14 09:00 in S5: Overview of the BLAST model-checker

Ondřej Šerý

2007-11-13 14:00 in S4: Verifying Specifications with Proof Scores in CafeOBJ

Kokichi Futatsugi

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.

2007-11-07 09:00 in S5: SOFA &ndash; Internal meeting

Petr Hnětynka

2007-11-06 14:00 in S5: Klapper

Antonino Sabetta (ISTI CNR, Pisa)

2007-11-05 14:15 in a lecture room announced later: Platform-independent Performance Prediction

Michael Kuperberg (Universität Karlsruhe)

2007-11-05 12:30 in a lecture room announced later: Palladio

Klaus Krogmann (Universität Karlsruhe)

October 2007

2007-10-31 09:00 in S5: A decade of AutoFOCUS: process, methods, models, tools

Florian Hölzl (TU München)

During the last decade the chair of software and systems engineering conducted intensive research in the field of distributed systems as can be found for example in embedded systems in modern cars and airplanes. Software and systems engineering thereby comprises suitable processes, methods, models and tools. In this talk I will give an overview of our research results in the different phases of the engineering process. Development starts with the requirements engineering phase. RE is very important, because any errors introduced here can have serious impact (read costs) on the later development activities. During system design we obtain a profound understanding of the system under development through the specification of the system using suitable models that range from coarse, abstract ones to fine-grained, implementation related ones. Along these levels of abstraction, we usually specify the data the system works with, its structure or architecture, and its behavior, i.e. dynamic aspects, of the system parts. The system interface from the user's perspective must also be specified during the design phase. User acceptance relies heavily on the usability of the system. This is an important topic that has to be treated during requirements analysis and system design. In modern model-based software engineering processes implementation is mostly reduced to code generation. However, deployment of the system into its runtime environment is a complex task that also uses specific models to define, e.g., task and bus schedules. Due to the complexity of modern systems and real applications system development must follow a rigorous process and defined methods. Furthermore, these have to be supported by suitable tools that take care of development artifact management and allow complex engineering tasks and analyses to be executed in reasonable time.

2007-10-30 14:00 in S4: Modeling and Architecture of an Integrative Environmental Simulation System

Rolf Hennicker (LMU München)

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.

2007-10-24 09:00 in S5: Reflecting Creation and Destruction of Instances in Component-Based Systems Modelling and Verification

Barbora Zimmerová (FI MUNI)

The talk discusses our solution to the issue of modelling and verification of communicational behaviour in component-based systems allowing creation and destruction of component instances. In the talk, I first present a modelling technique for capturing each component type and component instance as a finite-state transition system, and define the system model as a collection of those. Then I am going to present a verification technique we have defined for such a type of systems, and discuss application of the technique to the systems with dynamic instantiation of components at run time.

2007-10-23 14:00 in S5: Evaluating Non-Determinism in Linux with Different Page Allocation Strategies

Tomáš Kalibera

Although physical page allocation is well known to impact both mean performance and performance determinism, existing evaluation work of different page allocation strategies has so far only covered their impact on mean performance. The talk will present statistical methods, benchmarks, and results of an evaluation of non-determinism in performance of Linux applications, comparing bin-hopping, page coloring and the default Linux page allocation strategy.

2007-10-19 09:00 in a lecture room announced later: Ph.D. rehearsal

Jaroslav Gergic

2007-10-17 09:00 in S5: Using StrategoXT for generation of software connectors

Michal Malohlava

Software connectors are used in component based systems as a special entities modeling and realizing component interactions. Besides this behavior, connectors can provide extra functionality and benefits (e.g. logging, adaptation, monitoring). This approach requires generation of connector code with respect to requirements of components, a target environment and features specified at the design stage. In this talk I will show how to extend the existing connector generator by the Stratego/XT transformation engine, which includes a language for implementing program transformations and a collection of transformation tools. The toolset helps to realize a simple method of defining connector implementation, which is used as a template for a process of generation source code.

2007-10-16 14:00 in S4: Enterprise Content Management

Peter Eklund (The University of Wollongong)

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,, and is a mixed bag of problems: database replication, information retrieval, object caching, security and access control.

2007-10-10 09:00 in S5: EPEW 2007 &ndash; Overview of selected papers

Vlastimil Babka

The talk will provide an overview of the keynote and two selected papers presented at the 4th European Performance Evaluation Workshop (EPEW), which was held on September 27-28, 2007 in Berlin, Germany. The keynote and the papers address optimization problems in service provisioning systems, property-driven stochastic model checking using the SPDL logic, and the problem of automated generation of architectural feedback from performance analysis.

2007-10-03 09:00 in S5: UPPAAL 4.0

Tomáš Poch

Uppaal is a state-of-the-art explicit model checker for real-time systems. It has been developed jointly by Uppsala University and Aalborg University. So far, it has been successfully applied on many case studies ranging from communication protocols to multimedia applications. Within this seminar, an overview of basic functions and a verification algorithm will be presented.

Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>
  • How to find us?
Modified on 2016-06-15