Blog

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 2ⁿ 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.

Paper about TVL in Science of Computer Programming

Written by andreas, 22.10.2010

Our submission to the Science of Computer Programming journal published by Elsevier was just accepted. The paper is about TVL, our textual feature modelling language. It presents motivations for a textual language, examines existing languages, presents TVL (with a gentle introduction, as opposed to the rather technical TVL Specification), gives a formal and tool-independent semantics, and presents two evaluations (an industrial and a comparative evaluation). The detail of the industrial evaluation was published by colleagues and presented at the Software Language Engineering Conference recently.

The title of the journal paper is A Text-based Approach to Feature Modelling: Syntax and Semantics of TVL.

Here is the abstract:

In the scientific community, feature models are the de-facto standard for representing variability in software product line engineering. This is different from industrial settings where they appear to be used much less frequently. We and other authors found that in a number of cases, they lack concision, naturalness and expressiveness. This is confirmed by industrial experience.
When modelling variability, an efficient tool for making models intuitive and concise are feature attributes. Yet, the semantics of feature models with attributes is not well understood and most existing notations do not support them at all. Furthermore, the graphical nature of feature models’ syntax also appears to be a barrier to industrial adoption, both psychological and rational. Existing tool support for graphical feature models is lacking or inadequate, and inferior in many regards to tool support for text-based formats.
To overcome these shortcomings, we designed TVL, a text-based feature modelling language. In terms of expressiveness, TVL subsumes most existing dialects. The main goal of designing TVL was to provide engineers with a human-readable language with a rich syntax to make modelling easy and models natural, but also with a formal semantics to avoid ambiguity and allow powerful automations.

The PDF will follow once the CRC is ready.

Upcoming model checker for FTS

Written by andreas, 15.10.2010

There were no news for quite some time. We've been very busy the last months working on a new model checker for FTS. We're quite excited about the tool. It is going to be the first full-fledged FTS-based model checker. The input language is an extension of Promela, it is very intuitive (the temporal logic is LTL, Promela never claims are supported, too). The tool does on-the-fly state space generation and verification, has support for feature diagrams in TVL, does deadlock checking,...

I also forgot to mention that we had a short paper at the ASE conference last month.

BibTeX to Html revised and made into Wordpress plugin

Written by andreas, 01.04.2010

I revised the BibTeX2Html script and also packaged it as a Wordpress plugin. The following changes were made:

• rewrote the code that parses the authors, first names with hyphens are now abbreviated correctly;
• rewrote the code that formats the BibTeX entries, some of the various entry types were not correctly taken into account;
• parts of an entry can now be formatted with CSS (the script now places tags with a special class around key parts of each entry)
• and fixed some parsing problems for BibTeX entries.

The Wordpress plugin is shown in action here. Essentially, the plugin adds a new tag [bibtex]...[/bibtex], which you can use inside a page or a post. The plugin will convert the BibTeX code between any such tags into an Html list.

Model Checking Lots of Systems

Written by andreas, 12.02.2010

We just submitted the CRC of the upcoming ICSE paper, download it here. Here is the abstract:

In product line engineering, systems are developed in families and differences between family members are expressed in terms of features. Formal modelling and verification is an important issue in this context as more and more critical systems are developed this way. Since the number of systems in a family can be exponential in the number of features, two major challenges are the scalable modelling and the efficient verification of system behaviour. Currently, the few attempts to address them fail to recognise the importance of features as a unit of difference, or do not offer means for automated verification.

In this paper, we tackle those challenges at a fundamental level. We first extend transition systems with features in order to describe the combined behaviour of an entire system family. We then define and implement a model checking technique that allows to verify such transition systems against temporal properties. An empirical evaluation shows substantial gains over classical approaches.

More papers and the technical report that accompanies the paper can be found on the FTS webpage.

Paper at ICSE'10 (and several papers at VaMoS'10)

Written by andreas, 17.12.2009

There were no posts for a long time since I've been quite busy (and nothing newsworthy happened), so I am all the more excited to copy/paste the following fresh out of my inbox:

Dear Andreas, Patrick, Pierre-Yves, Axel and Jean-François,

[...] We are pleased to inform you that your paper,

"Model Checking Lots of Systems: Efficient Verification of Temporal
Properties in Software Product Lines"

has been accepted for presentation in the technical program and
for publication in the conference proceedings. The competition
was strong: only 52 of the 380 submissions were accepted, giving
an acceptance rate of 13.7%.

[...]

Sincerely,

Premkumar Devanbu and Sebastian Uchitel
Program Committee Co-Chairs
ICSE 2010

The paper title is rather explicit, all I want to add is that the formalism is called FTS, for Featured Transition System, but I won't elaborate on that know. I'll post the abstract next year, once the CRC is ready.

Our team also had a number of papers accepted at this year's VaMoS workshop (four, to be exact). One of them is about TVL which is a textual variability language, that is, a feature modelling language that uses text (basically, a C-like syntax) to represent feature models rather than graphical diagrams. The idea behind this is that a text-based language scales more easily and is more easily accepted in an industrial setting, mainly because of the wealth of powerful editors out there. The reviews seem to suggest that this issue is rather controversial, so lets hope for some interesting dicussions this January in Linz.

  Older ones »