A novel model-based testing approach for software product lines

Model-based testing relies on a model of the system under test. FineFit is a framework for model-based testing of Java programs. In the FineFit approach, the model is expressed by a set of tables based on Parnas tables. A software product line is a family of programs (the products) with well-defined commonalities and variabilities that are developed by (re)using common artifacts. In this paper, we address the issue of using the FineFit approach to support the development of correct software product lines. We specify a software product line as a specification product line where each product is a FineFit specification of the corresponding software product. The main challenge is to concisely specify the software product line while retaining the readability of the specification of a single system. To address this, we used delta-oriented programming, a recently proposed flexible approach for implementing software product lines, and developed: (1) delta tables as a means to apply the delta-oriented programming idea to the specification of software product lines; and (2) DeltaFineFit as a novel model-based testing approach for software product lines.     

How to Implement a Safe Real-Time System:The OBSERV Implementation of the Production Cell Case Study

The Production Cell example was chosen by FZI (the Computer Science Research Center), in Karlsruhe. to examine the benefits of formal methods for industrial applications. This example was implemented in more than 30 formalisms. This paper describes the implementation of the Production Cell in OBSERV. The OBSERV methodology for software development is based on rapid construction of an executable specification, or prototype, of a system, which may be examined and modified repeatedly to achieve the desired functionality. The objectives of OBSERV also include facilitating a smooth transition to a target system, and providing means for reusing specification, design, and code of systems, particularly real-time reactive systems. In this paper we show how the methods used in the OBSERV implementation address the requirements imposed by reactive systems. We describe the OBSERV implementation of the Production cell, explain design decisions, with special emphasis on reusability and safety issues. We demonstrate how to take care of safety and liveness properties required for this example. These properties are checked by means of simulation and formally proved with a model checker.     

GenUTest: a unit test and mock aspect generation tool

Unit testing plays a major role in the software development process. What started as an ad hoc approach is becoming a common practice among developers. It enables the immediate detection of bugs introduced into a unit whenever code changes occur. Hence, unit tests provide a safety net of regression tests and validation tests which encourage developers to refactor existing code with greater confidence. One of the major corner stones of the agile development approach is unit testing. Agile methods require all software classes to have unit tests that can be executed by an automated unit-testing framework. However, not all software systems have unit tests. When changes to such software are needed, writing unit tests from scratch, which is hard and tedious, might not be cost effective. In this paper we propose a technique which automatically generates unit tests for software that does not have such tests. We have implemented GenUTest, a prototype tool which captures and logs interobject interactions occurring during the execution of Java programs, using the aspect-oriented language AspectJ. These interactions are used to generate JUnit tests. They also serve in generating mock aspects—mock object-like entities, which enable testing units in isolation. The generated JUnit tests and mock aspects are independent of the tool, and can be used by developers to perform unit tests on the software. Comprehensiveness of the unit tests depends on the software execution. We applied GenUTest to several open source projects such as NanoXML and JODE. We present the results, explain the limitations of the tool, and point out direction to future work to improve the code coverage provided by GenUTest and its scalability.