Protocol conformance testing a SIP registrar

Photo: Tiptel

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

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

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

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

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

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.