The STECC Framework - An Architecture for Self-Testable Components

Development of a software system from existing components can surely have various benefits, but can also entail a series of problems. One type of problem is caused by a limited exchange of information between the developer and user of a component. A limited exchange and thereby a lack of information can have various consequences, among them the requirement to test a component prior to its integration into a software system. A lack of information cannot only make testing prior to integration necessary; it can also complicate this task. However, difficulties in testing can be avoided if certain provisions to increase testability are taken beforehand. This article briefly describes a new form of improving testability of, particularly commercial, components, the self-testing COTS components (STECC) strategy and explains in detail the STECC framework, which implements the necessary technical architecture to augment Java components with self-testability.

Test-Case Mutation

This chapter presents a new testing technique called “test-case mutation.” The idea is to apply a set of specific mutation operators to test cases for object-oriented software, which produces different versions of the original test cases. Then, the results of the original test case and of its corresponding mutants are compared; if they are very similar, the technique highlights the possible presence of a fault in the class under test. The technique seems useful for testing the correctness of strongly constrained classes. The authors have implemented a supporting tool that is also described in the chapter.

Automated Software Testing

This chapter approaches paramount aspects related to test automation, introducing the importance of implementation in the software market and essential bases, such as adjustment to the organizational reality and establishment of an efficient strategy. Types of tools and directives for a successful implantation are presented. Test automation has been considered the main measure taken to enhance test efficiency — fundamental in the software-development process. Responsible for verifying and/or validating the quality of the executable product compared to performed documentation and client requirements. Therefore, with the chapter content here provided, we aim to provide the reader with an understanding of test automation and grant relevant orientations to assist implementing it.

Safecharts Model Checking for the Verfication of Safety-Critical Systems

Unintentional design faults in safety-critical systems might result in injury or even death to human beings. However, the safety verification of such systems is getting very difficult because designs are becoming very complex. To cope with high design complexity, model-driven architecture (MDA) design is becoming a well-accepted trend. However, conventional methods of code testing and hazard analysis do not fit very well with MDA. To bridge this gap, we propose a safecharts model-based formal verification technique for safety-critical systems. The safety constraints in safecharts are mapped to semantic equivalents in timed automata. The theory for safety verification is proved and implemented in the SGM model checker. Prioritized and urgent transitions are implemented in SGM to model the safe chart risk semantics. Finally, it is shown that priority-based approach to mutual exclusion of resource usage in safecharts is unsafe and solutions are proposed. Application examples show the benefits of the proposed model-driven verification method.

Static Type Systems

Static type systems are fundamental tools used to determine properties of programs before execution. There exist several techniques for validation and verification of programs based on typing. Thus, type systems are important to know for the practicioner. When designing and implementing a technique based on typing systems, there is usually a gap between the formal tools used to specify it, and the actual implementations. This gap can be an obstacle for language designers and programmers. A better understanding of the features of a type system and how they are implemented can help enourmously to the good design and implementation of new and powerful verification methods based on type systems. This chapter addresses the problem of specifying and implementing a static type system for a simple language, but containing many of the subtleties found in bigger, mainstream languages. This contributes to the understanding of the techniques, thus bridging the gap between theory and practice. Additionally, the chapter contains a small survey of some of the existing developments in the static typing area and the static analysis based on typing.

Certifying Properties of Programs Using Theorem provers

Proving the correctness of a program, even the simplest one, is a complex and expensive task; but, at the same time, it is one of the most important activities for a software engineer. In this chapter, we explore the use of theorem provers to certify properties of software; in particular, two different proof-assistants are used to illustrate the method: Coq and PVS. Starting with a simple pedagogic example, a sort algorithm, we finally reproduce the same approach in a more realistic scenario, a model of a block-allocation algorithm for a video-on-demand server.

Discrete Event Simulation Process Validation, Verification, and Testing

This chapter introduces validation, verification, and testing tools and techniques pertaining to discrete event simulation. The chapter distinguishes between validation and verification within the context of discrete event simulation. Then, we will show the importance of such topic by revealing the amount research done in simulation validation and verification. The chapter subsequently discusses the reasons why simulation projects fail and the sources of simulation inaccuracies. Next, the chapter gives different taxonomies for validation, verification, and testing techniques (VV&T) for both types of simulation systems: object-oriented-based and algorithmic-based. Therefore, the chapter will present a translation of thirteen software-engineering practices suggested for simulation projects. Notwithstanding the significance of providing an objective assessment platform, as such, the chapter will shed light on the independence of VV&T pertaining to simulation systems.

Validation and Verification of Software Systems Using Virtual Reality and Coloured Petri Nets

Validation and verification techniques have been identified as suitable mechanisms to determine if the software meets the needs of the user and to verify if the software works correctly. However, the existing verification techniques do not support friendly visualization. Also, validation techniques with friendly visualization mechanisms do not allow the verification of the system’s correctness. In this chapter, we present a method for the validation and verification of software systems through the integration of formal methods and virtual reality. Furthermore, a software tool associated with such a method is also described along with an embedded system case study.

Fault-Based Testing

In this chapter, we review the state of the art and practice in fault-based testing. Based on the analysis and the reviews, we propose a comprehensive method for testing and present its main elements. Traditional fault-based testing is concerned with syntactic errors. These errors represent only a small portion of possible errors. Our testing approach is not restricted to these errors. We propose to use fault-tree analysis to determine how certain undesirable states can occur in a system. The results of the analysis expressed in terms of duration calculus formulas are integrated with state chart-based specifications. As a result, we obtain a testing model that provides a representation of the way the system behavior can be compromised by failures or abnormal conditions or interactions. In this way, we can automatically derive fault-based test cases. The example presented in this work illustrates the kinds of problems that arise in Web applications.

Efficient Software Quality Assurance Approaches Oriented to UML Models in Real Life

UML is accepted as the standard notation for object-oriented (OO) development. UML models have a widespread use in today’s software practices. Any initiative to improve software quality assurance (SQA) should assume that a high percentage of deliverables to be controlled are currently based on the use of UML notation. However, real life projects are strongly influenced by the need of reaching tangible productivity and efficiency goals. SQA techniques should be customized to meet the balance between quality and budget supported by risk analysis. In this chapter, different strategies and techniques devised to follow the above philosophy of efficiency are presented, especially centred in automatic testing generation from specifications. Our proposal is mainly based on a recommended course of action as well as on integrated tool support for Eclipse environments.