@article{
	elib_6068,
	author = {Robert Sachtleben},
	title = {An approach for the verification and synthesis of complete test generation  algorithms for finite state machines},
	year = {2022},
	keywords = {Isabelle; theorem proving; finite state machine; complete test strategy; Model-based Testing; },
	doi = {10.26092/elib/1665},	
}


@inproceedings{DBLP:conf/hase/PetrenkoY14,
  author    = {Alexandre Petrenko and
               Nina Yevtushenko},
  title     = {Adaptive Testing of Nondeterministic Systems with {FSM}},
  booktitle = {15th International {IEEE} Symposium on High-Assurance Systems Engineering,
               {HASE} 2014, Miami Beach, FL, USA, January 9-11, 2014},
  pages     = {224--228},
  year      = {2014},
  url       = {http://dx.doi.org/10.1109/HASE.2014.39},
  doi       = {10.1109/HASE.2014.39},
  timestamp = {Tue, 02 Dec 2014 17:13:29 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hase/PetrenkoY14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@InProceedings{Sachtleben2019,
    author="Sachtleben, Robert
    and Hierons, Robert M.
    and Huang, Wen-ling
    and Peleska, Jan",
    editor="Gaston, Christophe
    and Kosmatov, Nikolai
    and Le Gall, Pascale",
    title="A Mechanised Proof of an Adaptive State Counting Algorithm",
    booktitle="Testing Software and Systems",
    year="2019",
    publisher="Springer International Publishing",
    address="Cham",
    pages="176--193",
    abstract="In this paper it is demonstrated that the capabilities of state-of-the-art proof assistant tools are sufficient to present mechanised and, at the same time, human-readable proofs establishing completeness properties of test methods and the correctness of associated test generation algorithms. To this end, the well-known Isabelle/HOL proof assistant is used to mechanically verify a complete test theory elaborated by the second author for checking the reduction conformance relation between a possibly nondeterministic finite state machine (FSM) serving as reference model and an implementation whose behaviour can also be represented by an FSM. The formalisation also helps to clarify an ambiguity in the original test generation algorithm which was specified in natural language and could be misinterpreted in a way leading to insufficient fault coverage.",
    isbn="978-3-030-31280-0"
}


@article{Adaptive_State_Counting-AFP,
  author  = {Robert Sachtleben},
  title   = {Formalisation of an Adaptive State Counting Algorithm},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/Adaptive_State_Counting.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@incollection{luo_selecting_1995,
	location = {Boston, {MA}},
	title = {Selecting Test Sequences for Partially-Specified Nondeterministic Finite State Machines},
	isbn = {978-0-387-34883-4},
	url = {https://doi.org/10.1007/978-0-387-34883-4_6},
	series = {{IFIP} - The International Federation for Information Processing},
	pages = {95--110},
	booktitle = {Protocol Test Systems: 7th workshop 7th {IFIP} {WG} 6.1 international workshop on protocol text systems},
	publisher = {Springer {US}},
	author = {Luo, Gang and Petrenko, Alexandre and v. Bochmann, Gregor},
	editor = {Mizuno, Tadanori and Higashino, Teruo and Shiratori, Norio},
	date = {1995},
	langid = {english},
	doi = {10.1007/978-0-387-34883-4_6},
	keywords = {C.2.2, D.2.5, Network Protocols, Testing and Debugging},
}

@article{chow:wmethod,
	Author = {Tsun S. Chow},
	Journal = {IEEE Transactions on Software Engineering},
	Month = mar,
	Number = {3},
	Pages = {178--186},
	Title = {Testing Software Design Modeled by Finite-State Machines},
	Volume = {SE-4},
	Year = {1978}}

  @article{luo_test_1994,
	title = {Test selection based on communicating nondeterministic finite-state machines using a generalized Wp-method},
	volume = {20},
	issn = {0098-5589},
	doi = {10.1109/32.265636},
	pages = {149--162},
	number = {2},
	journal = {{IEEE} Transactions on Software Engineering},
	author = {Luo, G. and Bochmann, G.V. and Petrenko, A.},
	year = {1994}
	
}

@book{PeleskaHuangLectureNotesMBT,
	Author = {Peleska, Jan and Huang, Wen-ling},
	Month = {January},
	Note = {Lecture notes, available under \url{http://www.informatik.uni-bremen.de/agbs/jp/papers/test-automation-huang-peleska.pdf}},
	Publisher = {University of Bremen},
	Title = {Test Automation - Foundations and Applications of Model-based Testing},
	Year = {2019}}

@inproceedings{DBLP:conf/forte/DorofeevaEY05,
  author    = {Rita Dorofeeva and
               Khaled El{-}Fakih and
               Nina Yevtushenko},
  shorthand={{Dorofeeva et al(2005)}},
  title     = {An Improved Conformance Testing Method},
  booktitle = {Formal Techniques for Networked and Distributed Systems - {FORTE}
               2005, 25th {IFIP} {WG} 6.1 International Conference, Taipei, Taiwan,
               October 2-5, 2005, Proceedings},
  pages     = {204--218},
  year      = {2005},
  crossref  = {DBLP:conf/forte/2005},
  url       = {https://doi.org/10.1007/11562436_16},
  doi       = {10.1007/11562436_16},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/forte/DorofeevaEY05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}  

@article{simao_reducing_2012,
	title = {On reducing test length for {FSMs} with extra states},
	volume = {22},
	copyright = {Copyright © 2011 John Wiley \& Sons, Ltd.},
	issn = {1099-1689},
	url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.452},
	doi = {10.1002/stvr.452},
	abstract = {A long-standing problem when testing from a deterministic finite state machine is to guarantee full fault coverage even if the faults introduce extra states in the implementations. It is well known that such tests should include the sequences in a traversal set which contains all input sequences of length defined by the number of extra states. This paper suggests the SPY method, which helps reduce the length of tests by distributing sequences of the traversal set and reducing test branching. It is also demonstrated that an additional assumption about the implementation under test relaxes the requirement of the complete traversal set. The results of the experimental comparison of the proposed method with an existing method indicate that the resulting reduction can reach 40\%. Experimental results suggest that the additional assumption about the implementation can help in further reducing the test suite length. Copyright © 2011 John Wiley \& Sons, Ltd.},
	language = {en},
	number = {6},
	urldate = {2018-05-06},
	journal = {Software Testing, Verification and Reliability},
	author = {Simão, Adenilso and Petrenko, Alexandre and Yevtushenko, Nina},
	month = sep,
	year = {2012},
	keywords = {test generation, finite state machines, fault domain},
	pages = {435--454}
}

@INPROCEEDINGS{Soucha2018,
  author={M. {Soucha} and K. {Bogdanov}},
  booktitle={2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)}, 
  title={{SPYH}-Method: An Improvement in Testing of Finite-State Machines}, 
  year={2018},
  volume={},
  number={},
  pages={194-203},
  doi={10.1109/ICSTW.2018.00050}  
}

@proceedings{DBLP:conf/forte/2005,
  editor    = {Farn Wang},
  title     = {Formal Techniques for Networked and Distributed Systems - {FORTE}
               2005, 25th {IFIP} {WG} 6.1 International Conference, Taipei, Taiwan,
               October 2-5, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3731},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11562436},
  doi       = {10.1007/11562436},
  isbn      = {3-540-29189-X},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/forte/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}