Skip navigation
SuUB logo
DSpace logo

  • Home
  • Institutions
    • University of Bremen
    • City University of Applied Sciences
    • Bremerhaven University of Applied Sciences
  • Sign on to:
    • My Media
    • Receive email
      updates
    • Edit Account details

Citation link: https://doi.org/10.26092/elib/1665
Dissertation_Robert_Sachtleben.pdf
OpenAccess
 
by 4.0

An approach for the verification and synthesis of complete test generation algorithms for finite state machines


File Description SizeFormat
Dissertation_Robert_Sachtleben.pdf2.35 MBAdobe PDFView/Open
Authors: Sachtleben, Robert  
Supervisor: Peleska, Jan  
1. Expert: Peleska, Jan  
Experts: Wolff, Burkhart 
Abstract: 
Complete test suites are of special interest in the field of model-based testing, as they guarantee high fault detection capabilities under well-specified assumptions. The variety and complexity of strategies generating complete test suites, their implementations, and their completeness proofs impose difficulties upon manual verification. Furthermore, ambiguities or only implicitly specified assumptions in natural language descriptions and proofs easily lead to implementations that do not generate complete test suites.

The present dissertation proposes an alternative approach to the verification and implementation of test strategies that generate complete test suites for testing for language-equivalence on finite state machines, that employs the interactive theorem prover Isabelle.

In the first part of this work, similarities and differences between steps performed by the considered test strategies are identified. From these, a framework is derived as a higher order function capable of representing all considered strategies as concrete applications of it. Several implementations of parameters of this framework are shared between multiple strategies. Additional frameworks are developed to support alternative completeness proofs.

The second part of this work defines finite state machines, their properties and operations, as well as the frameworks in Isabelle/HOL and respectively proves them correct and complete. Completeness proofs over frameworks are decoupled from concrete implementations of their parameters by suitable interfaces. This approach enables the reuse of proofs between similar strategies and thus simplifies completeness proofs for new variations on already handled strategies.

Finally, the definitions in Isabelle are employed to automatically generate provably correct implementations of the considered test strategies. It is shown that these exhibit comparable performance to a manually developed C++ library for certain inputs.
Keywords: Isabelle; theorem proving; finite state machine; complete test strategy; Model-based Testing
Issue Date: 20-Jul-2022
Type: Dissertation
DOI: 10.26092/elib/1665
URN: urn:nbn:de:gbv:46-elib60689
Institution: Universität Bremen 
Faculty: Fachbereich 03: Mathematik/Informatik (FB 03) 
Appears in Collections:Dissertationen

  

Page view(s)

179
checked on Feb 3, 2023

Download(s)

75
checked on Feb 3, 2023

Google ScholarTM

Check


This item is licensed under a Creative Commons License Creative Commons

Legal notice -Feedback -Data privacy
Media - Extension maintained and optimized by Logo 4SCIENCE