Dawid Nowak
(UCD, Ireland)

With increasing growth in adoption of various cloud offering companies are finding themselves in a situation where it is getting harder and harder to test their applications. As number of possible components grows it becomes harder and harder generate enough load in the system to ensure that the application is working sufficiently well under stress. Even when enough load is generated the analysis of the output leaves much scope for improvement as the tools available on the market offer a very limited functionality when it comes to analysis and correlation of data points from different sources such as network monitoring tools, application logs, heap dumps, system performance monitors. Sophisticated algorithms are needed to automatically understand and correlate key points and automatically identify bottlenecks and other patterns of invalid behaviour. In this presentation I would like to highlight some of these problems from the perspective of a big verification lab.

Peter Libic

nWhich GC algorithm is better? When developers care for performance they usually ignore reference counting as an option that is too slow. The talk will present a recent paper showing that a well tuned and optimized reference counting collector can compete in performance with a modern tracing collector.

Tomas Pop

Growing performance of hand-held devices hardware prepares ground for a growing market of mobile applications. The advantage of running applications anytime anywhere has one significant drawback - it increases battery consumption. As the Internet connection has become available nearly anywhere, annattractive technique to overcome this obstacle is a remote execution of processor intensive parts of an applicationnin the case of available network connection...

Viliam Simko

Textual use-cases have been traditionally used at the design stage of development process for describing software functionality from the user's view. Their advantage is that they can beneasily understood by stakeholders and domain experts. However, since use-cases typically rely on a natural language, they cannot be directly subject to a formal verification. We present FOAM - a method featuring simple user-definable annotations, which are insertedninto a use-case to make its semantics more suitable for verification. Subsequently a model-checking tool verifies temporal invariants associated with the annotations. This way, FOAM allows for harnessing the benefits of model-checking while still keeping the use-casesnunderstandable for non-experts.

Vlastimil Babka

The seminar is based on the paper to be presented at ICPE 2012, put into the context of the previous talks about our Composable Cache Model and its evaluation. We investigate the problem of obtaining accurate stack profiles that serve as inputs of the model and thus greatly affect its accuracy. The problem appear to be related to the LRU approximation used in the processor. We show how the two of the previously used approaches for obtaining stack profiles can be combined using a specially developed algorithm that performs memory accesses according to a given profile. The resulting profiles singnificantly improve the model accuracy.n

Jaroslav Keznikl

Summary of the topics presented on the ASCENS meeting in Florence.

Ilias Gerostathopoulos

The aim of this talk is to present the advances of the Lero - Irish Research Center - in specifying a formal language for knowledge representation in autonomic service component-ensembles termed "Knowlang". The requirements, design choices and the proposed specification model is discussed. The use of Knowlang in the "Robots Ensemble" use case is also briefly examined.

David Hauzar

Jaroslav Král

Large information systems (IS) support as a rule business and are involved in social processes. We show that implies that the communication of software components forming the IS must take human aspects into account. The communication must be based on messages well understood by users. The messages should be coarse grained, declarative, and based on user knowledge domain. Many components are integrated as black boxes. Examples are legacies or the (information) systems of business partners. Their interfaces are as a rule fine grained and programmer oriented (they use RPC). We have often a limited possibility, if any, to change it as usually no source code is available. An effective solution in SOA is to design the interface as two layer structure where the upper layer is implemented as a service called front-end gate (FEG). We show that FEG can easily solve many business needs (agile business processes, role in business suits, development of business intelligence) and has many technical advantages (easy prototyping, agile development). FEG is in fact a connector. SOA in common sense does rarely explicitly use the concept of connector. The most important is that FEG can be easily modified onto head of a composition service (HCS) enabling unlimited composition of services. HCS can be modified and used such that it can serve as generalized router. It together with FEG and HCS are architectural services. The constructed SOA is a layer structure formed by application services and a network of architectural services (ArS). It is open how the further concepts results and models of component orientation can be applied in such SOA. Author used the variants of ArS in several successful projects, including soft real-time ones.

Ben Gras
(Vrije Universiteit, Netherlands)

Arun Thomas
(Vrije Universiteit, Netherlands)

MINIX 3 is an open-source multiserver operating system designed for high reliability. Unlike traditional operating systems, where flaws in device drivers and system components can crash the entire operating system, MINIX 3 can transparently recover from many such failures. In this talk, we will describe our ongoing research into OS dependability. Additionally, we will outline our efforts to turn MINIX 3 into a mainstream embedded operating system and provide a (rough) roadmap for the future.

Wolfram Hardt
(TU Chemnitz, Germany)

D3S Systems Group

Jiri Barnat
(FI MUNI)

With the increase in complexity and degree of parallelism of computer nsystems, it became critical to develop automated formal verification nmethods for ensuring their quality. Unfortunately, those methods are ncomputationally demanding and memory-intensive in general, hence, their napplicability to large and complex systems routinely seen in practice nthese days is limited. To verify large systems no option was left out than nto employ combined computing power of multiple computing devices. In this ntalk we will exemplify steps that must have been taken to build nhigh-prefomance scalable tool for parallel and distributed LTL model nchecking.

D3S Formal Group

D3S Component Group

The talk will overview the basic concepts of DEECo, which is a currently being developed component model for ubiquitos components with emergent connections. Subsequently, the seminar will have a form of brainstorming, the aim of which is to concretize D3S tasks within ASCENS project.

Marcela Šimková
(VUT Brno)

Functional verification is a widespread technique to check whether a hardware system satisfies a given correctness specification. As the complexity of modern hardware systems rises rapidly, it is a challenging task to find appropriate techniques for acceleration of this process. The presentation is aimed at HAVEN, a freely available open functional verification framework that exploits the field-programmable gate array (FPGA) technology for cycle-accurate acceleration of simulation-based verification runs. HAVEN takes advantage of the inherent parallelism of hardware systems and moves the verified system together with transaction-based interface components of the functional verification environment from software into an FPGA. The presented framework is written in SystemVerilog and complies with the principles of functional verification methodologies (OVM, UVM), assertion-based verification, and also provides adequate debugging visibility, making its application range quite large. Performed experiments confirm the assumption that the achieved acceleration is proportional to the complexity of the verified system, with the peak acceleration ratio being over 1,000.

Norman Feske
(Genode Labs, Dresden)

Today's operating systems try to find a balance between seemingly conflicting goals. Ease of use is traded against security, resource utilization is traded against resource accountability, and system complexity is traded against scalability. For example, SELinux is ill famed as hard to use and consequently remains widely unused. As another example, isolation kernels minimize the complexity of critical system software but at the cost of limiting these solutions to static applications. The Genode OS architecture shows how these apparently inherent conflicts can be solved by operating-system design. By combining a recursive system structure with capability-based security, mandatory access control becomes easy to deploy. At the same time, the trusted computing base can be minimized for each application individually such that the attack surface for security-critical system functions gets reduced by orders of magnitude compared to existing approaches. Furthermore, a concept for trading physical resources among processes allows for dynamic workloads while maintaining quality of service. That is not just theory - the system is ready for demonstration. Norman Feske will briefly present the roots and mission of Genode Labs, the company founded to support and drive the Genode OS technology. The main part of the talk will be focused on the OS architecture, give a glimpse at the implementation via live demonstrations, and outline the future road map.

Henry Bensler
(Corporate Research, Volkswagen, Germany)

The talk will give a short overview of Volkswagen Group Research and an overview of VW involvement in ASCENS project. In particular, it will present: motivation and objectives of the e-mobility case study, design approach and scenario description, model driven requirements, description of service component types, levels of service component ensembles, awarenes requirements, and expected results of project.

Louis Hache

After a brief introduction about Airbus history, organization and way to work, the aim of this talk is to present a tool used for system mixability checking. Additionally, the talk will discuss the usefulnes of task automatisation as well as the problems developers may encounter while working in a company of Airbus size.

Tomáš Poch

Introduction to GoodData.

Vojtěch Horký

Past seminars introduced the idea of capturing and meassuring relative method performance using Stochastic Performance Logic (SPL). This talk will focus on the practical aspects of this technique, namely annotating Java code with "performance assertions". Progress in implementation of a simple performance-testing framework as well as its usability with real-world projects will be reported.

Lukáš Marek

Many dynamic analysis tools for programs written in managed languages such as Java rely on bytecode instrumentation. Tool development is often tedious because of the use of low-level bytecode manipulation libraries. While aspect-oriented programming (AOP) offers high-level abstractions to concisely express certain dynamic analyses, the join point model of mainstream AOP languages such as AspectJ is not well suited for many analysis tasks and the code generated by weavers in support of certain language features incurs high overhead. DiSL is (domain-specific language for instrumentation) a new language especially designed for dynamic program analysis. DiSL offers an open join point model where any region of bytecodes can be a shadow, synthetic local variables for efficient data passing, efficient access to comprehensive static and dynamic context information, and weave-time execution of user-defined static analysis code.

Peter Libič

A report on progress (or lack of progress) in the topic of garbage collection modelling. Overview of problems and my attempts for solutions. Discussion on possible usage scenarios.

Pavel Jančík

Debugger with novel functions.

Jiří Barnat
(FI MUNI)

The aim of the talk is to present and summarize resent results in GPU acceleration of formal verification procedures, explicit state model checking in particular. The talk will briefly recapitulate explicit state model checking workflow and will identify what steps can be and what steps cannot be accelerated. The talk will focus on adaptation of parallel model checking algorithms and on usage of multiple GPU cards for handling a single verification taks.

Michal Kit

The talk will present a preliminary experience with the AGLOBE middleware. In addition to the overview of the API also the code samples will be presented.

Michal Malohlava

Report on dissertation thesis

Sebastian Bauer
(LMU, Germany)

My talk is about recent results of our ongoing effort to develop a unified framework for compositional specification of component-based systems. In particular, I will focus on the relation between specifications of component behaviors and contracts providing means to specify assumptions on environments as well as component guarantees. A contract framework can be built in a generic way on top of any specification theory which supports composition and specification refinement. Our contract framework lifts refinement to the level of contracts and proposes a notion of contract composition on the basis of dominating contracts. Contract composition satisfies a universal property and can be constructively defined if the underlying specification theory is complete, i.e. if it offers operators for quotienting and conjoining specifications. I will illustrate the generic construction of contracts by moving a specification theory for modal transition systems to contracts and we show that a (previously proposed) trace-based contract theory is an instance of our framework. n

Michal Pěchouček
(FEL, CVUT)

AGLOBE is an agent platform designed for testing experimental scenarios featuring agents position and communication inaccessibility, but it can be also used without these extended functions. The platform provides functions for the residing agents, such as communication infrastructure, store, directory services, migration function, deploy service, etc. Communication in AGLOBE is very fast and the platform is relatively lightweight. AGLOBE is suitable for real-world simulations including both static (e.g. towns, ports, etc.) and mobile units (e.g. vehicles). AgentFly is a multi-agent system enabling large-scale simulation of civilian and unmanned air traffic. The system integrates advanced flight path planning, decentralized collision avoidance with highly detailed models of the airplanes and the environment. All aerial vehicles in AgentFly are modeled by autonomous software agents. Each vehicle/agent is responsible for its own flight operation. The high-level mission of each vehicle is specified by an arbitrary number of waypoints. The operation is tentatively planned before take-off without consideration of possible collisions with other flying objects. During the flight, the agents detect mutual future conflicts in their flight plans and engage in peer-to-peer negotiation aimed at sophisticated re-planning in order to avoid the conflicts and maintain collision-free trajectories.

Ondřej Šerý

During model checking of software against various specifications,nit is often the case that the same parts of the program have to be modeled/verified multiple times. To reduce the overall verification effort, this paper proposes a new technique that extracts function summaries after the initial successful verification run, and then uses them for more efficient subsequent analysis of the other specifications. Function summaries are computed as over-approximations using Craig interpolation, a mechanism which is well-known to preserve the most relevant information, and thus tend to be a good substitute for the functions that were examined in the previous verification runs. In our summarization-based verification approach, the spurious behaviors introduced as a side effect of the over-approximation, are ruled out automatically by means of the counter-example guided refinement of the function summaries. We implemented interpolation-based summarization in our FunFrog tool, and compared it with several state-of-the-art software model checking tools. Our experiments demonstrate the feasibility of the new technique and confirm its advantages on the large programs.n

Jaroslav Keznikl

The draft of the Service Component Ensemble Language as it is being prepared in ASCENS will be presented and feedback on the applicability will be gathered.

Andrej Podzimek

This reading seminar will describe a new concurrent binary search tree algorithm based on AVL trees, developed and benchmarked at Stanford University by Nathan G. Bronson et al. (http://github.com/nbronson/snaptree). Since the algorithm has been implemented in the Java environment (depending on garbage collection and specific features of the Java memory model), making it applicable in operating system kernels would require a more general variant based around the RCU mechanism. Combining our RCU mechanism for UTS (the Solaris kernel) with the presented algorithm by Bronson et al. might improve concurrency of UTS kernel algorithms that use AVL trees.

Michal Kit

In this talk, Michal Kit will describe his previous projects (master thesis, ...).

Stephan Reiter
(LMU, Germany)

Cloud computing is a model that enables access to data and services from all kinds of devices over the Internet. Inherent in the continually growing use of products such as groupware, cloud storage and infrastructure as a service, is a trend towards centralization of computing resources, yielding potentially widespread disruption in case of failures at a provider. Just recently, Research in Motion had to acknowledge that a defect in its internal network resulted in an outage of the Blackberry e-mail service, affecting millions of customers around the globe. In the ASCENS project we focus on building systems on top of autonomous components. As part of a case study we pursue the implementation of cloud computing on top of a peer-to-peer network, utilizing the resources of connected computers in a decentralized manner. Availability of services, smart scheduling of tasks and easy participation are in the focus of our research. In this talk we will discuss these and other goals for our Science Cloud, present use cases and give an introduction to the technology that we will use to implement the cloud.

Vlastimil Babka

The talk will summarize two selected papers from the recent EPEW 2011 workshop, related to I/O and memory allocation profiling, and also present our own paper from the workshop - Can Linear Approximation Improve Performance Prediction ?

Lubomír Bulej, Tomáš Bureš, Jaroslav Keznikl, Alena Koubková, Andrej Podzimek, and Petr Tůma

Compared to functional unit testing, automated performance testing is difficult, partially because correctness criteria are more difficult to express for performance than for functionality. Where existing approaches rely on absolute bounds on the execution time, we aim to express assertions on code performance in relative, hardware-independent terms. To this end, we introduce Stochastic Performance Logic (SPL), which allows making statements about relative method performance. Since SPL interpretation is based on statistical tests applied to performance measurements, it allows (for a special class of formulas) calculating the minimum probability at which a particular SPL formula holds. We prove basic properties of the logic and present an algorithm for SAT-solver-guided evaluation of SPL formulas, which allows optimizing the number of performance measurements that need to be made. Finally, we propose integration of SPL formulas with Java code using higher-level performance annotations, for performance testing and documentation purposes.

Lubomír Bulej, Tomáš Bureš, Jaroslav Keznikl, Alena Koubková, Andrej Podzimek, and Petr Tůma

Compared to functional unit testing, automated performance testing is difficult, partially because correctness criteria are more difficult to express for performance than for functionality. Where existing approaches rely on absolute bounds on the execution time, we aim to express assertions on code performance in relative, hardware-independent terms. To this end, we introduce Stochastic Performance Logic (SPL), which allows making statements about relative method performance. Since SPL interpretation is based on statistical tests applied to performance measurements, it allows (for a special class of formulas) calculating the minimum probability at which a particular SPL formula holds. We prove basic properties of the logic and present an algorithm for SAT-solver-guided evaluation of SPL formulas, which allows optimizing the number of performance measurements that need to be made. Finally, we propose integration of SPL formulas with Java code using higher-level performance annotations, for performance testing and documentation purposes.

Iris Breddin
(RELATE Candidate)

In this talk, Iris Breddin will describe her work on supervised learning in AI with focus on mathematical algorithmic problems and the design of a wireless network protocol that uses minimum power and storage.

Vlastimil Babka

Petr Tůma

The memory subsystems of contemporary computer architectures are increasingly complex { in fact, so much so that it becomes difficult to estimate the performance impact of many coding constructs, and some long known coding patterns are even discovered to be principally wrong. In contrast, many researchers still reason about algorithmic complexity in simple terms, where memory operations are sequential and of equal cost. The goal of this talk is to give an overview of some memory subsystem features that violate this assumption signifcantly, with the ambition to motivate development of algorithms tailored to contemporary computer architectures.

Martin Děcký

Summary of recent achievements and improvements in HelenOS (Google Summer of Code projects, theses, software projects, etc.) and research outlook.

Viliam Simko

This seminar summarizes our paper presented at FACS 2011 symposium. We have presented a semi-automated method that helps iteratively write use-cases in natural language and verify consistency of behavior encoded within them. In particular, this is beneficial when the use-cases are created simultaneously by multiple developers. The proposed method allows verifying the consistency of textual use-case specification by employing annotations in usecase steps that are transformed into LTL formulae and verified within a formal behavior model. A supporting tool for plain English use-case analysis is currently being enhanced by integrating the verification algorithm proposed in the paper.

David Hauzar

The state-of-the-art tools for a bug discovery in languages used for a web application development, such as PHP, suffer a relatively high false-positive rate and low coverage of real errors; this is caused mainly by an unprecise modeling of dynamic features of such languages and path-insensivity of the tools. In this talk, we will describe our approach to finding security problems inside web applications. It combines path-sensitive static analysis, concrete and symbolic execution, literal analysis, taint analysis and type analysis.

Andrej Podzimek

This talk will give an overview of selected recent benchmarking techniques applicable to distributed computing and storage systems. Early classical benchmarking metrics for database systems (the Wisconsin Benchmark) will be described and compared to recent advances in the area of cloud benchmarking suites.

Roland Weiss
(ABB AG, Ladenburg, Germany)

ABB provides automation systems in the process, manufacturing, and power domain that are in service for a long time, e.g. it is not uncommon to run plants for more than 30 years. This poses several challenges to ABB's software development to maintain these products over their whole lifecylce, i.e. maintenance and evolution? Technologies in the IT area have typically very different lifecycles, e.g. operating systems change significantly within 10 years, and support for 10 year old operating systems is not common. In addition, the downtime of plants (both from an economical and social view point) has to be reduced. This requires runtime mechanism for live updates, redundancy etc. In this talk I want to discuss the challenges we see in software development at ABB, areas for research, and also some solutions that we promote.

Lukáš Marek

The current state of the Ferdinand project focused mainly on middleware measurement and related tasks.

Carlos Canal
(University of Malaga)

Component-based Software Development aims at builiding systems by composition of existing services, possibly developed by third parties. Indeed, a vast number of services are already available. These services are black-box components described by their interfaces. Hence, there is a need for techniques to combine them safely and efficiently. Moreover, components or services are hardly reused as they are, due to interface mismatch and they require customized adaptation to combine them. Our group has been working on Software Adaptation for abou ten years now. One of our recent research lines is to apply our previous results to dynamic system reconfiguration when adaptation is required, ensuring this way adaptation to environmental changes (such as netwrok failures, component upgrading, or availability of new, more suitable components) without stopping the system and by means of transparent substitution, and preserving certain system properties that go further backwards compatibility.

Marcel Paška
(University of West Bohemia, Pilsen)

The talk will present a novel approach to software development, mainly useful for embedded devices. Embedded software is described in a programming language with very high level of abstraction. We first generate a verifiable code from the description and prove that it has certain properties defined by LTL formulae. Then we generate the final C code with the same properties.

Vlastimil Babka

The talk presents initial evaluation of the precision of the cache capacity model introduced at the previous seminar on 23th November. The discussion includes the effects of using different methods to obtain stack profile inputs, factors that could be causing the cases of imprecise prediction, and also an initial comparison with a different published cache model.

Ludovic Henrio
(INRIA, France)

This talk presents a model for distributed components communicating asynchronously using futures – placeholders for results. Our components communicate via asynchronous requests and replies where the requests are enqueued at the target component, and the invoker receives a future. Then, future references can be dispersed among components. When the result is available for a future, it needs to be transmitted to all interested components, as determined by a future update strategy. We present formal semantics of our component model incorporating formalisation of one such future update strategy. We formalise in Isabelle/HOL, a component model comprising notions of hierarchical components, asynchronous communications, and futures. We present the basic constructs and corresponding lemmas related to structure of components. We present formal operational semantics of our components in presence of a future update strategy; proofs showing correctness of our future update strategy are presented. Our work can be considered as a formalisation of ProActive/GCM and shows the correctness of the middleware implementation.

Viliam Šimko

The talk will overview the goals of the ongoing project REPROTOOL, which takes up on Procasor and extends it by explicit use of models and different input/outputs.

Hugo Torres Vieira
(New University of Lisbon)

The development of service-oriented applications, prominently Web-Services, raises several challenges that call for new ideas, specialized models and dedicated analysis techniques. This talk covers some contributions that address such challenges, namely we present a specification model based on a novel notion of conversation, and static analysis techniques that allow to check crucial properties of service-oriented systems --- safety and progress of communication protocols. Our approach addresses systems that involve several simultaneous conversations between multiple parties, including conversations with a dynamic and unpredicted number of participants, scenarios found in real systems and that are out of reach of previous works.

Walter Binder
(USI, Lugano, Switzerland)

Many dynamic analysis tools for the Java Virtual Machine are implemented with low-level bytecode instrumentation techniques. While program manipulation at the bytecode level is very flexible, because the possible bytecode transformations are not restricted, tool development is tedious and error-prone. Specifying dynamic analyses at a higher level using AOP is a promising alternative in order to reduce tool development time and cost. However, general-purpose AOP languages lack some features that are essential for dynamic analyses, such as pointcuts at the level of individual bytecodes and basic blocks of code, primitives for passing data between woven advice in local variables, and support for custom static analysis at weaving time. This talk presents the design of @J (Aspect Tools in Java), an aspect-oriented DSL for dynamic program analysis currently under development at the University of Lugano. @J addresses the aforementioned issues and offers dedicated support for optimizing dynamic analyses on multicores.

Václav Pech
(JetBrains)

An overview of advanced concurrent programming abstractions and concepts (actors, agents, fork/join, dataflow concurrency, continuations) and an introduction to the GPars framework for Groovy.

David Babka

The talk will overview the status and achievements of the master thesis on the dynamic reconfigurations in SOFA 2. The thesis covers the factory pattern as proposed in SOFA 2 and the newer extensions, which allow modelling of dynamic entities.

Jaroslav Keznikl

Reading seminar on methods for formal modeling of software architectures, their evolution and checking of architectural properties.

Viliam Šimko

Report on paper "On the nEffectiveness of Abstraction Identification in nRequirements Engineering". The paper describes a statistical method of automatic identification of abstractions from documents written in natural language. The method computes log-likelihood (LL) value for every word (using English National Corpus), a heuristic function computes score of multi-word terms. This method performs better than the original single-word approach by AbstFinder. To evaluate the method, authors used a book about RFID technology with the book index as a set of abstractions.

Ivica Crnkovic
(MDU, Sweden)

This talk presents needs, challenges and experience of education of Global Software engineering. In particular experiences from a course "Distributed Software Development" will be discussed. DSD course was organizednand performed between the School for Innovation, Design andEngineering at Mälardalen University (MDU), Sweden, the University of Zagreb, Faculty of Electrical Engineering and Computing (FER), Croatia, and partially joined by the University of Paderborn (UPB), Germany. The talk will discuss the challenges in creating a joint DSD course (organizational, distance-related and cultural), the solutions implemented at DSD, lessons learned, and success stories. The talk is based on several papers, latest two accepted on CTGDSD workshop at ICSE 2011.

Pavel Ježek

The talk will overview the Microsoft Azure cloud technology. It will focus on the services provided and it will demonstrate the technology on code examples. The talk will also mention the business model underlying the provisioning of the platform.

David Hauzar

The talk will introduce basic concepts of the specification of concurrent behavior in the next version of C++.

Pavel Jančík

How many JavaScript programs use eval? Do authors of the JavaScript engines, optimizations and static analyzers make correct assumptions about behavior of the JavaScript? How does behavior of the JavaScript differ from other languages?

Tomáš Pop

This seminar refers about emerging trends and technologies that affects the market today or are supposed to affect the market in the near future. This overview will summarize Gartner top 10 technologies, Thoughtworks technology radar and IBM Next Five reports.

Michal Papež

The aim of SOFAnet 2 is to exchange components between SOFAnodes in ansimple and rational way. New high level concepts of Applications andnComponents were introduced. The talk will cover their mapping to SOFAn2 entities, means of distribution and a methodology to keep SOFA 2nrepository clean. A description of prototype implementation and itsncurrent status will be presented and new tools demonstrated.

Jaroslav Tulach
(Oracle, Czech Republic)

API design is something that everyone needs, yet only few have enough experience to do it right. As an original NetBeans architect I went through many phases: from believing that API design is art, to understanding that it is hard. Finally I realized that there are general rules which distinguish good design from bad one. I'll explain some of them in this presentation. However, as humans are attracted by weird creatures, I'll demonstrate that on paradoxes. We'll start with some claims that look silly and then we investigate why they are correct in the world of API design. I hope this is going to be interesting investigation.

Peter Libič

The talk will present progress in the effort on modeling of Java garbage collector performance, discuss the motivation for further study and possible future work on the topic. Also a report from the stay at USI Lugano will be part of the seminar.

Petr Hnětynka

The talk will provide an overview of the features expected to appear in new Java 7 (and possibly Java 8 ...).

Jan Jakubův

Process calculi are used to model concurrent systems with several interacting units called processes. Shape types are a general concept of process types which allows verification of various properties of processes from various calculi. The Poly* system, originally designed by Makholm and Wells, is a type system scheme which can be instantiated to a shape type system for many calculi. The talk starts with a short introduction to concurrent systems, to process calculi, and to process calculi type systems. Then the Poly* system is introduced and Poly* instantiation is demonstrated on simple examples. Finally we show several concrete applications of the Poly* system and its instantiations.

Michal Malohlava

MetaEdit+ is a leading tool in the domain of domain-specific modeling primarily targeting design of graphical modeling languages. It combines an elastic modeling environment with simple but powerful code generation techniques. The objective of the seminar is to show main tool concepts. The talk will demonstrate it on development of a simple graphical language for controlling mixing machine.

Jiří Kašpar
(FIT, CVUT)

In late 1990s, after almost a decade when cluster was a synonym of VMS Cluster, a lot of other commercial cluster solutions appeared. Later the principle of clusters was applied not only to operating systems and applications, but also to storage systems, databases, and virtual machines. As among all of these clusters there are a lot of similarities and differences, we propose cluster taxonomy based on resource sharing level and load balancing capabilities. In second part of the talk we will discuss design patterns of shared everything clusters.

Andrew McVeigh
(Imperial College London)

Extensible applications can be extended and customized by third party developers. This is an increasingly popular style (e.g. NetBeans, Firefox, Eclipse), but experience has shown that these applications are difficult to build, as they require the application creators to predict expected types of extensions in advance. We address this by adding three constructs to an ADL, allowing both reuse and evolution to be captured in the design phase. This fully aligns initial creation and subsequent extension, whilst retaining an architectural focus. We show the applicability to extensible systems where even unplanned extension is catered for. We will also demonstrate our toolset support for the approach, featuring automated structural consistency checking. At the end of the presentation, there will be an opportunity for a hands on tutorial.

Mirco Tribastone
(LMU, Munich)

This talk gives an overview of recent research concerning the use of stochastic process algebras for the quantitative analysis of hardware/software systems. The talk consists of three parts. The first part will introduce some basic notions on the usual discrete-state interpretation of models as continuous-time Markov chains. The second part will discuss deterministic approximations with ordinary differential equations for the analysis of large-scale models defined with the stochastic process algebra PEPA. Finally, the third part will conclude with comparisons against other approaches in the literature and, if time permits, with a discussion of open problems and ongoing research to tackle them.

Milan Češka
(FI, MUNI)

Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this presentation we show how the algorithms for LTL model checking can be redesigned in terms of matrix-vector product in order to accelerate LTL model checking on many-core GPU platforms. Our experiments demonstrate that using the NVIDIA CUDA technology results in a significant speedup of the verification process. However, the CUDA technology is quite often limited to small or middle-sized instances due to space limitations, which is also the case of our CUDA-aware LTL Model Checking solution. We further suggest how to overcome these limitations by employing multiple CUDA devices for acceleration of our fine-grained communication-intensive parallel algorithm for LTL Model Checking.

David Hauzar

A brief overview and summary of several interesting topics presented at The Future of Software Engineering Symposium by Erich Gamma, Joseph Sifakis and Andreas Zeller.

Nikola Beneš
(FI, MUNI)

Modal transition systems is a formalism that allows to describe partial (loose) specifications. The formalism supports stepwise refinement and compositional reasoning; it is thus well suited for design and specification of component-based systems. The aim of the first part of the talk is to introduce the modal transition systems and some of the problems that arise in connection with this formalism. The second part of the talk is devoted to showing some of our original results and is based on two published papers (TCS'09 and ICTAC'09).

Lukáš Marek

Reading seminar about "Modeling Virtual Machine Performance: Challenges and Approaches" and "Modeling Workloads and Devices for IO Load Balancing in Virtualized Environments"

Matthias Hauswirth

Trevis: A Context Tree Visualization & Analysis Framework and its Use for Classifying Performance Failure Reports. See http://sape.inf.usi.ch/publications/softvis10.n

Oldřich Nouza
(Faculty of Nuclear Sciences and Physical Engineering, CTU, Prague)

Model transformations are one of the most discussed topics of the modern software engineering. This paper deals with STRIPS planning as a powerful engine for uniformly automated object oriented model transformations like refactoring, design patterns application, and object normalization.

Tomas Poch

Reachability of a program location in the concurrent program is an undecidable problem. The pattern based verification is a technique deciding the related problem - whether the program location is reachable assuming that the threads are interleaved in a way corresponding to the given pattern. The pattern takes the form w_1* ... w_n* - sequence of words, where each of them can repeat arbitrarily many times. The talk will formulate the task of pattern based verification as a language problem and present the decision procedure in this manner. The talk will also cover the application of the technique in context of parallel processes communicating in the rendez-vous style as well as parallel processes with shared memory, touch the recent complexity results and comment on the ongoing work on the tool implementation.

Rolf Hennicker
(LMU, Germany)

Preservation of compatibility by refinement and preservation of refinement by component composition are crucial requirements for any kind of interface theory. In this talk we discuss several variants of interface theories on the basis of modal I/O-transition systems (MIOs) introduced by Larsen et al. First we present interface theories for MIOs with strong and weak modal refinement and compatibility on the basis of synchronous communication. Then we describe extensions in two directions, to asynchronous communication and towards the integration of changing data states of components. For each case we consider particular compatibility and refinement notions and we show that they work properly together, i.e. form an interface theory.

Ludwig Adam
(LMU, Germany)

The ability to specify and verify time constraints is of great importance in time-critical enterprise applications. In this work we consider Timed I/O-Automata for the specification of component behaviour with time constraints. The synchronized communication of a component with its environment can lead to a violation of specified time constraints. We are therefore interested in two aspects of compatibility: While timed output-compatibility ensures, that output messages of a component are accepted by its environment, timed input-compatibility ensures, that an input requirement of a component is always satisfied by its environment. Current model checkers do not explicitly support these notions of compatibility. We introduce syntactical transformation rules for Timed I/O-Automata that allows us to automatically verify these properties with the model checker UPPAAL.

Andy Georges
(Ghent University, Belgium)

In spite of the widespread adoption of virtualization and consolidation, there exists no consensus with respect to how to benchmark consolidated servers that run multiple guest VMs on the same physical hardware. For example, VMware proposes VMmark which basically computes the geometric mean of normalized throughput values across the VMs; Intel uses vConsolidate which reports a weighted arithmetic average of normalized throughput values. These benchmarking methodologies focus on total system throughput (i.e., across all VMs in the system), and do not take into account per-VM performance. We argue that a benchmarking methodology for consolidated servers should quantify both total system through- put and per-VM performance in order to provide a meaningful and precise performance characterization. We therefore present two performance metrics, Total Normalized Throughput (TNT) to characterize total system performance, and Average Normalized Reduced Throughput (ANRT) to characterize per-VM performance. We compare TNT and ANRT against VMmark using published performance numbers, and report several cases for which the VM- mark score is misleading. This is, VMmark says one platform yields better performance than another, however, TNT and ANRT show that both platforms represent different trade-offs in total system throughput versus per-VM performance. Or, even worse, in a cou- ple cases we observe that VMmark yields opposite conclusions than TNT and ANRT, i.e., VMmark says one system performs better than another one which is contradicted by the TNT/ANRT performance characterization.

Andy Georges
(Ghent University, Belgium)

In (experimental) computer science, a large portion of time should be (but mostly is not) spent on evaluating ideas, refining them, re-evaluate, and finally measure the results of the implemented idea. Computer science papers usually contain an evaluation section -- albeit a fairly limited one at times -- where the authors try to provide evidence that their approach is both valid and improves the state-of-the-art. During the last decade, there has been an increase in awareness that the computer science community is lacking on several aspects of (performance) evaluation. We have made several important contributions to improving the state-of-the-art in this domain, focusing on Java (process-level virtualisation). However, while we need to take the rigour in evaluating our ideas and tools one step further, we feel that many researchers still have not caught up yet. Furthermore, in our opinion, the field as a science urgently needs to wake up and become more scientific in its ways. In this talk we will discuss some of the steps that have been proposed by us and others, and present opportunities for further improving the way we conduct evaluations. These ideas are by no means set in stone; they are meant to provide a lead for further discussion and refinement. Three issues seem to form the crux of the matter: experimental design, benchmarks and measurements. However, all of these issues are intertwined with the motivation people are given to conduct decent experimentation, and here as well a (cultural) change is needed.

Tomáš Potužák
(ZCU, Pilsen)

In the presentation, the Component-based Simulation Framework for Component Testing is described. The simulation framework, which is currently under active development, enables to test extrafunctional properties of real software components in simulated environment. Hence, there is no need for creation of the (potentially incorret) models of the components. The framework itself is constructed from software component in order to ensure modularity of performed simulations.n

Jakub Gemrot

There is an arise of interest in complex virtual worlds, including U.S.Army, therapists, fire fighters. They may be used to for training simulations, medical treatment of psychological illnesses or training rescue missions. These applications demands simulated virtual beings, be it virtual humans or animals, with complex behaviours. Trying to experiment with virtual behaviors means to have a virtual world paired with a tool that enables one to quickly test different approaches for behaviour coding. As far as we know, our tool Pogamut is the only one that is being systematically developed tonenable such experimentation with different behaviour languages. The presentation will be aimed to discuss problems of pairing behaviour language interpreters with virtual worlds showing Pogamut bound together with virtual world of the Unreal Tournament 2004 computer game.

Michal Malohlava

The talks summarizes 1st modeling wizard summer school which took place in Oslo at the end of September. The talk highlights key points of sessions and reports identified challenges in modeling world.

Jiří Kašpar
(FIT, CVUT)

In late nineteen's, after almost a decade when cluster was a synonym of VMS Cluster, a lot of other commercial cluster solutions appeared. Later the principle of clusters was applied not only to operating systems and applications, but also to storage systems, databases, and virtual machines. As among all of these clusters there are a lot of similarities and differences, we propose cluster taxonomy based on resource sharing level and load balancing capabilities. In second part of the talk we will discuss design patterns of shared everything clusters.

Andrej Podzimek

Read-Copy-Update (RCU) is a synchronization mechanism that increases concurrency and improves throughput in SMP (Symmetric Multiprocessing) environments. These improvements are achieved by keeping multiple versions of the protected data, which allows readers and writers to run in parallel. The RCU mechanism is used in virtually all subsystems of the Linux kernel. The talk will present a new and original implementation of RCU for UTS (the kernel used by Solaris, former OpenSolaris, Nexenta and Illumos). The new RCU implementation for UTS has been benchmarked in cooperation with a non-blocking hash table. The benchmark compared the RCU algorithm with a readers-writer lock and with another RCU implemetation called QRCU. More details can be found in Andrej's diploma thesis linked below. The second link refers to the presentation slide show.

Vlastimil Babka

The talk introduces a work-in-progress model for predicting cache misses and performance of workloads running in parallel over a shared cache. The model takes stack distance profiles and several other metrics of the workloads as its input, and can produce an effective stack distance profile of the workloads under sharing. The talk also describes the adopted method for obtaining the required input metrics of an executable workload, and shows preliminary results.

Petr Hnětynka

Jan Kofroň

Rehearsal talk.

Tomáš Bureš

The talk will show basic features of the Alloy specification language and the use of Alloy analyzer for debugging a specification (meta-model).

Zbyněk Šlajchrt
(University of Economics, Prague)

Chaplin ACT is a Java class transformer, which modifies classes in such a way that their instances may form composites at runtime. While Scala and other languages support a static object composition, i.e. a composite has an immutable structure defined at the time of the composite's creation, Chaplin ACT allows creating composites whose internal structures may evolve. A new component may be added to a composite or, conversely, an existing component may be removed from it. Furthermore, after inserting an object to a composite as a new component the object's behavior may change. In this sense, the object plays a certain role in the composite. On the contrary, the presence of a new component in a composite may also influence the behavior of other components. It is analogous to our everyday's experience: anybody who enters a certain context normally adapts his/her behavior to it. Some behavior may be suppressed while other may emerge. The presence itself may also influence the behavior of other people in the current context. We will demonstrate this technology on several examples and show how to incorporate it into our applications. Furthermore, some insights to the project's internals will be given. Chaplin ACT is developed as an open-source project (http://www.iquality.org/chaplin/) in the framework of my doctoral thesis.

Pavel Jančík

The behavior protocols (BP) are typically used to check the correctness of the component composition. Even though component composition is error-free (from the BP point of view) a component system can violate the behavior protocol due to bugs arising from implementation.The talk gives an overview of the way how to check compliance of the primitive component implementation with behavior specification and summarize the experience gained during the work on my master thesis. The overall structure of the checker, extension of the Java PathFinder as well as features of the TBP protocol and their implications for model checking of code will be presented

David Hauzar

Report on a paper by Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies: Local Verification of Global Invariants in Concurrent Programs. Abstract: We describe a practical method for reasoning about realistic concurrent programs. Our method allows global two-state invariants that restrict update of shared state. We provide simple, sufficient conditions for checking those global invariants modularly. The method has been implemented in VCC3 , an automatic, sound, modular verifier for concurrent C programs. VCC has been used to verify functional correctness of tens of thousands of lines of Microsoft’s Hyper-V virtualization platform4 and of SYSGO’s embedded real-time operating system PikeOS.

Martin Děcký

Concluding remarks and comments on the report about the 40th International Summer School in Marktoberdorf, a continuation from 2010-10-16.

Viliam Šimko

The systematic review led to the analysis of 20 primary studies (16 approaches) obtained after a carefully designed procedure for selecting papers published in journals and conferences from 1996 to 2008 and Software Engineering textbooks. A conceptual framework was designed to provide common concepts and terminology and to define a unified transformation process.

Tomáš Pop

This seminar refers about the paper "Industrialization of Research Tools: the ATL Case". The paper describes AtlanMod research team experience with a long term process of a technical transfer of research results to commercial quality tool with large user base.n

Martin Děcký

A brief overview and summary of several interesting topics presented at the 40th International Summer School in Marktoberdorf (Software and Systems Safety: Specification and Verification) by Manfred Broy, Tony Hoare, Ed Brinksma, Carlo Ghezzi, Susanne Graf, John Harrison, Connie Heitmeyer, Holger Hermanns, Kim Larsen, Doron Peled and John Rushby.

Ondřej Šerý

Reading seminar.

Carlo Ghezzi
(Politecnico di Milano, Italy)

Modern software applications are increasingly embedded in an open world that is constantly evolving, because of changes in the requirements, in the environment, and in usage profiles. These changes are difficult to predict and anticipate, and are out of control of the application. In many cases, changes cannot be handled off-line, but require the software to self-react by adapting its behavior dynamically, to continue to ensure the desired quality of service. The big challenge in front of us is how to achieve the necessary degrees of flexibility and dynamism required by software applications without compromising the needed dependability. The talk focuses on quantitative probabilistic requirements. It discusses how the initial design of an application may proceed through a model-driven process towards an implementation that satisfies requirements. Design-time parameters characterizing the environment are intrinsically subject to uncertainty, both because predictions are intrinsically inaccurate and because the environment is likely to change. It is thus necessary to check at run time if these parameters change significantly and may eventually lead to requirements violations. To do so, we need to extend verification to run time, by monitoring the environment, in order to get the real data that characterize it and affect the behavior of the application, and feeding the model (which continues to exist at run time) with new parameters, replacing the outdated values that were used at development time. The updated model can check whether the requirements are still met, or whether a reconfiguration is needed in the application in order to continue to satisfy the requirements. The talk reports on some results of recent research, developed within the SMScom project, funded by the European Commission, Programme IDEAS-ERC, Project 227977 (http://www.erc-smscom.org/). The focus is on modelling, model update, and automatic reasoning on requirements. An initial attempt to support self-adapting reactions will also be outlined.

Jaroslav Keznikl

SOFA 2 is a component system including several innovative concepts as hierarchical components or software connectors. Its current implementation is tightly connected to the Java language which brings many benefits however it makes difficult for fast prototyping. However, the contemporary trends in software engineering leverage prototyping effort by integrating different scripting languages (JavaScript, Python) because of their dynamic nature. The talk gives a brief overview of the current SOFA 2 scripting support implementation and summarises the problems encountered and the experience gained during the work on my master thesis.

Roland Mader
(AVL, Austria)

The CESAR project aims on improving the development process of safety-critical embedded systems. A major goal of CESAR is to provide the reference technology platform (RTP) for embedded systems development. The vision of the RTP is a set of compatible entities that can be used to form tailored, integrated tools chains for embedded systems development. These tools chains follow a model-based integration approach. Among the first tools that have been adapted to the RTP were AVL InMotion and Papyrus for EAST-ADL2. These tools have been combined to create a tool chain that allows tracing between requirements and test cases as well as multi-site and multi-user collaboration.

Petr Hošek

The Scala language continuously gains more and more popularity among programmers thanks to many new concepts it offers. Therefore, it makes perfect sense to take a further insight on this language. Beside the language itself, its ecosystem is also very important. That is why we will focus on the Scala ecosystem in this presentation. First of all, we will take a closer look at Scala compiler. This is being used not only as a compiler, but as an important building block of other tools as well. We will show how the compiler could be easily extended and used as a part of our applications. We will continue by overview of the most important tools and libraries you will use when developing applications in Scala. In the end, we will take a look at the entirely new member of the Scala ecosystem, the Collaborative Scaladoc project. This project has been created within the scope of Google Summer of Code 2010 program and aims to use the collaborative approach for the development of Scala documentation.

Luke Rajlich
(Zynga)

The talk will cover how FarmVille built a massively scalable game service. This talk will cover the technical challenges the team faced in building the service and how to overcome hurdles in scaling a service. Participants will leave with a better understanding of how large scale game services are designed, built, and scaled.

Peter Sweeney
(IBM T. J. Watson Hawthorne)

Summary of the state-of-the-art.

Marta Kwiatkowska
(University of Oxford, UK)

The vast majority of software verification research to date has concentrated on qualitative analysis methods, for example the absence of safety violations in program executions. Many programs, however, contain randomisation, timing and resource information. Quantitative verification is a technique for establishing quantitative properties of a system model, such as the probability of battery power dropping below minimum, the expected time for message delivery and the expected number of messages lost before protocol termination. Tools such as the probabilistic model checker PRISM (www.prismmodelchecker.org) are widely used in several application domains, including security and network protocols, but their application to real software is limited. This lecture presents recent results concerning quantitative software verification for ANSI-C programs extended with random assignment. The goal is to focus on system software that exhibits probabilistic behaviour and properties such as “the maximum probability of file-transfer failure”, or “the maximum expected number of failed transmissions”. We use a quantitative abstraction-refinement framework based on predicate abstraction, in which probabilistic programs are represented as Markov decision processes and their abstractions as stochastic two-player games. These techniques have been implemented and successfully used to verify actual networking software.

Tomáš Pop

Rehearsal talk.

José Luiz Fiadeiro
(University of Leicester, UK)

We report on the work that we developed within the FP6-IST-FET Integrated Project SENSORIA (www.sensoria-ist.eu), which aimed at providing formal support for modelling service-oriented systems in a way that is independent of the languages in which services are programmed and the platforms over which they run. We discuss the semantic primitives that are being provided in the SENSORIA Reference Modelling Language (SRML) for modelling composite services, i.e. services whose business logic involves a number of interactions among more elementary service components as well the invocation of services provided by external parties. This includes a logic for specifying stateful, conversational interactions, a language and semantic model for the orchestration of such interactions, and an algebraic framework supporting service discovery, selection and dynamic assembly. (More information is available at http://www.cs.le.ac.uk/srml/)

Zdeněk Žabokrtský
(UFAL, Charles University)

I will introduce TectoMT, which is a highly modular NLP (Natural Language Processing) software system implemented in Perl programming language under Linux. It is primarily aimed at Machine Translation, making use of the ideas and technology created during the Prague Dependency Treebank project. At the same time, it is also hoped to significantly facilitate and accelerate development of software solutions of many other NLP tasks, especially due to re-usability of the numerous integrated processing modules (such as taggers, parsers, or named-entity recognizers), which are all equipped with uniform object-oriented interfaces.

Radovan Janeček
(CA Inc.)

I will provide brief overview of the IBM Mainframe platform with the emphasis on the latest trends (virtualization, data center consolidation, power/cooling optimization, etc.) that keep this platform still very interesting for CIOs. As the mainframe has become first class citizen of the distributed world (zLinux, J2EE, CICS web services, etc.) the question is whether there are interesting research topics we can together collaborate on. Interactive discussion and joint discoveries are the main purpose of this seminar.

Tomáš Pop

In this semiar will be presented complex performance study of SS7Tracker: application for tracking mobile users in GSM networks build on top of modular architecture. Analysis is based on simulation using statistical distributions extracted from previous system measurements.

Peter Libič

Garbage collectors are integral part of many runtime systems. The seminar consists of two parts: the first is an overview of selection of contemporary garbage collection algorithms, including basic reference counting, tracing andnadvanced algorithms like G1 and concurrent mark and sweep. The secound part presents the basic models and their simple solutions.

Petr Hošek

Overview of the current status of SOFA HI, profile of SOFA 2 targeted at high-integrity real-time embedded applications development. Generic concepts will be presented together with the description of prototype implementation and possible future development directions will be given.n

Václav Remeš

The possibility to migrate components between different computers at application runtime brings along many possibilities, mainly at the field of load-balancing of the system. There are many issues related to component migration, from leading the component into a reconfigurable state till obtaining component state and transfer to a different computer. Discussion of experience gained during the work on master thesis "Migration and load-balancing in distributed hierarchical component systems".

Michal Malohlava

uSOFA represents a new generation of the SOFA component system. The main goal of uSOFA is to describe SOFA concepts with SOFA and hence, to provide highly configurable self-hosted SOFA implementation. uSOFA is based on a simple micro-component model allowing us to capture design as well as runtime concerns of component-based applications. To mitigate the runtime complexity, micro-components can be assembled into two types of model aspects: a component aspect which provides control layer for components and platform aspects focusing on expressing required platform functionality.nThe talk focuses on clarification of these concepts and explains them on an example.

Lukáš Marek

Existing Java profilers mostly use one of two distinct profiling methods, sampling and instrumentation. Sampling is not as informative as instrumentation but the overall overhead can be small. Instrumentation is more informative than sampling, since it intercepts every entrance and exit in the measured code, but the overhead is large. We propose a method that collects profiling information associated with a specific object instance, rather than with a specific code location. Our method, called object instance profiling, can collect contextual information similarly to other instrumentation methods, but can be used more selectively and therefore with lesser overhead.

Kurt Geihs
(Universität Kassel, Germany)

Adaptive applications modify their behaviour at run-time in response to significant changes in their operating context. In particular, ubiquitous computing applications require run-time adaptivity due to the inherently dynamic nature of the computing environment. We discuss the adaptation requirements and constraints of such scenarios. Our proposed solution is based on architectural adaptation and extended context management that integrates dynamic service discovery. This allows the substitution of an application component by an external, dynamically discovered service at run-time, if the utility of the application is increased by the reconfiguration. The development of such adaptive applications is a complex and challenging task. We present a new model-driven development method that supports the design and implementation of adaptive applications. The core of the approach is an architectural variability model that specifies application variants and their dependencies on the operating context. This design-time adaptation model is transformed to a run-time model which is used by the adaptation manager in the middleware to decide about adaptation actions according to a given objective function. Experiences with case studies and open research questions will be discussed at the end of the talk.

Pavel Parízek

Overview of interesting papers from ETAPS 2010.

Ondřej Šerý

Low-level errors related to memory safety (e.g., buffer overflow) are no longer considered to be the most dangerous programing errors. Nowadays, the top ranking programming errors (see, e.g., http://cwe.mitre.org/top25/) are SQL injection (SQLI) and Cross-site scripting (XSS). These errors are especially hard to avoid in the dynamically typed scripting languages, such as PHP, with fast unconstrained evolution and rather poor information sources. This talk is a brief excursion into the topic of static analysis of web applications with special focus on PHP and static string analysis as published by Wassermann and Su.

Tomáš Poch

Continuation of the previous talk considering refinement of TBP supporting unlimited number of threads.n

Viliam Šimko

An automated model-driven approach to generate executable code directly from the textual use-cases written in plain English. The approach is based on earlier JEE generator extends to allows for the use-cases to be prepared in different formats and for generating final code in different programming languages and component frameworks.

Tomáš Poch

Overview of refinement relations as present in formalisms of interface automata, CCS and CSP.nBased on the experience from those formalisms, refinement for the formalism of TBP is proposed.

Martin Děcký

Recently HelenOS version 0.4.2 has been released. This seminar summarizes the achievements of HelenOS after 5 years of active development.

Pavel Ježek

Overview of experience.

Wolfgang Pree
(SRC, University of Salzburg, Austria)

The talk starts with an overview of the various challenges in the construction of reliable, safety-critical embedded systems. One challenge is to overcome the brittle, hardware-dependent timing behavior of existing systems by providing an adequate correct-by-construction method. The Timing Definition Language (TDL) is the result of several years of research of ourgroup in this area. TDL allows the explicit description of timing behavior along with automatic (timing) code generation and formal guarantees of the timing behavior of concurrent activities. TDL also meets real-world requirements known from the automotive and aerospace domains, such as the description of both synchronous and asynchronous activities. We present TDL's core language elements, highlight some concepts for code generation and demonstrate the TDL tool chain.

Tomáš Kalibera

Real-time Java is being considered as a promising platform for real-time and embedded systems of the future. Distinguishing features of Java compared to technologies used today include automatic memory management, integrated support for concurrency or a good supply of libraries with standard APIs. Despite several successful deployments in demonstrator studies based on production and open-source implementations, there are significant open issues that prevent deployment in resource constrained embedded systems and/or safety-critical systems. The talk will focus on automated memory management as a key feature desired for real-time Java systems, which is also the key obstacle for predictability and throughput. The talk will also mention open issues related to the verification of real-time Java systems.

Petr Tůma

Vlastimil Babka

Software performance prediction methods are typically validated by taking an appropriate software system, performing both performance predictions and performance measurements for that system, and comparing the results. The validation includes manual actions, which makes it feasible for a small number of systems only. To significantly increase the number of systems on which software performance prediction methods can be validated, and thus improve the validation, we propose an approach where the systems are generated together with their models and the validation runs without manual intervention. The approach is described in detail and initial results demonstrating both its benefits and its issues are presented.

Tomáš Černý
(FEL, ČVUT)

The Model Driven Development (MDD) has provided a new way of engineering today’s rapidly changing requirements into the implementation. However, the development of user interface (UI) part of an application has not benefit much from MDD although today’s UIs are complex software components and they play an essential role in the usability of an application. As one of the most common UI examples consider view forms that are used for collecting data from the user. View forms are usually generated with a lot of manual efforts after the implementation. For example, in case of Java 2 Enterprise Edition (Java EE) web applications, developers create all view forms manually by referring to entity beans to determine the content of forms, but such manual creation is pretty tedious and certainly very much error-prone and makes the system maintenance difficult. One promise in MDD is that we can generate code from UML models. Existing design models in MDD, however, cannot provide all class attributes that are required to generate the practical code of UI fragments. In this paper, we propose a UML profile for view form generation as an extension of the object relational mapping (ORM) profile. A profile form of hibernate validator is also introduced to implement the practical view form generation that includes an user input validation.

Stephan Tobies
(European Microsoft Innovation Center, Germany)

VCC is an industrial-strength verification suite for the formal verification of concurrent, system-level C code. VCC's development is driven by two major verification initiatives in the Verisoft XT project: the Microsoft Hyper-V Hypervisor and SYSGO's PikeOS micro kernel. The talk will give a brief overview on the Hypervisor with a special focus on verification related challenges that this kind of highly optimized, concurrent, system-level software poses. It will discuss how the design of VCC addresses these challenges, and will highlight some specific issues of the Hypervisor verification and how they can be solved with VCC.

Holger Giese
(Hasso Plattner Institut, University of Potsdam, Germany)

While software is an immaterial object that does not decay with time, Parnas pointed out that it is in fact aging. Lehman's laws of software evolution accordingly states that a system that is being used undergoes continuing adaption or degrades in effectiveness. Consequently, we can observe that the ability to cost-effectively adapt software has become one of the most important critical success factors for software development today.<br>One particular vision to address this challenge is self-adaptive software that incorporates the capability to adjust itself to the changing needs into the software itself. This capability promises at first to considerably reduce the costs for required administration and maintenance and to avoid a decline in quality. In addition, future generation of software systems that interconnect the today more or less decoupled applications into complex, evolving software landscapes will require the capability to adapt itself as an important cornerstone as the software as whole can no longer be engineered at development time.<br>In this talk we want review why we should look for means to engineer self-adaptive software systematically and what requirements have to be fulfilled to achieve the systematic software engineering of self-adaptive systems. Then, we will look into the particular role of models for engineering self-adaptive systems and discuss the current vision for the model-driven software engineering of self-adaptive systems. Besides the means to build self-adaptive systems with models, we will also review the role of models for the validation and verification of such systems.

Colin Atkinson
(University of Mannheim, Germany)

Although they differ in how they decompose and conceptualize software systems, one thing that all advanced software engineering paradigms such as SOA, MDD and CBD have in common is that they increase the number of different views involved in visualizing a system. Managing these different views can be challenging even when a paradigm is used independently, but when they are used together the number of views and inter-dependencies quickly becomes overwhelming. In this talk Colin Atkinson will present a novel approach for organizing and generating the different views used in advanced component-based development methods referred to as Orthographic Software Modeling (OSM). This provides a simple metaphor for integrating different development paradigms and for leveraging domain specific languages in software engineering. Development environments that support OSM essentially raise the level of abstraction at which developers interact with their tools by hiding the idiosyncrasies of specific editors, storage choices and artifact organization policies. The overall benefit is to simplify the development, evolution and maintenance of component -based systems.

Florian Matthes
(Technische Universität München)

Application landscapes in large enterprises consist of hundreds or thousands of highly connected semi-autonomous application systems which are designed, created, evolved, maintained, used and financed by people with diverse interests and sometimes incompatible educational background. We report on recent efforts in academia and industry to improve the long-term and strategic management of this core enterprise asset by improving the communication between these stakeholders. A key challenge is to develop models, visualizations, tools and management practices which simultaneously address social, technical and economic aspects in a balanced and pragmatic manner based on sound software, service and data modeling principles.

Frédéric Loiret
(INRIA, France)

As embedded systems must constantly integrate new functionalities, their developement cycles must be based on high-level abstractions, making the software design more flexible. CBSE provides an approach to these new requirements. However, low-level services provided by operating systems are an integral part of embedded applications, furthermore deployed on resource-limited devices. Therefore, the expected benefits of CBSE must not impact on the constraints imposed by the targeted domain, such as memory footprint, energy consumption, and execution time. In this talk, we will present the componentization of a legacy industry-established Real-Time Operating System, and how component-based applications are built on top of it. We use the Think framework that allows to produce flexible systems while paying for flexibility only where desired. Performed experimentions show that the induced overhead is negligeable.

Séverine Sentilles
(MDU, Sweden)

Emphasis on component development & component reuse, Seamless integration of analysis techniques.

Jan Carlson
(MDU, Sweden)

A component model for “distributed control-intensive embedded systems”. Reuse, predictability, early model-based analysis. Rich design-time component notion including models, attributes, realization, analysis results, etc. Two layers: ProSys: Active subsystems, message passing. ProSave: Passive components, trigger/data flow.

Lubomír Bulej

Overview and status report.

Lukáš Marek

Overview of the diploma thesis.

Petr Hošek

General overview.

Vlastimil Babka

The talk summarizes two selected papers from the ICPADS 2009 conference, related to performance prediction and cache sharing, and outlines the keynotes.

Peter Libič

Summary report.

Alexey Khoroshilov
(Linux Verification Center, ISPRAS)

The talk covers the main activities of the Linux Verification Center of ISPRAS (LinuxTesting.org): (i) Model-based (formal specification based) test suite OLVER covering more than 1500 interfaces of the Linux Standard Base Core, (ii) LSB Infrastructure Program, which is a joint effort of the ISPRAS and the Linux Foundation, and (iii) Linux Driver Verification Program aimed to develop domain specific automatic verification toolset for Linux device drivers. The latter program is discussed in details including the specifics of the domain (Linux device drivers), and their consequences for verification tools, repository of domain specific rules to be verified, our experience with BLAST and other approaches, and first results and future plans.

Ondřej Šerý

Thesis progress report

Laurent Mounier
(VERIMAG, France)

Runtime-verification and runtime-enforcement are lightweight and effective software validation techniques that do not require complete and accurate formal models of the system under consideration. Thus, they can be easily applied for service oriented applications, where components can be dynamically updated, or available only as binary code. In this presentation we will discuss the expressive power of these techniques in the framework of the safety/progress classification of linear temporal properties. We will give an efficient procedure to generate a validation or enforcement monitor from a given property, and we will discuss some practical implementation issues trough our prototype tool called j-VETO (for Java Validation end Enforcement Tool).

SOFA team

Current status report.

Juan Ángel Lorenzo
(University of Santiago de Compostela)

General overview.

Martin Děcký

Status update on the progress of formal description of the architecture and behavior of HelenOS. General approach, the use of ADL and BP, challenges and open questions.n

Michal Malohlava

Domain modeling and engineering is currently massively adopted approach. Different types of domain-specific languages (DSL) as well as frameworks for deriving such DSLs are introduced. However, in the domain of component-based systems pure domain-specific component models do not exist. This talk present an approach proposed by Kung-Kiu Lau and Faris M. Taweel to derive domain-specific component models for a given domain.

Patricia López
(University of Cantabria)

General overview.

Jaroslav Bauml
(University of West Bohemia in Pilsen)

The existing consistency controls in component systems at build time or in runtime cannot prevent type mismatch failures caused by independent client and server bundle development. Our solution to this problem use automated versioning of components. Version identifiers are generated from results of subtype-based comparison of component representations, thus achieving a consistent and formally backed interpretation of thenversion numbering scheme.

Kamil Ježek
(University of West Bohemia in Pilsen)

Components interchangeability checks will fail if extra-functional properties are not resolved properly. Although a lot of work towards an extra-functional properties description has been done, a solution targeting their context independence has not been proposed yet. We have been working on a model hiding direct values of the properties which allows us to deploy components in a set of contexts without destroying scales of values. We propose a novelty system of registries which encapsulates direct (context dependent) values in each registry prepared for each context. A component's properties descriptor consequently uses only abstract names of values which are linked to registries.

Pavel Parízek

Checking Programs for Real-Time and Embedded Systems

Jan Kofroň

Overview of the current state of the Q-ImPrESS project will be presented; the focus will be set on the current state of the tools, on the outlook to the nearest future, and identification of actions to be performed to prepare the Q-ImPrESS tools for annual review. Please note that the presentation will be quite technical and insight into the project technologies is a prerequisite for understanding the talk.

Tomáš Bureš

Language introduction.

Tomáš Černý
(FEL, ČVUT)

Web debugging proxy overview.

Barbora Bühnová [Zimmerová]
(FI MUNI)

Performance evaluation of (component-based) system models is highly dependent on the level of detail used for building the models. This talk focuses on one particular construct, which is not getting much attention in existing performance models - the context and history-dependent internal state of the system (or its components). In the talk, we define the state, design a classification of possible state types, and discuss the performance impact of the state types, together with the implied increase of the model size.

Lucia Kapová
(Universität Karlsruhe)

Model-driven performance prediction methods require abstract design models to evaluate the performance of the target system during early development stages. Developing such abstract models including important implementation details should not incur additional effort for performance engineers. The talk focuses on performance completions which hide low-level details from performance engineers and introduces their automatical integration using model-driven technologies.

Laurent Mounier
(Verimag, France)

Michal Malohlava

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.

Vaclav Rajlich
(Wayne State University, USA)

Tomach Poch, Frantisek Plasil

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.

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.

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

Durga Prasana Sahoo

Peter Libic

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.

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.

Michal Malohlava

Pavel Parizek

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

Michal Bečka

Martin Decky, Pavel Jezek

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.

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.

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.

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.

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. [http://research.microsoft.com/en-us/projects/chess/default.aspx]

Vlastimil Babka

Pavel Parizek, Tomas Poch

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,nwhile 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.

Pavel Parizek, Tomas Poch

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.

Viliam Šimko

Mini-workshop - ADAM Team, Lille, France

Mini-workshop - ADAM Team, Lille, France

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.

Tomas Bures, Michal Malohlava, Petr Hnetynka

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

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

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.

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.

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

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

Pavel Ježek

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.

Tomas Poch

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.

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

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.

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.

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.

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.

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.

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.

Petr Tuma

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.

Tomáš Pitner
(Masaryk University, Brno)

Web 2.0 represents the recent evolutionary shift towards morenuser-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.n

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.

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.

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

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.

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.

Pavel Parízek

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

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.

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.

Juan Ángel Lorenzo

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

Vladimír Mencl
(Canterbury Christ Church University)

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.

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

MIXER

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)

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.

Pavel Ježek

Jiří Adámek

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

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.

Awais Rashid?

Pavel Parízek

Jaroslav Svacina?

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.

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

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.

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.

Michal Malohlava

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.

Pavel Parízek

František Plášil

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.

Petr Hnětynka

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.

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.

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

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.

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.

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.

Dominik Hurnaus
(Johannes Kepler Universität Linz)

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

Samuel Kounev
(University of Cambridge)

Marek Procházka
(Space Sytems and Applications)

Tomáš Bureš

Petr Hnětynka

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="http://research.microsoft.com/~leino/">http://research.microsoft.com/~leino/</a>

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.

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.

Free slot

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.

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 www.minix3.org.

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.

Frantisek Plasil

Ondřej Šerý

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.

Petr Hnětynka

Antonino Sabetta
(ISTI CNR, Pisa)

Michael Kuperberg
(Universität Karlsruhe)

Klaus Krogmann
(Universität Karlsruhe)

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

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.

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.

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.

Jaroslav Gergic

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.

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

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.

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.