Fall Days 2014
Hotel de Leijhof, Oisterwijk,
November 5-7, 2014
The IPA Fall Days are an annual multi-day event, focussing on several topics of interest to the broader research community of IPA. This year’s Fall Days are dedicated to topics on Testing (6 November) and Algorithms (7 November).
Registration
Registration closed on 21 October (upon serious request of the hotel); this is in contrast to the previously announced registration deadline of 24 October.
As always, IPA PhD students can attend for free. For others, details on pricing is made available upon request.
To make maximal use of the available capacity, we process applications on the following basis: Registrations are treated “first come, first serve”. All PhD students (IPA and non-IPA) have to share a room. Others may also be asked to share if we run out of rooms.
Programme
Wednesday 5 November is reserved for the IPA PhD workshop. The workshop aims to promote the interaction and cohesion with PhD students from other universities on both a social and technical level, provide a hospitable setting in which presentation skills can be demonstrated and improved through constructive feedback by peers, and be fun.
The invited speaker of the PhD Workshop is Mark Timmer, winner of the award for the best IPA Dissertation of 2013.
The programme for the PhD Workshop and the programme for 6 and 7 November can be found below. When available, the abstract of a presentation is revealed by clicking on the title of the presentation. The slides for some of these presentations can be found here.
WEDNESDAY 5 NOVEMBER: PHD WORKSHOP
| 11:30-12:00 | Registration |
| 12:00-13:25 | Lunch |
| 13:25-13:30 | Opening PhD Workshop |
| 13:30-14:00 | Marcus Gerhold, UT, The BEAT project: BEtter testing with gAme Theory Testing is naturally phrased as a game, where the tester tries to find faults, playing against the system-under-test. The goal of the BEAT project is to improve test effectiveness and efficiency by using mathematical game theory, yielding higher system quality at lower costs. |
| 14:00-14:30 | Dan Zhang, TU/e Towards Verified Java Code Generation from Concurrent State machines We present work in progress on, verified, transformation of a modeling language based on communicating concurrent state machines, SLCO, to Java. Some concurrency related challenges, related to atomicity and non-standard fairness issues, are pointed out. We discuss solutions based on Java synchronization concepts. |
| 14:30-14:45 | Coffee |
| 14:45-15:15 | Enno Ruijters, UT The state of the art in Fault Tree modeling and analysis Fault Tree Analysis is a prominent method to analyze the risks related to economically and safety critical assets, such as power plants, airplanes, and data centers. Since the 1960s, a wide variety of modeling and analysis techniques have been developed. This talk offers a brief introduction to fault trees and how they are analyzed, and discusses benefits, drawbacks, and analysis methods of modern extensions such as dynamic FTs, repairable FTs, and extended FTs. |
| 15:15-15:45 | Rajesh Kumar, UT Quantitative Analysis of Socio-Technical Models TBA |
| 15:45-16:15 | João Paulo Pizani Flor, UU An Embedded Hardware Description Language using Dependent Types Formal verification of hardware circuits is growing in prominence, with the accelerating rise in circuit complexity and strict correctness requirements. The use of automated theorem provers based in dependent type theory is a relatively recent phenomenon and shows very promising results when applied to software verification. Therefore, we aim to investigate what benefits can be brought by a Domain-Specific Language (DSL) for hardware description embedded in a language with dependent types. The developed EDSL (Π-Ware) allows for circuits to be modeled and simulated, and for properties to be proven concerning functional correctness and structure. |
| 16:15-16:30 | Coffee |
| 16:30-17:30 | Mark Timmer, UT Efficient Modelling, Generation and Analysis of Markov Automata Quantitative model checking is concerned with the verification of both quantitative and qualitative properties over models incorporating quantitative information. Increases in expressivity of the models involved allow more types of systems to be analysed, but also raise the difficulty of their efficient analysis. Four years ago, the Markov automaton (MA) was introduced as a generalisation of probabilistic automata and interactive Markov chains, supporting nondeterminism, discrete probabilistic choice as well as stochastic timing. However, (1) an efficient formalism for modelling and generating MAs was still lacking, and (2) the omnipresent state space explosion threatened the analysability of these models. In his thesis, Mark Timmer solved the first problem and contributed significantly to the solution of the second. He developed the process-algebraic modelling language MAPA, designed and analysed several syntactic reduction techniques to improve efficiency, and implemented the tool SCOOP to apply these techniques. In this presentation he introduces the basics, the approach, and the results of his work. |
| 17:30-18:30 | Award Ceremony and Drinks |
| 18:30- | Dinner |
THURSDAY 06 NOVEMBER
| 09:00-10:00 | Jan Tretmans, ESI and RU Model-Based Testing for Embedded Systems: Challenges, Theory, and Research Questions High-tech embedded systems increasingly depend on software: software controls, connects, and monitors almost every aspect of modern high-tech system operation. Consequently, overall system quality and reliability are more and more determined by the quality of the embedded software. Systematic testing of software plays an important role in the quest for improved software quality. Model-based testing is one of the promising technologies to meet the challenges imposed on (embedded) software testing.This presentation will first discuss some trends, issues, and challenges in testing high-tech embedded systems. Then the ideas of model-based testing are elaborated. Finally, we discuss to what extent model-based testing can help alleviating the testing issues, and which research questions emanate. |
| 10:00-10:30 | Coffee |
| 10:30-11:15 | Michele Volpato, RU Active automata learning and its application in model-based testing Model-based testing allows the creation of test cases from a model of the system under test. Often, such models are difficult to obtain, or even not available. Automata learning helps in inferring the model of a system by observing its behaviour. The model can be employed for many purposes, such as testing other implementations, regression testing, or model checking. The talk presents the theory behind Angluin’s L* automata learning algorithm and the current research made to adapt it to nondeterministic reactive systems. In particular concepts of ioco theory, a well known model-based testing framework, will be applied, and challenges will be discussed. |
| 11:15-12:00 | Moritz Beller, TUD Modern Code Reviews in Open-Source Projects: Which Problems Do They Fix? Code review is the manual assessment of source code by humans, mainly intended to identify defects and quality problems. Modern Code Review (MCR), a lightweight variant of the code inspections investigated since the 1970s, prevails today both in industry and open-source software (OSS) systems. In this talk, I outline the practical benefits that the MCR process produces on reviewed source code. To that end, I present two case studies that I carried out on two OSS systems each, classifying more than 1,400 review-induced source code changes manually. Surprisingly, results show that the types of changes due to the MCR process in OSS are strikingly similar to those in the industry and academic systems from literature, featuring the similar 75:25 ratio of maintainability-related to functional problems. I also reveal that 7–35% of review comments are discarded and that 10–22% of the changes are not triggered by an explicit review comment. Patterns emerged in the review data; I investigated them to get to know the technical factors that influence the number of changes due to the MCR process. I found that bug-fixing tasks lead to fewer changes and tasks with more altered files and a higher code churn have more changes. Contrary to intuition, the person of the reviewer had no impact on the number of changes. |
| 12:15-13:30 | Lunch |
| 14:00-14:45 | Machiel van der Bijl, Axini Model-based testing, on the difference between theory and practice Axini makes the modeling and model-based test-tool Axini TestManager. We have been developing and using this tool-set for the last seven years. In this talk I will reflect on what we needed to do to make model based testing practically applicable. Furthermore I will reflect on what it takes to make, market and sell a disruptive technology.Machiel van der Bijl, enterpreneur and co-founder of Axini has an MSc and PhD from the University of Twente. Before Axini he worked as an IT-consultant in the Finance and High Tech industry. |
| 14:45-15:30 | Sarmen Keshishzadeh, TU/e Formalizing DSL Semantics for Reasoning and Conformance Testing A Domain Specific Language (DSL) is a language that is tailored for a specific class of problems. Thus a DSL focuses on the essential concepts in a certain problem domain and abstracts from low-level implementation details. In combination with code generators, DSLs bring software development closer to domain requirements. The development of DSLs usually centers around the grammar and a code generator; there is little attention for the semantics of the DSL. However, a formal semantics is essential for reasoning about specifications in terms of the DSL (i.e., DSL instances). We argue that the semantics should be expressed independent of a code generator. Thus semantic issues can be revealed that could otherwise remain undetected. We also use the semantics to define the conformance of an implementation to a DSL instance, and to automatically test conformance of the (generated) implementation code to a DSL instance. We illustrate our approach using an industrial prototype DSL for the healthcare domain. |
| 15:30-16:00 | Coffee |
| 16:00-16:45 | Wishnu Prasetya, UU Scriptable Automated Unit Testing An OO class is usually more challenging for automated testing than traditional procedures. Methods of a class often interact through their instance variables. A test against the class would therefore take the form of a sequence of calls to its methods, aimed at exposing certain interaction. However, generating a good test suite is in general not trivial. Systematically calculating which sequences are needed to trigger certain behavior can be very costly, if at all possible. The strength of an automated testing tool is therefore always limited. We can get much more from the tool by adding a layer of Domain Specific Language (DSL) over it, e.g. to configure it, to post-process the test suites it generates, and even to script such operations. In this talk I will explain some basic concepts in class-level unit testing, and mention some standard techniques. I will show the enhancement of a random-based sequence generator for testing Java classes with a DSL. A random-based testing tool is fast, but it is generally considered as weak. With the DSL we can custom configure it, and significantly improve its delivery. Generated test suites are valuable assets for testers, more than just the verdict they give. The DSL can be used to interactively query suites. The obvious use of queries is to express and verify specifications, but they are also useful to check if we actually have enough witnesses that confirm their validity. In addition to the traditional Hoare triples, I will show how Linear Temporal Logic (LTL) and algebraic properties can be queried. |
| 16:45-17:30 | Alexander Elyasov, UU Inference of Execution Equivalence for Failure Simplification and More Logging of application behaviour is a common practice used in software engineering to support the postmortem analysis of computer applications. There are dozens of techniques developed for mining of various information from application logs. In this work, we propose a log-based inference technique that allows to derive equivalent execution sequences of application events. We present two use cases of such equivalences in testing: 1) to assist in failure simplification, and 2) to be used as testing oracles. In the first use case, we consider how a failing execution trace can be simplified such that it could still be possible to reproduce the original failure. The second use case suggests to utilize equivalent executions as application invariants, i.e. properties universally holding for an application. In the presentation, we will touch some fundamental topics in software testing such as failure simplification by delta debugging and inference of automated oracles. We will also try to reflect some open challenges and problems faced by the researchers in the testing field. |
| 18:00-20:00 | Dinner |
| 20:30- | Social Event |
FRIDAY 07 NOVEMBER
| 09:30-10:15 | Hans Zantema, TU/e and RU Turtle graphics of morphic streams Streams are infinite sequences. The simplest streams that are not ultimately periodic are morphicstreams: fixed points of particular morphisms mapping single symbols to strings of symbols. A most basic way to visualize a stream is by a turtle curve: for every alphabet symbol fix an angle, and then proceed the stream elements by drawing unit segments and turn the corresponding angle.We investigate turtle curves of morphic streams. In particular, criteria are given for turtle curves being finite (consisting of finitely many segments), and for being fractal or self-similar: it contains an upscaled copy of itself.
Based on the latter, we also give a way to generate turtle curves of morphic streams that are space-filling: every grid node or grid edge of the plane (or a half plane or quarter plane) is met exactly once by the curve. |
| 10:15-11:00 | Arie Bos, TU/e Hyperorthogonal Wellfolded Hilbert Curves Recently we developed new space filling curves which go under the adjectives mentioned in the title. We will present a description of these curves together with a construction in arbitrary dimensions, clarified with figures in 2D and 3D. |
| 11:00-11:30 | Coffee |
| 11:30-12:15 | Herman Haverkort, TU/e space-filling curves: applications in computer science TBA |
| 12:15-13:30 | Lunch |