Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2015 | Buch

Scalable Incremental Test-case Generation from Large Behavior Models Kapitel lesen Erstes Kapitel lesen

Tests and Proofs

9th International Conference, TAP 2015, Held as Part of STAF 2015, L’Aquila, Italy, July 22-24, 2015. Proceedings

herausgegeben von: Jasmin Christian Blanchette, Nikolai Kosmatov

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 9th International Conference on Tests and Proofs, TAP 2015, held in L` Aquila, Italy, in July 2015, as part of the STAF 2015 Federated Conferences. The 11 revised full papers and 1 short papers presented together with 3 invited talks were carefully reviewed and selected from 21 submissions. The accepted papers contribute to various testing techniques (model-based, property-based, grammar-based, bounded-exhaustive), fault localization, model-driven engineering, as well as model coverage, consistency and validation, among others. Many papers rely on interactive and automatic theorem provers, including SMT solvers and model checkers.

Inhaltsverzeichnis

Frontmatter
Scalable Incremental Test-case Generation from Large Behavior Models
Abstract
Model-based testing is a popular black-box testing technology that enables automation of test generation and execution, while achieving a given coverage. The application of this technology to large and complex systems is still a challenging problem, due to the state-space explosion resulting from the size of specification models.
In this paper, we evaluate a test-case generation approach that tackles this complexity along two axes. Firstly, our approach relies on a synchronous specification language for test models, thus avoiding the problem of interleaving actions. Secondly, our specification language enables incremental test-case generation by providing support for compositional modeling, in which each requirement or view of the system is expressed as a separate partial model. The individual requirement models are then naturally combined by conjunction, which is incrementally computed during the generation of tests.
We apply our test-case generation technique to two large industrial case studies: (1) an electronic control unit (ECU) of an agricultural device; and (2) a railway interlocking system. We demonstrate the scalability of our approach by creating a series of test models with increasing complexity and report on the experimental results.
Bernhard K. Aichernig, Dejan Ničković, Stefan Tiran
Test Case Generation for Concurrent Systems Using Event Structures
Abstract
This paper deals with the test-case generation problem for concurrent systems that are specified by true-concurrency models such as Petri nets. We show that using true-concurrency models reduces both the size and the number of test cases needed for achieving certain coverage criteria. We present a test-case generation algorithm based on Petri net unfoldings and a SAT encoding for solving controllability problems in test cases. Finally, we evaluate our algorithm against traditional test-case generation methods under interleaving semantics.
Konstantinos Athanasiou, Hernán Ponce-de-León, Stefan Schwoon
Fast Model-Based Fault Localisation with Test Suites
Abstract
Fault localisation, i.e. the identification of program locations that cause errors, takes significant effort and cost. We describe a fast model-based fault localisation algorithm which, given a test suite, uses symbolic execution methods to fully automatically identify a small subset of program locations where genuine program repairs exist. Our algorithm iterates over failing test cases and collects locations where an assignment change can repair exhibited faulty behaviour. Our main contribution is an improved search through the test suite, reducing the effort for the symbolic execution of the models and leading to speed-ups of more than two orders of magnitude over the previously published implementation by Griesmayer et al.
We implemented our algorithm for C programs, using the KLEE symbolic execution engine, and demonstrate its effectiveness on the Siemens TCAS variants. Its performance is in line with recent alternative model-based fault localisation techniques, but narrows the location set further without rejecting any genuine repair locations where faults can be fixed by changing a single assignment.
Geoff Birch, Bernd Fischer, Michael R. Poppleton
Case Study: Automatic Test Case Generation for a Secure Cache Implementation
Abstract
While many approaches for automatic test case generation have been proposed over the years, it is often difficult to predict which of them may work well on concrete problems. In this paper, we therefore present a case study in automatic, model-based test case generation: We implemented several graph-based methods that compute test cases with a model checker using trap properties, and evaluate these methods on a Secure Block Device implementation. We compare the number of generated test cases, the required generation time and the achieved code coverage. Our conclusions are twofold: First, automatic test case generation is feasible and beneficial for this case study, and even found a real bug in the implementation. Second, simple coverage methods on the model may already yield test suites of sufficient quality.
Roderick Bloem, Daniel Hein, Franz Röck, Richard Schumi
Verifying Code Generation Tools for the B-Method Using Tests: A Case Study
Abstract
In this paper, we present a case study where two code generators for the B-Method were validated using software testing techniques. Our testing strategy is a combination of Grammar-Based Testing (GBT) and Model-Based Testing (MBT) techniques. The strategy consists of two steps. In the first step, grammar-based coverage criteria are used to generate a wide and meaningful set of test input models to validate the parsing capabilities of the code generators. In the second step, a MBT tool is used to validate the correctness of the output produced by these tools. The MBT tool generates a set of tests based on the same input model used by the code generation tools. The generated code is considered correct (consistent with the input model) if it passes this set of tests. Using this testing strategy, we were able to find problems in both code generation tools with moderate effort.
Anamaria M. Moreira, Cleverton Hentz, David Déharbe, Ernesto C. B. de Matos, João B. Souza Neto, Valério de Medeiros Jr.
Software Validation via Model Animation
Abstract
This paper explores a new approach to validating software implementations that have been produced from formally-verified algorithms. Although visual inspection gives some confidence that the implementations faithfully reflect the formal models, it does not provide complete assurance that the software is correct. The proposed approach, which is based on animation of formal specifications, compares the outputs computed by the software implementations on a given suite of input values to the outputs computed by the formal models on the same inputs, and determines if they are equal up to a given tolerance. The approach is illustrated on a prototype air traffic management system that computes simple kinematic trajectories for aircraft. Proofs for the mathematical models of the system’s algorithms are carried out in the Prototype Verification System (PVS). The animation tool PVSio is used to evaluate the formal models on a set of randomly generated test cases. Output values computed by PVSio are compared against output values computed by the actual software. This comparison improves the assurance that the translation from formal models to code is faithful and that, for example, floating point errors do not greatly affect correctness and safety properties.
Aaron M. Dutle, César A. Muñoz, Anthony J. Narkawicz, Ricky W. Butler
Sequential Generation of Structured Arrays and Its Deductive Verification
Abstract
A structured array is an array satisfying given constraints, such as being sorted or having no duplicate values. Generation of all arrays with a given structure up to some given length has many applications, including bounded exhaustive testing. A sequential generator of structured arrays can be defined by two C functions: the first one computes an initial array, and the second one steps from one array to the next one according to some total order on the set of arrays. We formally specify with ACSL annotations that the generated arrays satisfy the prescribed structural constraints (soundness property) and that the generation is in increasing lexicographic order (progress property). We refine this specification into two programming and specification patterns: one for generation in lexicographic order and one for generation by filtering the output of another generator. We distribute a library of generators instantiating these patterns. After adding suitable loop invariants we automatically prove the soundness and progress properties with the Frama-C platform.
Richard Genestier, Alain Giorgetti, Guillaume Petiot
Checking UML and OCL Model Consistency: An Experience Report on a Middle-Sized Case Study
Abstract
This contribution reports on a middle-sized case study in which the consistency of a UML and OCL class model is checked. The class model restrictions are expressed by UML multiplicity constraints and explicit, non-trivial OCL invariants. Our approach automatically constructs a valid system state that shows that the model can be instantiated and thus proves consistency, i.e., shows that the invariants together with the multiplicity constraints are not contradictory.
Martin Gogolla, Lars Hamann, Frank Hilken, Matthias Sedlmeier
A Constraint Optimisation Model for Analysis of Telecommunication Protocol Logs
Abstract
Testing a telecommunication protocol often requires protocol log analysis. A protocol log is a sequence of messages with timestamps. Protocol log analysis involves checking that the content of messages and timestamps are correct with respect to the protocol specification. We model a protocol specification using constraint programming (MiniZinc), and we present an approach where a constraint solver is used to perform protocol log analysis. Our case study is the Public Warning System service, which is a part of the Long Term Evolution (LTE) 4G standard. We were able to analyse logs containing more than 3000 messages with more than 4000 errors.
Olga Grinchtein, Mats Carlsson, Justin Pearson
Experimental Evaluation of a Novel Equivalence Class Partition Testing Strategy
Abstract
In this paper, a novel complete model-based equivalence class testing strategy is experimentally evaluated. This black-box strategy applies to deterministic systems with infinite input domains and finite internal state and output domains. It is complete with respect to a given fault model. This means that conforming behaviours will never be rejected, and all nonconforming behaviours inside a given fault domain will be uncovered. We investigate the question how this strategy performs for systems under test whose behaviours lie outside the fault domain. Furthermore, a strategy extension is presented, that is based on randomised data selection from input equivalence classes. While this extension is still complete with respect to the given fault domain, it also promises a higher test strength when applied against members outside this domain. This is confirmed by an experimental evaluation that compares mutation coverage achieved by the original and the extended strategy with the coverage obtained by random testing.
Felix Hübner, Wen-ling Huang, Jan Peleska
Testing Functional Requirements in UML Activity Diagrams
Abstract
In model driven engineering (MDE), models constitute the main artifacts of the software development process. From models defining structural and behavioral aspects of a software system implementation artifacts, such as source code, are automatically generated using model transformation techniques. However, a crucial issue in MDE is the quality of models, as any defect not captured at model level is transferred to the code level, where it requires more time and effort to be detected and corrected. This work is concerned with testing the functional correctness of models created with a subset of UML called fUML comprising class and activity diagrams. We present a testing framework for fUML, which enables modelers to verify the correct behavior of fUML activities.
Stefan Mijatov, Tanja Mayerhofer, Philip Langer, Gerti Kappel
Coverage of OCL Operation Specifications and Invariants
Abstract
We consider operation coverage of OCL operation specifications and invariants in class diagrams with respect to sequence diagrams. The coverage criteria are based on the operations that are executed from the sequence diagrams and their asserted OCL subexpressions. We propose an algorithm that automatically generates a set of sequence diagrams in order to maximise these coverage criteria. A model finder is leveraged for this purpose. As a result, also operations and constraints can be determined that can never be executed and asserted, respectively. Our algorithm has been implemented in the UML specification tool USE.
Mathias Soeken, Julia Seiter, Rolf Drechsler
Backmatter
Metadaten
Titel
Tests and Proofs
herausgegeben von
Jasmin Christian Blanchette
Nikolai Kosmatov
Copyright-Jahr
2015
Electronic ISBN
978-3-319-21215-9
Print ISBN
978-3-319-21214-2
DOI
https://doi.org/10.1007/978-3-319-21215-9

Premium Partner

    Bildnachweise