Home Curriculum Vitae Work Blog Stuff



Get Firefox!
Get Thunderbird!
W3C HTML Validator
W3C CSS Validator



BibTex2Html Script moved to GitHub

Written by andreas, 29.12.2013

The code and download files of my popular BibTeX to HTML conversion script were moved from classen.be/bibtex2html to GitHub.

Now everyone can easily fork it or send me fixes as pull requests.

FOSD Workshop

Written by andreas, 19.02.2013

I am programme co-chair of this year's FOSD Workshop, which will take place this October, co-located with GPCE at SPLASH 2013 in Indianapolis, Indiana, USA.

The workshop will feature a keynote by Jo Atlee, lightning talks, tool demos and of course presentations of research papers. Please consider submitting a paper. There is still plenty of time, the deadlines are not even fixed yet.

FOSD 2013 Call for Papers.

Get the call for papers in PDF or as text.

Journal paper in IEEE Trans Software Eng (TSE)

Written by andreas, 16.12.2012

Back in the summer of 2011 we submitted a paper to IEEE Transactions on Software Engineering (TSE). Since this was a regular submission, things went quite slow, but alas, we finally received the acceptance letter! On measures such as impact factor, TSE is consistently ranked as one of the top three Software Engineering journals, so I'm happy.

The paper draws from Chapters 4, 5, 6 and 9 of my dissertation, mainly Chapter 6, which studies the explicit FTS model checking algorithms.

Here is the abstract:

The premise of variability-intensive systems, specifically in software product line engineering, is the ability to produce a large family of different systems efficiently. Many such systems are critical. Thorough quality assurance techniques are thus required. Unfortunately, most quality assurance techniques were not designed with variability in mind. They work for single systems, and are too costly to apply to the whole system family. In this paper, we propose an efficient automata-based approach to LTL model checking of variability-intensive systems.
We build on earlier work in which we proposed Featured Transitions Systems (FTSs), a compact mathematical model for representing the behaviours of a variability-intensive system. FTS model checking algorithms verify all products of a family at once and pinpoint those that are faulty. This paper complements our earlier work, covering important theoretical aspects such as expressiveness and parallel composition as well as more practical things like vacuity detection and our logic feature LTL. Furthermore, we provide an in-depth treatment of the FTS model checking algorithm. Finally, we present SNIP, a new model checker for variability-intensive systems. The benchmarks conducted with SNIP confirm the speedups reported previously.

You can download a preprint here.

Two journal papers in STTT

Written by andreas, 23.09.2012

The current issue (volume 14, number 5) of the International Journal on Software Tools for Technology Transfer (STTT) revolves around software diversity. There are two papers of our research group in this issue.

The first, Model checking software product lines with SNIP, is taken almost literally out of my dissertation. It describes the SNIP model checker, a tool for verifying behavioural models of software product lines. The other one, A code tagging approach to software product line development: An application to satellite communication libraries describes an approach for implementing software product lines, developed with Spacebel a Belgian company producing software for the space industry.

Paper at ICSE'12

Written by andreas, 14.04.2012

Our submission to ICSE 2012 in Zurich was accepted and the CRC submitted. The paper is titled Simulation-Based Abstractions for Software Product-Line Model Checking and looks at the theoretical aspects of simulation and abstraction in FTS. Like our 2010 ICSE paper, the focus of this paper is the theory, and the evaluation is based on an experimental Haskell implementation. There were less submissions than last year (408 vs. 441), 87 of which were accepted (21% acceptance rate). I wonder why they increased the acceptance rate; it's not as if they don't get high quality submissions, but they all need to fit into a three day schedule somehow.

Here is the abstract:

Software Product Line (SPL) engineering is a software engineering paradigm that exploits the commonality between similar software products to reduce life cycle costs and time-to-market. Many SPLs are critical and would benefit from efficient verification through model checking. Model checking SPLs is more difficult than for single systems, since the number of different products is potentially huge. In previous work, we introduced Featured Transition Systems (FTS), a formal, compact representation of SPL behaviour, and provided efficient algorithms to verify FTS. Yet, we still face the state explosion problem, like any model checking-based verification. Model abstraction is the most relevant answer to state explosion. In this paper, we define a novel simulation relation for FTS and provide an algorithm to compute it. We extend well-known simulation preservation properties to FTS and thus lay the theoretical foundations for abstraction-based model checking of SPLs. We evaluate our approach by comparing the cost of FTS-based simulation and abstraction with respect to product-by-product methods. Our results show that FTS are a solid foundation for simulation-based model checking of SPL.

Download the PDF.

New version of BibTeX to Html script

Written by andreas, 11.12.2011

I added a new parameter to the script, which can be used to place a link titled "Abstract" behind an entry in case the abstract of the entry is specified. For the Wordpress plugin, this new feature is enabled automatically. A click on the "Abstract" link will open a popup window with the abstract. If you are not using the Wordpress plugin, you have to provide the script which displays the abstract inside the popup window yourself. I added instructions for how to do so.

As to the Wordpress version, the popup window now also includes a reference to the stylesheet of the current Wordpress theme. The body of the window has class bibtex-display, which can be used to format it appropriately in the stylesheet.

In addition to this, I also removed the dots in the links shown behind an entry (e.g., "pdf.." is now "pdf"); also "more.." became "www".

Btw. all the updates recently were due to feature requests by people using the script. So don't be afraid to ask.

New version of BibTeX to Html script

Written by andreas, 10.11.2011

A new version of the BibTeX to HMTL script is available. I added several new features and fixed some bugs.

Sorting is now parameterised (in fact, I implemented this in may already); you can supply a list of fields by which to sort. I reverted the default sorting order to the order in which the entries are specified in the file. Previously, there was a default sorting by year (if there was no grouping by year already); this has to be specified explicitly now. The sorting order depends on the locale (using uksort with strcoll). It is now also possible to limit the number of author names printed to some integer value; if this number is exceeded, the script prints "et al.".

The Wordpress version was changed to make these settings (and most of the others) available through shortcode parameters (previously, only the grouping values could be set). See here for the list of available parameters.

I also fixed a number of bugs, in particular one in the formatting of author names given as "Secondname, Firstname", and one which caused the sorting to not be done when there was grouping by type. I also noticed that Wordpress messes with the javascript: links; this is fixed now, too.

More info and download here.

PhD Thesis

Written by andreas, 24.10.2011

I defended my PhD Thesis on October 3rd, 2011. The title of my dissertation is "Modelling and Model Checking Variability-Intensive Systems". It describes an approach for model checking in the context of product lines, where each product is specified in terms of its features; that is, a summary of my research on FTS. Both ICSE papers were incorporated into the thesis.

You can get a PDF here.

I have since left the university and I currently work at Intec Software Engineering. The project on product line verification and FTS continues, mainly through the work of Maxime Cordy, who just received a scholarship by the FNRS. The FTS website remains as the point where all results are centralised (it moved to a new location).

SNIP released

Written by andreas, 26.11.2010

As indicated previously, we are developing a model checker for product lines based on FTS. The model checker is called SNIP and was just released.

SNIP packages the (mainly theoretical) results of our ICSE 2010 paper into an efficient model checker for software product lines. SNIP was specifically designed to be usable by third parties, to have an intuitive specification language and a gentle learning curve.

Its specification language is based on the well known Promela language (from SPIN). Variability in the behaviour is specified by guarding statements with features. A guarded statement is only executed in products that contain the features of its guard. When checking properties, SNIP takes these guards and the feature model into account. For this, it uses our TVL feature modelling language.

Given an LTL property, SNIP will determine which products violate the property, which products satisfy it, and so on. SNIP also checks assertions and deadlocks.

More info and download here.

Paper at ICSE'11

Written by andreas, 18.11.2010

Yesterday, we've received word that the paper we submitted to next year's ICSE conference in Hawaii was accepted. The paper is titled Symbolic Model Checking of Software Product Lines and extends the results published at this year's ICSE. Hawaii did attract more submissions than Cape Town, with 441 submissions (vs. 380). The acceptance rate is similar, 14%.

Basically, we show how FTS can be encoded symbolically and give model checking algorithms for CTL over symbolic FTS. We also propose a variant of CTL called feature CTL, or fCTL; which enables to specify formulas that should hold only for certain products of a product line. The paper is more applied than last year's paper as we propose an implementation of these algorithms as part of the NuSMV model checker. Benchmarks conducted on a 256-product elevator example show that the modified version of NuSMV is in average orders-of-magnitude quicker than running standard NuSMV on each product.

Here is the abstract:

We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics.
We recently proposed featured transition systems (FTS), a compact representation for SPL behaviour, and defined algorithms for model checking FTS against linear temporal properties. Although they showed to outperform individual system verifications, they still face a state explosion problem as they enumerate and visit system states one by one.
In this paper, we tackle this latter problem by using symbolic representations of the state space. This lead us to consider computation tree logic (CTL) which is supported by the industry-strength symbolic model checker NuSMV. We first lay the foundations for symbolic SPL model checking by defining a feature-oriented version of CTL and its dedicated algorithms. We then describe an implementation that adapts the NuSMV language and tool infrastructure. Finally, we propose theoretical and empirical evaluations of our results. The benchmarks show that for certain properties, our algorithm is over a hundred times faster than model checking each system with the standard algorithm..

Download the PDF.

  Older ones »




[ copyright © 2015 by Andreas Classen ]   [ Curriculum Vitae ]   [ Work ]   [ Blog ]   [ Stuff