Abstract
Software testing is a very important activity of the software development process. To expedite the testing process and improve the quality of the tests, models are increasingly used as a basis to derive test cases automatically - a technique known as model-based testing (MBT). Given a system model and a test suite derived automatically from the model or created by other process, the coverage of the model achieved by the test suite is important to assess the quality and completeness of the test suite early in the software development process. This paper presents a novel tool that shows visually the coverage achieved by a test suite on a UML state machine model. The tool receives as input a UML state machine model represented in XMI and a test suite represented in a XML format, and produces a colored UML state machine model that shows the coverage result. Model test coverage is determined by simulating the execution of the test suite over the model. An example is presented in order to show the features of the tool. © 2010 IEEE.

Abstract
Several approaches exist to automatically derive test cases that check the conformance of the implementation of abstract data types (ADTs) with respect to their specification. However, they lack support for the testing of implementations of ADTs defined by generic classes. In this paper, we present a novel technique to automatically derive, from specifications, unit test cases for Java generic classes that, in addition to the usual testing data, encompass implementations for the type parameters. The proposed technique relies on the use of Alloy Analyzer to find model instances for each test goal. JUnit test cases and Java implementations of the parameters are extracted from these model instances. © 2012 Springer-Verlag.

Abstract
This paper describes a process to reverse engineer structural and behavioural formal models of a GUI application by a dynamic technique, mixing manual with automatic exploration. The goal is to diminish the effort required to construct the model and mapping information needed in a model-based GUI testing process. A skeleton of a state machine model of the GUI, represented in a formal pre/post specification language, is generated automatically by the exploration process. Mapping information between the model and the implementation is also generated along the way. The model extracted automatically is then completed manually in order to get an executable model which can be used as a test oracle. Abstract test cases, including expected outputs, can be generated automatically from the final model and executed over the GUI application, using the mapping information generated during the exploration process.

Abstract

Abstract
The incorrect behaviour of Graphical User Interfaces (GUIs) can compromise the effective use of the overall software application. One way to discover defects and increase the quality of GUIs is through testing. Test cases can be created manually or produced automatically from a model of the GUI. The size and complexity of GUIs makes it unpractical to do extensive manual testing. However, creating a model of the GUI in order to generate automatically test cases is also a laborious task. This paper presents a reverse engineering approach for diminishing the effort required for constructing the model of an existing GUI. The GUI is exercised by a combination of manual and automatic exploration, and information about its structure and some of its behaviour is automatically extracted, resulting in an incomplete GUI model. This model is subsequently completed manually, validated and used as input for automatic test generation and execution.

Abstract
It is proposed an approach to integrate formal methods in the software development process, with an emphasis on the user interface development. The approach covers the specification by means of formal models, early model animation and validation, construction and conformity testing of the user interface implementation with respect to the specification. These conformity tests are described in detail through a state transition model with an abstraction function mapping concrete (implementation) to abstract (specification) states and operations. In order to illustrate the approach, it is presented a simple login/password dialog specification in VDM++, using a reusable control specification library, with a straightforward translation to Java or C#.