Blog

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.

BibTeX to Html updated

Written by andReas, 16.07.2009

Eric Sommerlade extended the BibTeX to HTML script to include suppot for accents in the correct BibTeX style. Thank you very much, Eric!

At the same time, I also extended the script with a new parameter for the list generator which will place a "BibTeX..." link behind each record. This link points to a second script (configurable by the user) which can make use of a new function that extracts a single BibTeX entry based on its key. To see how this looks like, check out my publication list.

Download the script here

Further documentation is included as a comment at the top of the file.

Two papers at SPLC'09

Written by andReas, 28.05.2009

I just returned from ICSE in Vancouver, more on that soon. We will have two papers at the upcoming 13th International Software Product Line Conference (SPLC), to be held in San Franciso in August.

The first one, Formal Modelling of Feature Configuration Workflows, builds on the paper presented in January at VaMoS. Here is the abstract:

In software product line engineering, the configuration process can be a long and complex undertaking that involves many participants. When configuration is supported by feature diagrams, two challenges are to modularise the feature diagram into related chunks, and to schedule them as part of the configuration process. Existing work has only focused on the first of these challenges and, for the rest, assumes that feature diagram modules are configured sequentially. This paper addresses the second challenge. It suggests using YAWL, a state-of-the-art workflow language, to represent the configuration workflow while feature diagrams model the available configuration options. The principal contribution of the paper is a new combined formalism: feature configuration workflows. A formal semantics is provided so as to pave the way for unambiguous tool specification and safer reasoning about of the configuration process. The work is motivated and illustrated through a configuration scenario taken from the space industry.

And the second paper, Relating Requirements and Feature Configurations: A Systematic Approach, looks at ways to configure feature diagrams by taking into account requirements and context properties. Abstract:

A feature model captures various possible configurations of products within a product family. When configuring a product, several features are selected and composed. Selecting features at the program level has a general limitation of not being able to relate the resulting configuration to its requirements. As a result, it is difficult to decide whether a given configuration of features is optimal. An optimal configuration satisfies all stakeholder requirements and quantitative constraints, while ensuring that there is no extraneous feature in it. In relating requirements and feature configurations, we use the description of the problem world context in which the software is designed to operate as the intermediate description between them. The advantage of our approach is that feature selection can be done at the requirements level, and an optimal feature configuration can be generated from the requirements selected. Our approach is illustrated with a real-life problem of configuring a satellite communication software. The use of an existing tool to support our approach is also discussed.

Paper at ICFI'09

Written by andReas, 10.03.2009

We just got news that our paper submitted to the 10th International Conference on Feature Interactions (ICFI 2009) was accepted. The paper was written together with Peter Ebraert and Theo D'Hondt (from the VUB) in the context of the Belspo-funded MoVES project. In the paper, we propose a formal semantics for change-oriented programming (the subject of Peter's Thesis, it's basically an approach to feature-oriented programming), and show how the semantics maps to that of feature diagrams, allowing to reuse a number of algorithms and tools of the feature diagram literature.

We are currently working on the CRC, the abstract reads as follows.

The idea of feature-oriented programming is to map requirements to features, concepts that can be composed to form a software product. Change-oriented programming (ChOP), in which features are seen as sets of changes that can be applied to a base program, has recently been proposed as an approach to FOP. Changes are recorded as the programmer works and can encapsulate any developer action, including the removing of code.

Before changes can be combined to form a product, it has to be verified that there are no harmful interactions between selected changes. There exists, however, no formal model of the current approach that may serve as a reference specification for ChOP implementations. In an effort to fill this gap, we propose a formal model of ChOP, which, as we will show, maps to the well-understood notion of feature diagram. Thanks to this, we can reuse a number of results in feature diagram research and apply them to ChOP.

Going to Vancouver

Written by andReas, 02.02.2009

After a very interesting time at VaMoS'09 we were notified Friday evening that our paper submitted to the NIER track at this years ICSE was accepted, what a nice start to the weekend! Unfortunately, getting home from Seville was not that "nice" after all, with a temperature difference of 20 degrees and hours of delay. Anyway, the title of the paper is "Towards Safer Composition" and it presents our idea of merging at the same time behavioural descriptions of features and variability information into one behavioural description; with that, we hope (1) to verify behavioural properties on an exponential number of feature combinations more efficiently and (2) to provide a "feature-aware" modelling approach for behaviour in SPLs. Here is the abstract (a PDF version will follow once the CRC is ready *edit* here it is).

Determining whether a set of features can be composed, or safe composition, is a hard problem in software product line engineering because the number of feature combinations can be exponential. We argue that synergies between current approaches to safe composition should be exploited and propose a combined approach. At the heart of our proposal is a merge operation that creates a behavioural description for the entire product family from a feature diagram and descriptions of individual feature behaviour. As a result, we intend to verify more efficiently safe composition for an exponential number of feature combinations.

Paper at VaMoS'09

Written by andReas, 05.01.2009

Happy new year!

We have a paper accepted at this year's VaMoS, the workshop on Variability Modelling of Software-intensive Systems, held in Sevilla at the end of January. The paper provides a formal semantics of multi-level staged configuration, originally proposed by Czarnecki, Helsen, and Eisenecker. There was only space for ten pages, the rest went into a technical report (you can find it here), and will be published later this year (I hope). You can download the pdf of the paper here. Here is the abstract:

Multi-level staged configuration (MLSC) of feature diagrams has been proposed as a means to facilitate configuration in software product line engineering. Based on the observation that configuration often is a lengthy undertaking with many participants, MLSC splits it up into different levels that can be assigned to different stakeholders. This makes configuration more scalable to realistic environments. Although its supporting language (cardinality based feature diagrams) received various formal semantics, the MLSC process never received one. Nonetheless, a formal semantics is the primary indicator for precision and unambiguity and an important prerequisite for reliable tool support.

We present a semantics for MLSC that builds on our earlier work on formal feature model semantics to which it adds the concepts of level and configuration path. With the formal semantics, we were able to make the original definition more precise and to reveal some of its subtleties and incompletenesses. We also discovered some important properties that an MLSC process should possess and a configuration tool should guarantee. Our contribution is primarily of a fundamental nature, clarifying central, yet ambiguous, concepts and properties related to MLSC. Thereby, we intend to pave the way for safer, more efficient and more comprehensive automation of configuration tasks.

Updated BibTeX 2 HTML script

Written by andReas, 30.09.2008

I recently updated the BibTeX to HTML script I use to generate my bibliography and which is available for download here. I added several (long overdue) features: proper ordering of entries by year, optional grouping of entries by year and/or type and the possibility to specify the order in which BibTeX types should be listed (as well as their names).

Introducing "Automate"

Written by andReas, 11.09.2008

Evaluating programs written by students is a repetitive and time-consuming task. Too often, this evaluation is done once the development is finished, leaving the students no time to change and enhance their program. At the University of Namur, we developed Automate in an effort to solve this problem. Automate manages student assignments, allows students to submit answers and automatically tests them for correctness. This has several key advantages: students now get immediate feedback on their work, it relieves the supervisor from manually testing each answer (allowing to break up an assignment into small steps, that can each be tested) and it provides the supervisor with a clear overview of the progress of each student.

Automate is actually a re-development of an internal tool that could no longer be maintained. The (french) name was kept for historical reasons. Technically, Automate has a three tier architecture. The front-end is provided by a webinterface written in PHP using the CodeIgniter framework; the middle tier is a threaded Java server that does the actual processing of submissons, and the back-end is provided by a MySQL database.

So that's what I've been working on for the past few weeks (and other weeks scattered through 2008). The tool will see its first use in the first semester of 2009. Even after that, the project will continue to evolve and we are planning on realeasing it under an open source license.

Back from ICSE

Written by andReas, 30.07.2008

This post comes a little late, sorry about that, I have been rather busy lately.

Last May I went to the International Conference on Software Engineering in Leipzig, Germany. I presented a paper at the Problem Frames workshop (IWAAPF) about our approach of formalising problem diagrams with the Event Calculus and how FIFramework (albeit in a somewhat degenerated form) can be used to prove the frame concern automatically.

The workshop was very interesting and the remainder of the conference was the occasion to catch up with research as well as to meet interesting people and colleagues whom I had not seen in a year. In all, ICSE was a very rewarding experience, I hope I make it to Vancouver next year.

Obviously, I also used the occasion to visit the city of Leipzig and brought back some pictures. Unfortunately, the city centre is is full of construction sites. They are building a railway tunnel below the city, causing sporadic construction sites, as well as kilometres of big blue pipes running through the city (which they need to pump ground water out of the underground site). Nevertheless, the city centre is worth a visit, especially the two churches (Nikolai and Thomas), the market place and the "new" town hall. I also walked down to the Völkerschlachtdenkmal, a monument constructed at the end of the 19th century. On my way there I crossed the former trade fair ground with the iconic soviet pavilion now standing in the midst of department stores and car dealerships, how ironic. Unfortunately I did not have the time to scout the whole place for nice locations and walked on rather quickly. On the opposite side of the town lies the Waldstraßenviertel, a whole district of Gründerzeit architecture, definitely a must-see.

I added four new pictures to the header rotation: 34 - a statue of the fountain in front of the Gewandhaus, 35 - the small dome at the entrance of Nikolaikirche, 36 - the Bach monument in front of the Thomaskirche and 37 - a view past the arcade of the chapel at the Südfriedhof.

  Older ones »