Keyvan Nayyeri

Following our weekly meetings to present and discuss ICSE 2010 papers on Software Engineering, a few weeks ago we talked about another paper entitled Model Checking Lots of Systems - Efficient Verification of Temporal Properties in Software Product Lines.

In industrial Software Development you may face with mass production of different derivations of a software system customized for the end user’s needs. From a standpoint, a software system is a set of major and minor features that are included and based on the circumstance, a user may or may not want some of these features. For example, the core functionality and features of Adobe Photoshop are the same (and constant) but you see different editions customized for a specific user’s requirements.

Software systems in industry are developed in families and the difference between family members is in the features. The number of systems developed in this way are growing, and modeling and verification of such systems have become vital tasks. Obviously, it’s arduous to model and verify such systems by hand because as the number of features increases, the number of possible combinations grows exponentially.

A Software Product Line (SPL) is the term that refers to the set of software systems that share a common set of features and Software Product Line Engineering (SPLE) is the engineered knowledge of reusing the features to help the economy of massive production of these software.

In this paper a group of European authors introduce a new approach for model checking the systems produced massively in industry and evaluate their approach with experimental results. First they provide a simple motivation example about a beverage vending machine that at a very high level gets the money, return change, and serves soda. They develop the example to show some other possibilities for the system such as serving tea, cancellation of a purchase, and distributing soda for free.

After describing the problem that is being solved by this paper, the authors discuss the challenges for their work and the contributions that they make, then jump to discussing the base concepts and definitions that they use throughout the paper such as Feature Diagram (FD) and Transition System (TS), Finite Automaton (FA), and Featured Transition System (FTS). Essentially, they model a system using a tuple of different sets that represent the main components appearing in the system. This helps them use mathematical notation to analyze the behavior of the system.

I skip the mathematical discussion as it’s beyond the scope of this blog and hard to explain for my regular readers but the outcome of this modeling (that you can read in the original paper) are some techniques and algorithms to automatically check the systems.

In the end, this foundation is used to implement their method and have an empirical evaluation. The FTS model checking technique is applied to a Haskell interpreter as a functional programming language and is used to check a mine pump controller exemplar, and the results of this experiment are provided to show the effectiveness of this introduced technique.

Based on the discussion that we had, this technique is in early development and has a long way to become mature. This paper (like many other scientific papers) lacks a thorough experimental analysis and the only example provided doesn’t convince the reader of the power and effectiveness of the approach.