In this presentation, I will present our active, coevolutionary and multi-objective approach to learning deterministic finite automata from examples, and its application to requirements engineering. Formal requirements specifications are usually produced, from vague user input, by requirements engineers. It is our aim to automate this process.

From user input in the form of positive and negative example behavior of a desired system, we infer automata that completely describe its behavior. The setting of requirements engineering yields specific challenges, like a small amount of input data and the selection of the right automata from the many automata that are consistent with the input data. Furthermore, the number of queries to the user should be as small as possible.

I will show how our approach deals with these challenges and discuss open questions and future work.

Practising my presentation on ICTSS of the paper "n-Complete Test Suites for IOCO"

Omar is a PhD student at the TU/e, applying learning at various companies.

the SUMBAT project (SUperSizing Model-BAsed Testing) will organize a small workshop, presenting first project results.

10:05 Model-Based Testing with TorXakis - Pierre van de Laar (TNO-ESI)

10:30 Model-Based Testing at Oce - Ramon Janssen (RU)

11:10 Model Learning at PANalytical - Jeroen Meijer (UT)

11:35 Model-Based Testing with Complete Test Suites - Petra van den Bos (RU)

Alexis will crash test his presentation for ISoLA conference.

Tanja Vos will present her testing tool Test*.

Paul will wish you a very nice holiday, but before that, he will touch on the key aspect of the determinizer in Tomte, how it actually works in the tool, limitations and discuss a move to a more symbolic framework.

Ramon will practice his talk at CAV about learning TCP with abstraction, and model checking with concretization of the abstract models.

In 1989 Rob van Glabbeek and Peter Weijland defined branching bisimulation as an alternative to weak bisimulation of Robin Milner. Frits Vaandrager and I formulated an algorithm with complexity O(mn) where m is the number of transitions of a labelled transition system and n is the number of states. This was quite a spectacular improvement over weak bisimulation which is cubic due to the transitive tau-closure. At that time there was also the O(mn) algorithm for strong bisimulation, by Kannelakis and Smolka, which was spectacularly improved by Paige and Tarjan to O(mlog n). To me it was open whether the algorithm for branching bisimulation could be improved, until a discussion with Anton Wijs about implementing the algorithms on a GPU, brought me to investigate the paper of Paige and Tarjan in relationship to the branching bisimulation algorithm again. This led to the insight to obtain the current algorithm (except for a small and easily repairable flaw, pointed out by Jansen and Keiren). The algorithm is amazingly complex, but it outperforms existing algorithms by orders of magnitude, especially if systems become large.

A preprint of the paper can be found at http://arxiv.org/abs/1601.01478

Petra will practice her talk for iFM 2016

In this talk, I will extend the basic system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as real values in the interval [0,1]. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. I will present the relationships among these distances, and we provide a full logical characterization of the distances in terms of quantitative versions of LTL and μ-calculus. I will show that, while trace inclusion (resp. equivalence) coincides with simulation (resp. bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic quantitative transition systems. Finally, I will go into algorithms for computing the distances.

(This work dates back to when I was at UC Santa Cruz and is joint work with Luca de Alfaro and Marco Faella)

trial presentation ICT.OPEN

Rick will practice his talk for LATA 2016 about finding minimal separating sequences for all pairs of state in O(n log n).

David will talk about a paper by Jan Friso Groote Anton Wijs: http://arxiv.org/abs/1601.01478

I will report on my research internship.

I will discuss the differences between the various learning algorithms for register automata. This includes the abstract learning algorithm from nominal automata, our tool Tomte and RAlib from Uppsala (and maybe more).

As far as I know, there only exist random test methods to generate test cases from an LTS/IOTS-model. I will discuss an adapted version of the FSM-based Lee and Yannakakis-method to find adaptive distinguishing sequences. These sequences enable a smarter and more directed way of testing.

As part of the Cyber-Physical Systems project in partnership with Océ, my current goal is to use Machine Learning (and other) techniques in order to predict printers failures. I will present here not only the current achievements or Machine Learning techniques employed, but also the main challenges to be completed. My presentation will also trigger a debate on the multidisciplinarity of the project.

I will give a brief overview on our CEGAR based algorithm and detail on how we have extended this algorithm to handle fresh output values. I will also talk on some of the optimizations we've made to the algorithm, and to the tool implementing it. The presentation is going to be a draft version of what I am going to present in Colombia next week.