Bernhard K. Aichernig

Protocol conformance testing a SIP registrar

2011-12-01T10:16:00.001+01:00

In recent years we have successfully applied model-based mutation testing to several implementations of communication protocols. In our work reported in

Bernhard K. Aichernig, Bernhard Peischl, Martin Weiglhofer, and Franz Wotawa. Protocol conformance testing a SIP registrar: an industrial application of formal methods. In Mike Hinchey and Tiziana Margaria, editors, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, London, England, UK, pages 215–226. IEEE Computer Society, 2007. (PDF) (doi:10.1109/SEFM.2007.31)

we tested parts of the Session Initiation Protocol (SIP) used in internet telephony in order to register and connect communication partners.

Our case study targeted a commercial and an open-source (OpenSER) SIP registrar. Furthermore, we compared the mutation approach to a standard model-based test case generation technique. Our mutation technique generated 124 test cases, compared to 6000 test cases generated by the standard approach.

The 6000 tests discovered nine different faults in the commercial SIP registrar and four in the open-source registrar OpenSER.

Interesting was the fact that the comparatively small set of 124 mutation tests uncovered one additional fault in the commercial implementation that was not detected by the 6000 tests of the classical approach.

This is a further indication that mutation testing could play an important role in a mature testing process.

Another important contribution of this paper was to show how our mutation technique could be scaled to larger models. We sliced the models with the help of markers around the injected faults.

Industry Day at QSIC 2012, Xi'an, China

2011-11-15T10:26:00.001+01:00

Photo: bachmont

The 12th International Conference on Quality Software (QSIC 2012) will be held in Xi'an, China, 27 to 28 of August, 2012. The QSIC series of conferences is an established event bringing together people in the area of software and systems quality.

I was happy to learn that Zhou Chaochen (Chinese Academy of Sciences), my former boss at UNU-IIST in Macao, is the General Chair of the event. Zhou Chaochen is the inventor of the Duration Calculus. I joined the UNU faculty in Macao from 2002 to 2006.

For the first time, QSIC is planning an industry day with a dedicated program committee build from practitioners from industry and applied research. I was invited to join this program committee. Wolfgang Grieskamp (Google) and Hongyu Zhang (Tsinghua University) are the Industry Chairs of QSIC 2012.

Paper Submission Due: 23rd April 2012

Further details can be found on the website of QSIC 2012.

P.S: QSIC is an established conference series. I had my first QSIC paper in 2005 and my latest paper at QSIC 2010:

Bernhard K. Aichernig and Percy Antonio Pari Salas. Test case generation by OCL mutation and constraint solving. In Kai-Yuan Cai and Atsushi Ohnishi, editors, QSIC 2OO5, Fifth International Conference on Quality Software, Melbourne, Australia, September 19-21, 2005, pages 64–71. IEEE Computer Society Press, 2005. (PDF) (doi:10.1109/QSIC.2005.63)
Harald Brandl, Martin Weiglhofer, and Bernhard K. Aichernig. Automated conformance verification of hybrid systems. In Proceedings of QSIC 2010: the 10th International Conference on Quality Software, Zhangjiajie, China, July 14-15, 2010. IEEE Computer Society, 2010. Copyright by IEEE. (PDF).

A new EU project started: MBAT

2011-11-04T11:55:00.001+01:00

On November 1st a new EU project started: MBAT - Combined Model-based Analysis & Testing of Embedded Systems.

MBAT is a three-years ARTEMIS joint undertaking project with 41 partners. I am the key researcher and project manager for TU Graz. MBAT combines the latest model-based testing technologies with static analysis techniques leading to a new model-based validation & verification method in the transportation domain (aerospace, automotive, railways).

My team at TU Graz brings in our expertise and tools in model-based mutation testing from the MOGENTES and TRUFAL projects. One aim is to combine model-based mutation testing with structural test case generation approaches. We will also investigate the relation of fault-models to the step-wise refinement in model-driven development.

In model-based mutation testing we inject faults in models of the system under test and automatically generate test sequences that will detect these faults in an implementation. Hence, our tests prevent that the faulty model has been implemented. For details see, e.g., our paper "Efficient mutation killers in action" that can be found in the list of our conference papers. This work describes the case-study of testing a car-alarm system.

In MBAT we will also investigate the current testing practice of our industrial partners and develop a process model where the different testing techniques of MBAT best fit. This will facilitate the adoption of the tools and techniques in industry.

We closely collaborate with the following Austrian project partners: AIT, AVL, and VIF.

Erlang Books

2011-10-17T14:58:00.003+02:00

Recently we started some student projects on distributed programming in Erlang. Erlang is a functional programming language for developing distributed fault-tolerant applications with soft-realtime requirements. Erlang comes with a powerful library supporting common architectural patterns.

The distinguishing feature of Erlang is the combination of the functional paradigm with the actor communication model. Every recursive function can be easily turned into a process that communicates via asynchronous messages with other processes. The only state in an Erlang program is the state of the communication mailboxes. Hence, no variables are shared. Therefore, functions or processes can be safely replaced during runtime.

Furthermore, Erlang comes with its own virtual machine that fully exploits multi-core processors. Erlang demonstrates the advantages of a declarative language when developing distributed applications.
As a starter I recommend the book of Erlang's inventor Joe Armstrong:

For a deeper understanding of Erlang's framework library OTP I recommend:

Have fun with Erlang!

P.S: Erlang is not just fun. Amazon's distributed database web-service SimpleDB is written in Erlang.

My Student Projects for 2011/12

2011-10-05T15:07:00.014+02:00

Creativity without reflection is dangerous!

These are my project proposals for student projects in the academic year 2011/12. Most of the topics can be scaled to small student projects, bachelor thesis projects, master thesis projects and in some cases up to dissertation subjects. The projects are not isolated but fit the current research agenda of my group. The students are supervised in meetings in two-week periods.

MOMUTBUCK - Model-based Mutation Testing of a Controller for a Bucket Arm of a Wheel Loader
Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for a given Java implementation. Especially, the combination of random and mutation testing shall be investigated. This project is related to our completed FP7 MOGENTES project and to the running TRUFAL project.

ERLBUCK - Developing the controller of the bucket arm of a wheel-loader in Erlang (taken)
The aim of this project is to investigate the language features of Erlang and develop a distributed implementation of the controller. A UML model, a Java implementation and test cases exists. The idea is to use test-driven development to develop the distributed solution.

AUTOFAULT - Fault Models in the Automotive Domain
Fault models capture typical faults that occur during the development of software. The task of this project is to analyze typical faults specific to the automotive application domain. The bug history at AVL shall be analyzed regarding common faults specific to the domain and user requirements. In model-based mutation testing, such fault models serve as a basis to develop mutation operators, injecting faults into a model. Then test cases are generated targeting these specific faults. This project is related to our completed FP7 MOGENTES project and to the running TRUFAL project.

ACTIONSAT - Action System to SMT Solver Translation
Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. SMT Solvers are special SAT-Solvers extended with reasoning mechanisms for specific data types. SMT stands for SAT Modulo Theory. The aim is to develop a translator from the specification language of action systems to SMT-Lib, the standard input language for SMT solvers. Such a translation will enable the symbolic analysis of action system models, e.g., for test case generation.

One option is to develop the translator in Prolog
Another option is to use the new programming language Scala (taken)

ACTIONMIN - Action System to Minion Constraint Solver Translation
Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. The Minion Constraint Solver is highly optimized solver for solving constraint satisfaction problems. The aim is to develop a translator from the specification language of action systems to the input language of Minion. Such a translation will enable the symbolic analysis of action system models, e.g., for test case generation

One option is to develop the translator in Prolog
Another option is to use the new programming language Scala

MOMUTSUR - Model-based Mutation Testing Survey
Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to research related work and write a survey on the topic. This includes the study of related literature as well as the evaluation of other existing tools. This project is related to our FP7 MOGENTES project.

ERLTOPDOWN - Systematic Distributed System Development in ERLANG (taken)
The aim of this project is to investigate the systematic top-down development of a sequential system description into a reliable distributed ERLANG application. ERLANG is a functional language for developing highly fault-tolerant distributed systems consisting of thousands of light-weight parallel processes. The student will start with the existing formal method RAISE and map the concepts to ERLANG programming.

CLOUDTCG - Distributed Test Case Generation in the CLOUD
Our group has considerable experience in developing model-based test case generators using mutation analysis. This technique subsumes other test case generation techniques, but is computationally expensive. We face state-space explosion problems known from model checking. One way to cope with this problem is to develop distributed test case generation algorithms. The idea is to use ERLANG as an implementation framework for these algorithms. The student shall develop a first prototype demonstrating the basic distributed architecture of such a new test case generator running in the cloud

DOMFAULTOSS - Domain Specific Fault Models in OSS
Fault models capture typical faults that occur during the development of software. The task of this project is to analyze typical faults specific to a certain application domain. The bug history of open-source software shall be analyzed regarding common faults specific to the domain and user requirements. In model-based mutation testing, such fault models serve as a basis to develop mutation operators, injecting faults into a model. Then test cases are generated targeting these specific faults.

MOMUTCON - Model-based Mutation Testing of the Conference Protocol
Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for the Conference Protocol, a simple multicast chat box protocol. This project is related to our completed FP7 MOGENTES project.

SEMU - Semantic Mutations of UML State Chart Diagrams
Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. In model-based mutation testing a model is mutated by changing its syntax. The mutants represent bugs and test cases are generated to detect such bugs in an implementation. In this project we consider semantic mutations of models, i.e. what are the possible faulty interpretations of a given model. It is well-known that there are several possible interpretations of UML state charts. The student shall investigate the state of the art on this topic and describe the possible semantic variations. This semantic variations will be build into our UML-Action System translator for generating test cases. The idea is to generate test cases that will detect faulty behavior due to semantic misinterpretations. This project is related to our FP7 MOGENTES project.

Student Projects 2011

2011-03-01T14:50:00.000+01:00

Photo: PhillipC

These are my project proposals for student projects in 2011. Most of the topics can be scaled to small student projects, bachelor thesis projects, master thesis projects and in some cases up to dissertation subjects. The projects are not isolated but fit the current research agenda of my group. The students are supervised in weekly meetings.

ERLTOPDOWN - Systematic Distributed System Development in ERLANG
The aim of this project is to investigate the systematic top-down development of a sequential
system description into a reliable distributed ERLANG application. ERLANG is a functional language for developing highly fault-tolerant distributed systems consisting of thousands of light-weight parallel processes. The student will start with the existing formal method RAISE and map the concepts to ERLANG programming.
CLOUDTCG - Distributed Test Case Generation in the CLOUD
Our group has considerable experience in developing model-based test case generators using mutation analysis. This technique subsumes other test case generation techniques, but is computationally expensive. We face state-space explosion problems known from model checking.
One way to cope with this problem is to develop distributed test case generation algorithms.
The idea is to use ERLANG as an implementation framework for these algorithms. The student shall
develop a first prototype demonstrating the basic distributed architecture of such a new test case generator running in the cloud.
ERLSIP Developing a SIP-Server in Erlang
The aim of this project is to investigate the language features of Erlang and develop a server implementing (parts of) the SIP protocol. SIP (Session-Initiation-Protocol) is used in Voice-Over-IP applications. Other protocols, like the conference protocol are possible.
DOMFAULT - Domain Specific Fault Models
Fault models capture typical faults that occur during the development of software. The task of this project is to analyze typical faults specific to a certain application domain. The bug history of open-source software shall be analyzed regarding common faults specific to the domain and user requirements. In model-based mutation testing, such fault models serve as a basis to develop mutation operators, injecting faults into a model. Then test cases are generated targeting these specific faults.
ACTIONSAT - Action System to SMT Solver Translation
Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. SMT Solvers are special SAT-Solvers extend with reasoning mechanisms for specific data types. SMT stands for SAT Modulo Theory. The aim is to develop a translator from the specification language of action systems to SMT-Lib, the standard input language for SMT solvers. Such a translation will enable the symbolic analysis of action system models, e.g., for test case generation.
MOMUTCON - Model-based Mutation Testing of the Conference Protocol: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for the Conference Protocol, a simple multicast chat box protocol. This project is related to our FP7 MOGENTES project.
MOMUTSUR - Model-based Mutation Testing Survey: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to research related work and write a survey on the topic. This includes the study of related literature as well as the evaluation of other existing tools. This project is related to our FP7 MOGENTES project.
SEMU - Semantic Mutations of UML State Chart Diagrams: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. In model-based mutation testing a model is mutated by changing its syntax. The mutants represent bugs and test cases are generated to detect such bugs in an implementation. In this project we consider semantic mutations of models, i.e. what are the possible faulty interpretations of a given model. It is well-known that there are several possible interpretations of UML state charts. The student shall investigate the state of the art on this topic and describe the possible semantic variations. This semantic variations will be build into our UML-Action System translator for generating test cases. The idea is to generate test cases that will detect faulty behavior due to semantic misinterpretations. This project is related to our FP7 MOGENTES project.

COCA - Concolic Execution of Action Systems: Concolic stands for concrete and symbolic execution and is a technique for systematically exploring the paths of a program. Prominent tools that use this technique are jCute and PEX. The aim of this project is to develop a concolic executor for Action Systems. Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. The student will study the problem and develop a prototype for a subset of the language. We currently use Action Systems as input to our model-based testing tools in the FP7 project MOGENTES.

SYMPRO - Symbolic Execution in Prolog: Symbolic execution is a technique we currently use for automated test case generation. In symbolic execution a program is executed with symbolic values. The result of such a symbolic execution is a formula describing all possible outputs dependent on the symbolic inputs. Prolog is well-suited to implement such a symbolic interpreter. The aim of this project is to use the professional prolog system Sicstus to develop a prototype symbolic interpreter for a small programming language. The idea is to exploit the Constraint Solvers of Sicstus Prolog in the style of constraint logic programming.

TAP 2011, Zurich

2010-09-09T11:52:00.007+02:00

Photo: Daniel Gasienica

I have been invited to serve on the Program Committee of TAP 2011, the 5th International Conference on Tests & Proofs, to be held in Zurich, Switzerland, June 30 - July 1, 2011.

The TAP conference is devoted to the convergence of proofs and tests. It combines ideas from both sides for the advancement of software quality.

We had a paper at TAP 2009 on concolic execution of distributed systems (see my conference papers).

To prove the correctness of a program is to demonstrate, through impeccable mathematical techniques, that it has no bugs; to test a program is to run it with the expectation of discovering bugs. The two techniques seem contradictory: if you have proved your program, it's fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on any hope to prove its correctness.

Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using rather different techniques and tools.

And yet the development of both approaches leads to the discovery of common issues and to the realization that each may need the other. The emergence of model checking has been one of the first signs that contradiction may yield to complementarity, but in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer.

The conference will include a mix of invited and submitted presentation, and a generous allocation of panels and informal discussions. All papers will be published in Springer's LNCS series.

ICTAC 2011, Johannesburg

2010-09-08T21:11:00.003+02:00

Photo: Axel Bührmann

I have been invited to serve on the Program Committee of ICTAC 2011 to be held in Johannesburg, South Africa from 31 August to 2 September 2011.
ICTAC 2011 is the 8th International Colloquium on Theoretical Aspects of Computing, the latest in a series founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). ICTAC brings together practitioners and researchers to present their research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development.

SEFM 2011, Montevideo, Uruguay

2010-09-08T20:45:00.005+02:00

Photo: Eduardo Amorim

I have been invited to serve on the Program Committee of SEFM 2011, the 9th IEEE International Conference on Software Engineering and Formal Methods. SEFM 2011 will take place in Montevideo, Uruguay, end of November 2011. The PC-chairs are Gilles Barthe and Gerardo Schneider.
The aim of the conference is to bring together practitioners and researchers from academia, industry and government to advance the state of the art in formal methods, to facilitate their uptake in the software industry and to encourage their integration with practical engineering methods. Papers that combine formal methods and software engineering are especially welcome.
I served as a PC-Cochair for SEFM 2005. For information on the past SEFM conferences visit the general SEFM webpage.

SCENARIOS 2011, Berlin

2010-09-08T20:07:00.008+02:00

Photo: Ishtar Gate, Pergamon Museum, Berlin 2010.

I have been invited to serve on the Program Committee of SCENARIOS 2011, the 1st international workshop on Scenario-Based Testing . SCENARIOS 2011 is a satellite worksop of ICST 2011 to be held in Berlin, Germany, March 2011.

Nowadays, more and more techniques rely on human intervention so as to ensure the applicability of testing approaches. Indeed, a trade-off has to be found between the relevance of the test cases (requiring strong human intervention) and automation. Scenario-Based Testing addresses this issue by looking for more automation, with human intervention restricted to insightful activities. Over the years, different scenario based testing techniques have been developed to assist the validation engineer, using textual scenarios such as regular expressions, graphical notations such as UML interaction diagrams or test purposes specified as transitions systems. All these techniques represent an efficient solution to the state space explosion problem by restricting the possible executions of the system to a limited, and hopefully more accurate, subset of admissible traces. In addition, they make it possible to capture the human expertise for testing specific situations that can not be targeted by a systematic model coverage approach.

This first edition of the workshop on Scenario-Based Testing aims at gathering ideas and techniques in the area of semi-automated testing. It is intended to assess the effectiveness of available techniques and promote original research ideas that can be concretized into an industrial context.

MBT 2011, April 2-3, 2011, Saarbruecken, Germany

2010-09-08T19:33:00.010+02:00

Photo: Wolfgang Staudt

I have been invited to serve on the Program Committee of MBT 2011, the 7th Workshop on Model-Based Testing. MBT 2011 is a satellite worksop of ETAPS 2011 to be held in Saarbrücken, Germany.

The workshop is devoted to model-based testing of both software and hardware. Model-based testing is closely related to model-based specification. Models are used to describe the behavior of the system under consideration and to guide such efforts as test selection and test results evaluation. Both testing and verification are used to validate models against the requirements and check that the implementation conforms to the specification model.

Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics, such as state-based formalisms. Testing with such models allows one to measure the degree of the product's conformance with the model.

Techniques to support model-based testing are drawn from diverse areas, like formal verification, model checking, control and data flow analysis, grammar analysis, and Markov decision processes.

The intent of this workshop is to bring together researchers and users of models for to discuss the state of the art in theory, applications, tools, and industrialization of model-based specification, testing and verification.

Original submissions are solicited from industry and academia. They are invited to present their work, plans, and views related to model-based testing. The topics of interest include but are not limited to:

Online and offline test sequence generation methods and tools
Test data selection methods and tools
Runtime verification
Model-based test coverage metrics
Automatic domain/partition analysis
Combination of verification and testing
Models as test oracles
Scenario based test generation
Meta programming support for testing
Formalisms suitable for model-based testing
Application of model checking techniques in model-based testing
Game-theoretic approaches to testing
Model-based testing in industry: problems and achievements

Erlang on Mac OS X 10.6 (Snow Leopard)

2010-05-12T15:27:00.020+02:00

This is what I did to install Erlang on my MacBook Pro:

Install the GCC compiler. This is done by installing Xcode, Apple's developer tool set, available for free after registration. It can be found at the Apple ADC.
Install the Apache FOP print formatter. This Java application is needed for building the documentation. This implies that you also need Java. The configuration routine checks for Java SDK 1.5. (or higher). I had Java SDK 1.6 installed.
Get the latest Erlang source, which in my case was a file named otp_src_R13B03.tar. Unarchive the file and follow the instructions:
```
$ cd otp_src_R13B03
$. /configure
$ make
$ sudo make install
```
Now bring up a terminal and issue the command:
```
$ erl
Erlang R13B03 (erts-5.7.4) [source] [smp:2:2] [rq:2] [async-threads:0] [kernel-poll:false]

Eshell V5.7.4  (abort with ^G)
1> 1+2.
3
2>
```
That's it! I am ready to have some Erlang fun.

ICFEM 2010, Nov 16-19, Shangai

2010-05-12T10:08:00.016+02:00

Photo: Wolfgang Staudt

Another Shanghai conference I have been invited to serve on the Program Committee: ICFEM 2010, the 12th International Conference on Formal Engineering Methods. ICFEM 2010 will take place in Shanghai, right after UTP 2010. Submission deadline for abstracts is 28th of May 2010. The conference chair is my former colleague at UNU-IIST He Jifeng (East China Normal University, China), PC-cochairs are Jin Song Dong (National University of Singapore, Singapore) and Huibiao Zhu (East China Normal University, China).

ICFEM brings together those interested in the application of formal engineering methods to computer systems. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, and to help advance the state of the art. We are interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical, tangible benefit.

Submissions related to the following principal themes are encouraged, but any topics relevant to the field of formal methods and their support environments will also be considered:

Formal model-based development and code generation
Abstraction and refinement
Formal specification and modelling
Software verification
Formal approaches to software testing
Software model checking
Formal methods for object and component systems
Analysis and models for concurrency
Formal methods for cloud computing
Tool development and integration
Software safety, security and reliability
Experiments involving verified systems
Applications of formal methods

UTP 2010, Nov 15-16, Shanghai

2010-04-14T09:28:00.008+02:00

Photo: stevechasmar

I have been invited to serve on the Program Committee of UTP 2010, the 3rd International Symposium on Unifying Theories of Programming. UTP 2010 will take place in Shanghai. Submission deadline for abstracts is 4th of June 2010. The PC-chair is Shengchao Qin, University of Durham, UK.

Based on the pioneering work on Unifying Theories of Programming by Tony Hoare, He Jifeng, and others, the aims of the UTP Symposium series are to continue to reaffirm the significance of the ongoing UTP project, to encourage efforts to advance it by providing a focus for the sharing of results by those already actively contributing, and to raise awareness of the benefits of such unifying theoretical frameworks among the wider computer science and software engineering communities.

Of particular interest is how unification may be used to meet the goals and difficulties to be encountered in the Grand Challenges of Computing, with particular reference to the UK's "GC6: Dependable Systems Evolution", its international cousin the "Verified Software Initiative", and their plan to develop a Verified Software Repository. To this end the UTP2010 Symposium welcomes contributions on the above themes as well as others which can be related to them. Such additional themes include, but are not limited to, relational semantics, relational algebra, healthiness conditions, normal forms, linkage of theories, algebraic descriptions, incorporation of probabilistic programming, timed calculi and object-based descriptions, as well as alternative programming paradigms such as functional, logical, data-flow, and beyond. In all cases, the UTP approach should be compared and advantages/disadvantages discussed.

Student Projects 2010

2010-03-03T09:11:00.038+01:00

Photo: PhillipC

These are my project proposals for student projects in 2010. Most of the topics can be scaled to small student projects, bachelor thesis projects, master thesis projects and in some cases up to dissertation subjects. The projects are not isolated but fit the current research agenda of my group. The students are supervised in weekly meetings.

MOMUTSIP - Model-based Mutation Testing of the SIP Protocol: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for the Session Initiation Protocol used in Voice-Over-IP applications. This project is related to our FP7 MOGENTES project.

MOMUTCON - Model-based Mutation Testing of the Conference Protocol: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for the Conference Protocol, a simple multicast chat box protocol. This project is related to our FP7 MOGENTES project.

MOMUTSUR - Model-based Mutation Testing Survey: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to research related work and write a survey on the topic. This includes the study of related literature as well as the evaluation of other existing tools. This project is related to our FP7 MOGENTES project.

SEMU - Semantic Mutations of UML State Chart Diagrams: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. In model-based mutation testing a model is mutated by changing its syntax. The mutants represent bugs and test cases are generated to detect such bugs in an implementation. In this project we consider semantic mutations of models, i.e. what are the possible faulty interpretations of a given model. It is well-known that there are several possible interpretations of UML state charts. The student shall investigate the state of the art on this topic and describe the possible semantic variations. This semantic variations will be build into our UML-Action System translator for generating test cases. The idea is to generate test cases that will detect faulty behavior due to semantic misinterpretations. This project is related to our FP7 MOGENTES project.

MUTO - Mutation Operators for Object-Oriented Action Systems: (in progress) Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. In model-based mutation testing a model is mutated by changing its syntax. The mutants represent bugs and test cases are generated to detect such bugs in an implementation. The mutants are generated by so called mutation operators. A mutation operator is a rule how a certain syntactic term, e.g. a programming statement, should be changed. This changes or mutations represent faults. The aim of this project is to define a set of mutation operators for our Object-Oriented Action System modeling language. Based on this, a tool shall be developed that takes a model and the set of mutation operators and produces a number of mutated versions of this model (mutants). We use such mutants as input for our test case generator.

MOMUTCAR - Model-based Mutation Testing of a Car Alarm System: (in progress) Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for an industrial case study of a car alarm system. This project is related to our FP7 MOGENTES project.

SYANCO Winter School, Feb 8-12, Berlin

2010-01-19T11:18:00.012+01:00

Photo: alles-schlumpf

I have been invited to lecture on the upcoming SYANCO Winter School in Berlin.

The International Winter School on Synthesis and Analysis of Component Connectors is taking place from 8 till the 12 of February 2010 at Park Inn Berlin-Alexanderplatz, Berlin, Germany. It is jointly organized by Coordination Languages Research Group (SEN3), Centrum Wiskunde & Informatica (CWI), the Netherlands and Faculty of Computer Science, TU Dresden, Germany.

I will give a two hours lecture on Model-based Mutation Testing: Foundations and Applications. This lecture gives an introduction to mutation testing on the modelling level.

The original idea of mutation testing on the source-code level goes back to the late 1970s and works as follows: The tester injects faults into a program under test, by deliberately changing its source code. This faulty versions of the program are called mutants. Then, test cases are executed on these mutants. If all the faults are detected, the set of test cases can be considered adequate. If the tests fail this quality assessment, then additional test cases should be designed until all faults are detected. The assumption is that other faults in the original program can be caught as well, if it is able to detect the injected faults. We show how this technique can be applied in model-based testing. The idea is to automatically generate test cases from mutated formal models. The test cases are designed to detect those bugs in a system under test that have been anticipated on the modelling level. In the course we will present (1) the general theory behind our technique, based on program semantics and refinement preorders, (2) map the theory to different modelling styles, including contracts and process algebras, and (3) discuss the model-based mutation testing of protocols and embedded systems.

SEFM 2010, 13-17 September, Pisa, Italy

2009-11-12T11:51:00.007+01:00

Photo: Pisa 2007

I have been invited to serve on the Program Committee of SEFM 2010, the 8th IEEE International Conference on Software Engineering and Formal Methods. SEFM 2010 will take place in Pisa. Submission deadline for abstracts is 22 March 2010. The PC-chairs are Jose Luis Fiadeiro and Stefania Gnesi.

The aim of the conference is to bring together practitioners and researchers from academia, industry and government to advance the state of the art in formal methods, to facilitate their uptake in the software industry and to encourage their integration with practical engineering methods. Papers that combine formal methods and software engineering are especially welcome.

I served as a PC-Cochair for SEFM 2005. For information on the past SEFM conferences visit the general SEFM webpage.

Here the call for papers will be published as soon as it is out.

Fault-based Test Case Generation for Component Connectors

2009-10-23T17:06:00.009+02:00

Photo: Matthew Stinson

Sun Meng at CWI had the idea to translate my UTP-theory of mutation testing to REO connectors. This resulted in a TASE 2009 paper published in July:

Bernhard K. Aichernig, Farhad Arbab, Lacramioara Astefanoaei, Frank S. de Boer, Sun Meng, and Jan Rutten. Fault-based test case generation for component connectors. In TASE 2009, Third IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, July 29–31, pages 147–154. IEEE Computer Society, July 2009. Copyright by IEEE. (PDF) (doi:10.1109/TASE.2009.14)

The paper demonstrates that the idea of formalizing basic software engineering concepts in Hoare and He's Unifying Theories of Programming really helps to transfer knowledge and technology. In this case mutation testing found a new application domain: component connectors for modeling coordination in service-oriented architectures.

Abstract. The complex interactions appearing in service-oriented computing make coordination a key concern in serviceoriented systems. In this paper, we present a fault-based method to generate test cases for component connectors from specifications. For connectors, faults are caused by possible errors during the development process, such as wrongly used channels, missing or redundant subcircuits, or circuits with wrongly constructed topology. We give test cases and connectors a unifying formal semantics by using the notion of design, and generate test cases by solving constraints obtained from the specification and faulty connectors. A prototype symbolic test case generator serves to demonstrate the automatizing of the approach.

More conference papers.

FMCO 2008: Conformance Testing of Distributed Concurrent Systems with Executable Designs

2009-10-13T18:04:00.025+02:00

Photo: *clairity*

In August our FMCO 2008 paper was published:

Bernhard K. Aichernig, Andreas Griesmayer, Einar Broch Johnsen, Rudolf Schlatte, and Andries Stam. Conformance testing of distributed concurrent systems with executable designs. In Formal Methods for Components and Objects: 7th International Symposium, FMCO 2008, Sophia Antipolis, France, October 21–23, 2008, Revised, volume 5751 of Lecture Notes in Computer Science, pages 61–81, Berlin/Heidelberg, August 2009. Springer. (PDF) (doi:10.1007/978-3-642-04167-9_4)

The paper is a result of the CREDO project. It shows our testing process based on the modeling language Creol. Concolic execution on the model generates test stimuli and these are then executed on a system under test. During a test run the event traces are recorded and then replayed on the model. A small GUI helps to identify the controllable events for generating the test driver for Creol.

Abstract. This paper presents a unified approach to test case generation and conformance test execution in a distributed setting. A model in the object-oriented, concurrent modeling language Creol is used both for generating test inputs and as a test oracle. For test case generation, we extend Dynamic Symbolic Execution (also called Concolic Execution) to work with multi-threaded models and use this to generate test inputs that maximize model coverage. For test case execution, we establish a conformance relation based on trace inclusion by recording traces of events in the system under test and replaying them in the model. User input is handled by generating a test driver that supplies the needed stimuli to the model. An industrial case study of the Credo project serves to demonstrate the approach.

More conference papers.

MBT 2010, March 21, Paphos, Cyprus

2009-10-12T14:04:00.006+02:00

Photo: Grabowski

I have been invited to serve on the Program Committee of MBT 2010, the 6th Workshop on Model-Based Testing. MBT 2010 is a satellite worksop of ETAPS 2010 to be held at Paphos, the birthplace of Aphrodite.

The call for papers is out. Submission deadline: December 10, 2009

Techniques to support model-based testing are drawn from diverse areas, like formal verification, model checking, control and data flow analysis, grammar analysis, and Markov decision processes.

Online and offline test sequence generation methods and tools
Test data selection methods and tools
Runtime verification
Model-based test coverage metrics
Automatic domain/partition analysis
Combination of verification and testing
Models as test oracles
Scenario based test generation
Meta programming support for testing
Formalisms suitable for model-based testing
Application of model checking techniques in model-based testing
Game-theoretic approaches to testing
Model-based testing in industry: problems and achievements

Journal Paper: Fault-Based Conformance Testing in Practice

2009-10-07T22:42:00.017+02:00

Photo: marcusuke

We got our work on mutation testing of communication protocols published in the International Journal of Software and Informatics.

The article is part of a special double issue on Formal Methods edited by Prof. Dines Bjorner. The journal is published by the Chinese Academy of Science and has an international editing board.

Martin Weiglhofer, Bernhard Aichernig, and Franz Wotawa. Fault-based conformance testing in practice. International Journal of Software and Informatics, 3(2–3):375–411, June/September 2009. Copyright by Institute for Software, Chinese Academy of Science. (PDF)

In this work we present our results on testing two communcation protocols the Session Initiation Protocol and the Conference Protocol. The protocols are modeled in LOTOS and then mutation testing is applied on the LOTOS specs for generating test cases. We present detailed data of the test process including the nice result that we were able to find a new bug in an implementation that was not detected by random and scenario-based testing.

Paper abstract: Conforming to protocol specications is a critical issue in modern distributed software systems. Nowadays, complex service infrastructures, such as Voice-over-IP systems, are usually built by combining components of dierent vendors. If the components do not correctly implement the various protocol specications, failures will certainly occur. In the case of emergency calls this may be even life-threatening. Functional black-box conformance testing, where one checks the conformance of the implemented protocol to a specication becomes therefore a major issue. In this work, we report on our experiences and ndings when applying fault-based conformance testing to an industrial application. Besides a discussion on modeling and simplications we present a technique that prevents an application from implementing particular faults. Faults are modeled at the level of the specication. We show how such a technique can be adapted to specications with large state spaces and present results obtained when applying our technique to the Session Initiation Protocol and to the Conference Protocol. Finally, we compare our results to random and scenario based testing.

AI meets Formal Methods: Qualitative Reasoning and Action Systems

2009-09-23T21:45:00.016+02:00

Photo: cokada

We got our work on combining Qualitative Reasoning Techniques with Action Systems accepted at ICFEM 2009 in Rio.

This year the conference was highly competitive with an acceptance rate below 30 percent. The paper integrates Qualitative Differential Equations into Back's Action System formalism for modeling hybrid systems. The work forms part of the MOGENTES Project and aims at model-based testing of hybrid systems.

To our knowledge this is the first time that Qualitative Differential Equations have been merged into a formal development technique. The results are not limited to Action Systems, but apply also to similar formalisms like e.g. Event-B.

Bernhard K. Aichernig, Harald Brandl, and Willibald Krenn. Qualitative action systems. In Proceedings of ICFEM 2009: 11th International Conference on Formal Engineering Methods, Dec 9-12, 2009, Rio de Janeiro, Lecture Notes in Computer Science. Springer-Verlag, 2009. in press. (PDF)

Paper abstract: An extension to action systems is presented facilitating the modeling of continuous behavior in the discrete domain. The original action system formalism has been developed by Back et al. in order to describe parallel and distributed computations of discrete systems, i.e. systems with discrete state space and discrete control. In order to cope with hybrid systems, i.e. systems with continuous evolution and discrete control, two extensions have been proposed: hybrid action sys- tems and continuous action systems. Both use dierential equations (relations) to describe continuous evolution. Our version of action systems takes an alternative approach by adding a level of abstraction: continuous behavior is modeled by Qualitative Dierential Equations that are the preferred choice when it comes to specifying abstract and possibly non-deterministic requirements of continuous behavior. Because their solutions are transition systems, all evolutions in our qualitative action systems are discrete. Based on hybrid action systems, we develop a new theory of qualitative action systems and discuss how we have applied such models in the context of automated test-case generation for hybrid systems.

TAP 2010, June 28 - July 2, Malaga, Spain

2009-09-07T21:53:00.023+02:00

Photo: Pat McDonald

I have been invited to serve on the Program Committee of TAP 2010, the 4th International Conference on Tests & Proofs.

The TAP conference is devoted to the convergence of proofs and tests. It combines ideas from both sides for the advancement of software quality.

Gordon Fraser, a former colleague of mine at TU Graz, is co-chairing the PC with Angelo Gargantini. The conference chairs are Yuri Gurevich, Microsoft Research, USA and Bertrand Meyer, ETH Zuerich, Switzerland.

Last year, we had a paper at TAP 2009 on concolic execution of distributed systems (see my conference papers).

Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using rather different techniques and tools.

The conference will include a mix of invited and submitted presentation, and a generous allocation of panels and informal discussions. All papers will be published in Springer's LNCS series.

Two in One: functional plus OO-programming in Scala

2009-08-10T19:42:00.019+02:00

Photo: PyEuler

I believe in the functional first approach to teach computer programming to computer scientists. This means that students start with a functional programming language before programming in an imperative object-oriented style.

The advantage of this approach is that at the beginning the students can focus on problem solving writing functions with a given set of data structures ignoring the computer architecture. Only later they concentrate on how to implement such data-structures in an efficient way by exploiting the computer architecture.

From 1998-2001 I was involved in such a course to first year students of TU Graz. We started with SML in the first half-year and then switched to Java. All this could now be done in the programming language Scala that combines the pros of both programming paradigms.

I recommend to take a closer look at Scala. It might be the Java of the future. Scala combines features of both worlds. The most prominent features I've missed so long in OO languages are there:

functions are values
pattern matching
higher order functions
closures
lazy evaluation
Milner's type inference system

However, it is far from being un-orthodox with OO features like:

all values are objects
compiles to the Java Virtual Machine
full overloading including operators
(multiple) inheritance
direct definition of (singleton) objects
support for concurrency

The power this combination of paradigms brings cannot be underestimated: Scala's control structures can be extended in the language itself. Hence, it is possible to write domain specific commands. An example is Scala's support for the Actor communication model known from Erlang. It has been defined purely in Scala and is included as a library. Voila! Parallel programming with Actors on the JVM. Use the summer break to dive into Scala! Fun included.

Modeling and Testing Multi-Threaded Asynchronous Systems with Creol

2009-07-29T10:05:00.020+02:00

Bosphorus bridge in Istanbul viewing from Asia to Europe.

After a long waiting period, yesterday our TTSS 2008 paper was published by Elsevier. The paper is a result of the CREDO project.

Bernhard Aichernig, Andreas Griesmayer, Rudolf Schlatte, and Andries Stam. Modeling and testing multi-threaded asynchronous systems with Creol. In Proceedings of the 2nd International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2008), Istanbul, Turkey, 30 August 2008, volume 243 of Electronic Notes in Theoretical Computer Science, pages 3–14. Elsevier, July 2009. (PDF) (doi:10.1016/j.entcs.2009.07.002)

The paper describes a model-based testing technique for asynchronous, concurrent systems and shows how the modeling language Creol can serve as a test oracle. Creol is a nice object-oriented modeling language for distributed systems by University of Oslo. We applied the technique to a commercial agent-based information system.

The basic steps of our method are:

Create an abstract model of the system under test (SUT) in Creol.
Instrument the source code of the SUT by aspect-oriented programming techniques (here AspectC) for recording events.
Execute tests on the SUT and record the events.
Translate the event traces to Creol test cases.
Replay the test case on the model.
If successful: the test passed;
If it fails: model check if there is a different non-deterministic path for this test case, if not the test failed.

Check out my other conference papers.

ICTAC 2010, Sept 1-3, Natal, Brazil

2009-07-27T16:58:00.026+02:00

Photo courtesy of Dany Sakugawa

I have been invited to serve on the Program Committee of ICTAC 2010.

It will have a special track on Formal Testing Approaches headed by Marie-Claude Gaudel.

ICTAC 2010 is the 7th International Colloquium on Theoretical Aspects of Computing, the latest in a series founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). ICTAC brings together practitioners and researchers to present their research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development.

The seventh edition of the event, ICTAC2010, will be held from the 1st to the 3rd of September, 2010, in Natal, Brazil.

ICTAC2010 will invite submissions of research papers of up to 15 pages and of tool papers of up to 6 pages. Research papers should contain original research, and sufficient detail to assess the merits and relevance of the contribution. Submissions reporting on industrial case studies are also welcome. Tool demonstration papers should stress the technical and practical side, illustrating how one can apply the theoretic contributions in practice. The schedule for submission and evaluation of papers is as follows.

Submission of abstracts: 08 March, 2010
Submission deadline: 15 March, 2010
Notification of acceptance: 30 April, 2010
Final version: 16 May, 2010

Semantics? Yes tester, you need it!

2009-07-23T15:59:00.021+02:00

Once I had a testing project in industry in which we ran into the common situation that we did not know how to interpret a given requirement. Well, we asked the requirements manager for advice. Since it was a tricky question, he forwarded our request to the customer and to the developers. We were fortunate in getting quick responses. However, there was a problem: the answers were contradicting each other.

What had happened? Well, the customer and the developers had different interpretations of the requirements. There was a misunderstanding about this requirement. The consequence: the developers were implementing an incorrect system from the customers point of view.

So what about the tester? His understanding of the requirements is crucial. In the example above, the asking of us testers highlighted a serious problem. Without a clear understanding of the requirements, no reliable test verdict (pass or fail) can be given.

However, how do we know, if a tester understands the requirements? He could have made the same mistake as the developers. What if two testers (e.g. the customer's and the developer's) have different understandings of the requirements of a given SUT? Well, they would give different test verdicts: one might accept the SUT the other not. Is there a way to prevent such misunderstandings?

Not in general, because misunderstanding is a psychological process of wrong interpretation. However, we can limit the roots of such misinterpretations. We need to define the semantics, i.e. the meaning, of the requirements. And if nobody does it in a project, the tester should.

How do we define the semantics of requirements? Answer: by writing them in a formal notation with a precise semantics. There are modeling languages that come with a precise semantics, like VDM-SL, Z, B, Alloy, RAISE, CSP, LOTOS etc. These languages serve different purposes, but what they have in common is that their meaning is precisely defined, i.e. there is no ambiguity how to interpret what is written down.

Therefore, model-based testing should always apply models with a precise, formal semantics. Ok, most of the time a tester will not need it, because the meaning seems obvious, but as testers know, the rare cases matter. It even becomes more critical for model-based testing tools. If there is no precise standard semantics, different tools might behave differently for the same models. (A common problem of compilers for programming languages without precise semantics).

Here is my advice: if somebody tries to sells you a model-based testing technique, ask him if his notation has a formal semantics. If he answers positively, double-check and ask for formal proofs done in this notation. No proofs, no formal semantics. Don't accept notations with misunderstanding built in!

More on model-based testing with formal notations can be found in my publications.

Lecturing in China

2009-07-23T10:08:00.020+02:00

From 2002 to 2006 I worked for the UN as a Research Fellow of UNU-IIST in Macao, a special administrative region of China. Part of the job was to hold advanced computer-science courses in developing countries. The participants were post-graduates, typically young assistant professors.

In 2003, at a course in Lanzhou I certainly got the most impressive welcome: my name on a banner at the entrance to the campus (see picture). In China protocol is important, but Lanzhou Jiatong University was special. As a UN representative I was also officially welcomed by the rector and interviewed by their campus TV. I must admit, I was slightly impressed. Even more so by the fact that they had their own hotel on campus in which I stayed.

The course title was Formal Methods in Software Development. Lanzhou Jiatong University, Lanzhou, China, December 15--19, 2003.

Teaching formal methods is fun!

The course participants.

Lecturing in Africa

2009-07-21T23:47:00.036+02:00

From 2002 to 2006 I worked for the UN as a Research Fellow of UNU-IIST in Macao, China. Part of the job was to hold advanced computer-science courses in developing countries. The participants were post-graduates, typically young assistant professors.

Most fascinating and adventurous were my two courses in Africa, one in Lagos, Nigeria and one in Dakar, Senegal.

University of Lagos, Nigeria, Nov. 4-8, 2002

The course title was Formal Methods in Software Development. It was part of the School on Methods, Tools and Techniques for Industrial Software Development jointly organized by UNU-IIST and University of Lagos.

The Lagos course participants and their lecturer (guess who it is!).

Our lunch was colorful.

Universite Cheikh Anta Diop, Dakar, Senegal, November 24–28, 2003

The course in Dakar was on Foundations of Software Testing covering formal testing techniques.

The Dakar course participants and myself.

On the weekend there was time to enjoy the beauty of Africa.

Bernhard's Research Area

2009-07-09T12:55:00.005+02:00

Bernhard’s research focuses on the foundations of software engineering. In particular, I'm interested in

formal development methods
specification, modeling and design of reliable software
theories of programming, refinement calculi, concurrency
foundations of software testing.

His current research is mainly concerned with the automated generation of test-cases from formal requirements specifications as well as with the associated testing theories. This includes the investigation of existing testing, specification and refinement techniques. The aim is to develop testing theories that are able to unify the existing results on specification-based testing and advance the field.

His current emphasis is on fault-based testing. Fault-based testing is a technique where testers anticipate errors in a system under test in order to asses or generate test cases. The idea is to have enough test cases capable of detecting these anticipated errors. He applies this method on the specification level. His latest testing theory is based on Hoare and He's Unifying Theory of Programming (UTP) and has been instantiated to test case generator’s for OCL, Spec#, LOTOS and most recently Action Systems.

MOGENTES Project

2009-07-09T10:12:00.009+02:00

I am the project manager and senior researcher for TU Graz in the MOGENTES project.

MOGENTES stands for Model-based Generation of Tests for Dependable Embedded Systems and is an European STREP project in the 7th EU framework programme.

The coordinator is the Austrian Institute of Technology.

MOGENTES aims at significantly enhancing testing and verification of dependable embedded systems by means of automated generation of test cases relying on development of new approaches as well as innovative integration of state-of-the-art techniques.

Driven by the needs of its industrial partners, it will address both testing of non-functional issues like reliability, e.g. by system stress and overload tests, and functional safety tests, meeting the requirements of standards such as IEC 61508, ISO WD 26262, or AUTOSAR.

MOGENTES will demonstrate that different domains with a wide variety of requirements can significantly benefit from a common model-based approach for achieving automated generation of efficient test cases and for verifying system safety correctness using formal methods and fault injection, as this approach increases system development productivity while achieving predictable system dependability properties. For that purpose, proof-of concept demonstrations will show the applicability of the developed technologies in two application domains: railway and automotive (on- and off-road).

In particular, MOGENTES aims at the application of these technologies in large industrial systems, simultaneously enabling application domain experts (with rather little knowledge and experience in usage of formal methods) to use them with minimal learning effort. All in all, MOGENTES will increase knowledge and develop new techniques and tools in the area of verification and validation of dependable embedded systems which can be applied in model-based development processes also by non-experts in formal methods.