Qualification and Certification in the Avionics Domain

Get Complete Project Material File(s) Now! »

Specification-based Oracles of Code Generator Integration Tests

Having so far discussed the production of integration test models, we also need to investigate the corresponding test oracles i.e. the means to determine if an integration test passes or fails. Since integration tests aim at covering unit test requirements of all the transformations involved in the MTC, then there will likely be a large number of tests. It is therefore desirable if not necessary to have automatic test oracles determine the validity of test outputs.
In an integration test of an ACG the input is a model and the output is source code. In the literature we find that most test oracle approaches aim at validating the semantics of source code, i.e. verifying that the behavior of the generated code is compatible with the semantics of the input model. However in the context of qualification and certification, the syntax of the generated source code is also of importance and must be shown to comply with the applicable code standard. This syntactic aspect is less developed in the literature of ACG testing. Additionally, the qualification standard requires test oracles to be based on the specification, which in turn is subject to several reviews by different stakeholders. As a result, it is important that this specification be readable and easily understandable. Consequently, the second problem that we tackle in our work is the following:
Devising a specification and automatic test oracles approach focusing on the syntax of the generated source code and the readability of the specification. Having defined the two main problems tackled by this study, we present in the next section a summary of the solutions that we propose to address them.

Summary of Contributions

To address the first problem of backward translation of test requirements we propose to transpose it to the formal framework of Algebraic Graph Transformation which provides the means to translate and reason on constraints. As for the second problem of determining the verdict of integration tests, we propose a specification and test oracles approach based on the textual concrete syntax of the generated source code. In the following sections we develop our solutions and the conceptual and concrete contributions that they provide.

Backward Translation of Test Requirements

Concerning the first problem of backward translation of test requirements, we note first that MTCs can include several steps (e.g. typically 15 for code generation). As a result we propose an iterative approach that performs the backward translation of test requirements step by step. Solving the sub-problem of backward translation for one model transformation step of the chain would theoretically unlock the solution for the complete chain.
In the scope of this thesis, we propose and validate an approach to the one-step backward translation of a unit test requirement into an equivalent constraint over the input of the preceding transformation. To do so, we propose to rely on existing theoretical concepts in the formal framework of Algebraic Graph Transformation (AGT) [Ehrig et al., 2006]. Assuming that the transformation is specified in the ATL model transformation language [Jouault et al., 2008], our approach is composed of two steps:
1. Translate the preceding transformation from ATL to the formal framework of AGT.
2. Consider the unit test requirement as a postcondition, i.e. a constraint on the output of the transformation, and translate it into an equivalent precondition, i.e. a constraint over the input of the transformation. The translation uses a set of analyses called Post2Pre that we propose based on the formal construction of the weakest liberal precondition (wlp) in AGT.
With these two steps, we obtain a constraint over the input of the preceding transformation that ensures the satisfaction of the unit test requirement. Since the result is a constraint, it can again be considered as a postcondition of its preceding transformation, and thus the analysis can be iterated.

Table of contents :

List of Figures
List of Tables
List of Code Listings
Résumé de la Thèse en Français
1 Contexte
1.1 Certification de Systèmes Critiques et Qualification d’Outils .
1.2 Chaines de Transformations de Modèles et Génération de Code
2 Etat de l’Art
3 Problématique
3.1 Test Unitaire et Test d’Intégration des Chaines de Transformations de Modèles
3.2 Oracles de Test des Transformations Model-to-Code
4 Contributions
4.1 Traduction Arrière des Exigences de Test Unitaire
4.2 Spécification et Oracles de Tests de Transformations Modelto- Text
5 Résultats Expérimentaux
5.1 Validation de ATL2AGT
5.2 Validation de Post2Pre
5.3 Validation de l’Approche de Spécification et d’Oracles de Test Model-to-Text
6 Conclusion
6.1 Rappel des Problématiques
6.2 Résumé des Contributions
6.3 Perspectives de Poursuite
1 Introduction
1.1 General Context
1.2 Problem Statement
1.2.1 Unit Testing v/s Integration Testing
1.2.2 Specification-based Oracles of Code Generator Integration Tests
1.3 Summary of Contributions
1.3.1 Backward Translation of Test Requirements
1.3.2 Specification and Test Oracles of Model-to-Code Transformations
1.4 Document Organisation
2 Background: Qualification and Certification in the Avionics Domain
2.1 Introduction
2.2 Certification of Critical Airborne Software
2.2.1 Planning and Development Processes
2.2.2 Verification Activities and Verification Objectives
2.3 Claiming Certification Credit with Qualified Tools
2.4 Qualifying an ACG
2.4.1 Coupling of Certification and Qualification – Qualifiable Tools
2.4.2 Tool Qualification Planning
2.4.3 Tool Development
2.4.4 Tool Verification
2.5 Requirements-Based Testing in Qualification
2.6 Scope of the Research: Model Transformation Chains
2.7 Conclusion
3 Literature Review on the Testing of Model Transformations and Code Generators
3.1 Introduction
3.2 Formal Verification of Model Transformations
3.3 Model Transformation Testing Foundations
3.3.1 General Scheme for Test Adequacy Criteria and Test Generation
3.3.2 General Scheme for Test Oracles
3.4 Test Adequacy Criteria
3.4.1 Mutation Criterion
3.4.2 Input Metamodel Coverage Criteria
3.4.3 Specification-based Criteria
3.4.4 OCL Structural Coverage Criteria
3.5 Test Model Generation
3.5.1 Ad-hoc Model Generation Based on Model Fragments
3.5.2 Model Generation with Constraints Satisfaction Problem Solving
3.5.3 Semi-Automatic Model Generation based on Mutation Analysis
3.6 Test Oracles
3.6.1 Manually Validated Expected Results
3.6.2 Contracts as Partial Oracles
3.7 Testing of Model Transformation Chains
3.7.1 Test Suite Quality for Model Transformation Chains
3.8 Testing Code Generators
3.8.1 Semantic Testing of Code Generators
3.8.2 Syntactic Testing of Code Generators
3.9 Conclusion
4 Analysis and Problem Statement
4.1 Introduction
4.2 Unit Testing and Integration Testing of Model Transformation Chains
4.2.1 Unit Testing and Integration Testing in Qualification
4.2.2 Formalising Unit Testing
4.2.3 Achieving Unit Testing Confidence Through Integration Tests
4.2.4 The Problem: Producing Integration Test Models to Cover Unit Test Cases
4.3 Specification-based Test Oracles for Model-to-Code Transformations 104
4.3.1 Test Oracles and Requirements in Qualification
4.3.2 Requirements Specification of a Code Generator
4.3.3 Semantic and Syntactic Test Oracles
4.3.4 The Problem: Devise a Syntactic Specification and Test Oracles
Approach for an ACG
4.4 Conclusion
5 General Approach
5.1 Introduction
5.2 Backward Translation of Test Requirements
5.2.1 Core Principle : Backwards Translation of Constraints
5.2.2 Weakest Precondition of Algebraic Graph Transformations
5.2.3 Assumptions and Scope of the Contributions
5.2.4 Contributions
5.3 Syntactic Specification of Model-to-Code Transformation
5.3.1 Core Principle: Specification Templates
5.3.2 Automatic Test Oracles
5.3.3 Readability and Generation of Qualification Documents
5.3.4 Implementation Technology: Acceleo
5.3.5 Contributions
5.4 Conclusion
6 Translating ATL Transformations to Algebraic Graph Transformations
6.1 Introduction
6.2 Semantics of ATL
6.3 Semantics of AGT
6.4 Challenges of the Translation
6.5 Translating ATL to AGT
6.5.1 General Translation Scheme
6.5.2 Translating the ATL Resolve Mechanisms
6.5.3 Final Cleanup Phase
6.6 Translating OCL Guards and Binding Expressions
6.6.1 General Principles of the Existing Translation
6.6.2 Supporting Ordered Sets
6.7 Implementation
6.8 RelatedWork
6.9 Conclusion
7 Transforming Postconditions to Preconditions
7.1 Introduction
7.2 Background and Scope
7.3 Fundamentals of AGT
7.4 Properties of Preconditions
7.5 Weakest Liberal Precondition Construction
7.5.1 Basic NGC Transformations
7.5.2 The wlp Construction
7.6 Bounded Programs and Finite Liberal Preconditions
7.6.1 Bounded Iteration with Finite wlp
7.6.2 wlp of Bounded Programs
7.6.3 Scope of the BoundedWeakest Liberal Precondition
7.6.4 From Bounded wlp to Non-Bounded Liberal Preconditions
7.6.5 Discussion
7.7 RelatedWork
7.8 Conclusion
8 Implementation and Simplification Strategies for wlp
8.1 Introduction
8.2 Implementing Graph Overlapping
8.3 Complexity of Graph Overlapping
8.4 Simplification Strategies for Taming Combinatorial Explosion
8.4.1 NGC and Standard Logic Properties
8.4.2 Rule Selection
8.4.3 ATL Semantics
8.4.4 Element Creation
8.5 Combining A and L for Early Simplification – Post2Le f t
8.6 Parallelisation and Memory Management
8.7 Conclusion
9 Template-based Specification of Model-to-Text Transformations
9.1 Introduction
9.2 Use Case: Simulink to C Code Generation in QGen
9.2.1 Semantics of Simulink Models
9.2.2 Implementation of Simulink Semantics in Source Code
9.2.3 General Structure of the Generated Code
9.3 Specification Templates and Queries
9.4 Organisation of the Specification
9.4.1 SimpleSimulink Metamodel
9.4.2 Library of Simulink Concepts
9.4.3 Library of Common Definition and Regular Expressions
9.5 Tool Operational Requirements
9.5.1 Defining Configuration Parameters
9.5.2 Specifying Code Patterns
9.6 Automatic Test Oracles
9.6.1 Determining Test Outcomes
9.6.2 Resolving Failed Tests
9.7 Document Generation: a Higher-Order Transformation
9.8 RelatedWork
9.9 Conclusion
10 Experimental Validation
10.1 Introduction
10.2 Validation of ATL2AGT
10.2.1 Functional Validation Using Back-to-Back Testing
10.2.2 Discussion on the Thoroughness of Validation
10.2.3 Discussion on Performance
10.3 Validation of Post2Pre
10.3.1 Functional Validation
10.3.2 Overview of the Scalability Problem and Current Status
10.3.3 Concrete Observation of Scalability Issues
10.3.4 Assessment of Simplification Strategies
10.3.5 Larger Examples and Discussion on Complexity
10.3.6 Parallelism and Memory Management
10.3.7 Concluding Remarks
10.4 Validation of Model-to-Code Specification and Test Oracles Approach
10.4.1 Deployment of the Approach
10.4.2 Feedback and Lessons Learned
10.4.3 Addressing the Variability and Completeness of the Specification
10.5 Conclusion
11 Conclusions and FutureWork
11.1 Summary of Contributions
11.1.1 Backward Translation of Test Requirements
11.1.2 Specification-based Test Oracles for Integration Tests
11.2 Summary of Scope of Applicability
11.3 Limitations and Future Work
11.4 Long-term Perspectives
Appendix A Examples ofWeakest Liberal Preconditions
A.1 Reminder of the ATL Transformation
A.2 Example 1
A.3 Example 2
A.4 Example 3
Bibliography