# Bibliography¶

R1

S. Abramsky. Observational Equivalence as a Testing Equivalence. Theoretical Computer Science , 53(3):225– 241, 1987.

R2

T. Arts, J. Hughes, J. Johansson, and U. Wiger. Testing Telecoms Software with Quviq Quickcheck. In ACM SIGPLAN Workshop on Erlang , ERLANG’06, pages 2–10. ACM, NY, USA, 2006.

R3

Axini. Testautomatisering. http://www.axini.com .

R4

C. Barrett, C.L. Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. ing, and C. Reynolds, A.and Tinelli. CVC4. In Computer Aided Verification – CAV 2011 , volume 6806 of Lecture Notes in Computer Science , pages 171–177. Springer-Verlag, 2011.

R5

A. Belinfante. JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution . In J. Esparza and R. Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems – TACAS 2010 , volume 6015 of Lecture Notes in Computer Science , pages 266–270. Springer, 2010.

R6

A. Belinfante, J. Feenstra, R.G. de Vries, J. Tretmans, N. Goga, L. Feijs, S. Mauw, and L. Heerink. Formal Test Automation: A Simple Experiment. In G. Csopaki, S. Dibuz, and K. Tarnay, editors, Int. Workshop on Testing of Communicating Systems 12 , pages 179–196. Kluwer Academic Publishers, 1999.

R7

G. Bernot, M. G. Gaudel, and B. Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal , 1991(November):387–405, 1991.

R8

M. van der Bijl, A. Rensink, and J. Tretmans. Compositional Testing with ioco . In A. Petrenko and A. Ulrich, editors, Formal Approaches to Software Testing – FATES 2003 , volume 2931 of Lecture Notes in Computer Science , pages 86–100. Springer-Verlag, 2004.

R9

Bijl, M. van der and Beek, H. van. Model-Based Testing in Safety-Critical Scaled Agile. Bits & Chips , August 2021.

R10

H.C. Bohnenkamp and M.I.A. Stoelinga. Quantitative Testing. In ACM & IEEE Int. Conf. on Embedded Software – EMSOFT’08 , pages 227–236. ACM, 2008.

R11

T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems , 14:25–59, 1987.

R12

P. van den Bos, R. Janssen, and J. Moerman. n -Complete Test Suites for IOCO . Software Quality Journal , 27(2):563–588, 2019.

R13

P. van den Bos and J. Tretmans. Coverage-Based Testing with Symbolic Transition Systems. In D. Beyer and C. Keller, editors, Tests and Proofs – TAP 2019 , volume 11823 of Lecture Notes in Computer Science , pages 64–82. Springer Int. Publishing, 2019.

R14

Bos, P. van den. Coverage and Games in Model-Based Testing . PhD thesis, Radboud University, Nijmegen, The Netherlands, 2020.

R15

L. Branda´n Briones and E. Brinksma. A Test Generation Framework for quiescent Real-Time Systems. In J. Grabowski and B. Nielsen, editors, Formal Approaches to Software Testing – FATES 2004 , volume 3395 of Lecture Notes in Computer Science , pages 64–78. Springer-Verlag, 2005.

R16

E. Brinksma. A Theory for the Derivation of Tests. In S. Aggarwal and K. Sabnani, editors, Protocol Specification, Testing, and Verification VIII , pages 63–74. North-Holland, 1988.

R17

E. Brinksma, R. Alderden, R. Langerak, J. van de Lagemaat, and J. Tretmans. A Formal Approach to Conformance Testing. In J. de Meer, L. Mackert, and W. Effelsberg, editors, Second Int. Workshop on Protocol Test Systems , pages 349–363. North-Holland, 1990.

R18

T.S. Chow. Testing Software Design Modeled by Finite-State Machines. IEEE Transactions on Software Engineering , 4(3):178–187, 1978.

R19

K. Claessen and J. Hughes. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In ACM SIGPLAN Int. Conf. on Functional Programming 2000 , ICFP’00, pages 268–279. ACM, NY, USA, 2000.

R20

D.R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial . GrammaTech, Inc., 2011.

R21

L. De Moura and N. Bjørner. Z3: An Efficient SMT Solver. In C.R. Ramakrishnan and J. Rehof, editors, Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems – TACAS 2008 , volume 4963 of Lecture Notes in Computer Science , pages 337–340. Springer, 2008.

R22

L. De Moura and N. Bjørner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM , 54(9):69–77, September 2011.

R23

R. De Nicola and M.C.B. Hennessy. Testing Equivalences for Processes. Theoretical Computer Science , 34:83–133, 1984.

R24

E.W. Dijkstra. Notes On Structured Programming – EWD249. T.H. Report 70-WSK-03, Technische Hogeschool Eindhoven, Eindhoven, The Netherlands, 1969.

R25

Dropbox. https://www.dropbox.com .

R26

H. Eertink. Executing LOTOS specifications: The SMILE tool. In T. Bolognesi, J. van de Lagemaat, and C. Vissers, editors, LOTOSphere: Software Development with LOTOS , pages 221–234. Kluwer Academic Publishers, 1995.

R27

P.H.J. van Eijk. Software Tools for the Specification Language LOTOS . PhD thesis, University of Twente, Enschede, The Netherlands, 1988.

R28

J. Engelfriet. Determinacy → (Observation Equivalence = Trace Equivalence). Theoretical Computer Science , 36(1):21–25, 1985.

R29

L. Frantzen, J. Tretmans, and T. Willemse. Test Generation Based on Symbolic Specifications. In J. Grabowski and B. Nielsen, editors, Formal Approaches to Software Testing – FATES 2004 , volume 3395 of Lecture Notes in Computer Science , pages 1–15. Springer-Verlag, 2005.

R30

L. Frantzen, J. Tretmans, and T.A.C. Willemse. A Symbolic Framework for Model-Based Testing. In K. Havelund, M. Nu´n˜ez, G. Ro¸su, and B. Wolff, editors, Formal Approaches to Software Testing and Runtime Verification – FATES/RV’06 , volume 4262 of Lecture Notes in Computer Science , pages 40–54. SpringerVerlag, 2006.

R31

M.-C. Gaudel. Testing can be Formal, too. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, TAPSOFT’95: Theory and Practice of Software Development , volume 915 of Lecture Notes in Computer Science , pages 82–96. Springer-Verlag, 1995.

R32

R.J. van Glabbeek. The Linear Time – Branching Time Spectrum. In J.C.M. Baeten and J.W. Klop, editors, CONCUR’90 , number 458 in Lecture Notes in Computer Science, pages 278–297. Springer-Verlag, 1990.

R33

R.J. van Glabbeek. The Linear Time – Branching Time Spectrum II (The Semantics of Sequential Systems with Silent Moves). In E. Best, editor, CONCUR’93 , number 715 in Lecture Notes in Computer Science, pages 66–81. Springer-Verlag, 1993.

R34

J.F. Groote and M.R. Mousavi. Modeling and Analysis of Communicating Systems . MIT Press, 2014.

R35

A. Hartman and K. Nagin. The AGEDIS Tools for Model Based Testing. In Int. Symposium on Software Testing and Analysis – ISSTA 2004 , pages 129–132, New York, USA, 2004. ACM Press.

R36

Haskell: An Advanced, Purely Functional Programming Language. https://www.haskell.org .

R37

L. Heerink. Ins and Outs in Refusal Testing . PhD thesis, University of Twente, Enschede, The Netherlands, 1998.

R38

A. Hessel, K.G. Larsen, M. Mikucionis, B. Nielsen, P. Pettersson, and A. Skou. Testing Real-Time Systems Using Uppaal . In R.M. Hierons, J.P. Bowen, and M. Harman, editors, Formal Methods and Testing , volume 4949 of Lecture Notes in Computer Science , pages 77–117. Springer-Verlag, 2008.

R39

C.A.R. Hoare. Communicating Sequential Processes . Prentice-Hall, 1985.

R40

J. Hughes, B.C. Pierce, T. Arts, and U. Norell. Mysteries of DropBox: Property-Based Testing of a Distributed Synchronization Service. In IEEE Int. Conf. on Software Testing, Verification and Validation – ICST , pages 135–145. IEEE, 2016.

R41

International Organization for Standardization. ISO/IEC 25010:2011 . Systems and software engineering – Systems and software Quality Requirements and Evaluation (SQuaRE) – System and software quality models. ISO, Geneva, 2011.

R42

ISO. Information Processing Systems, Open Systems Interconnection, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour . International Standard IS-8807. ISO, Geneve, 1989.

R43

R. Janssen and J. Tretmans. Matching Implementations to Specifications: The Corner Cases of ioco . In ACM/SIGAPP Symp. on Applied Computing – Software Verification and Testing Track , SAC’19, pages 2196–2205, New York, NY, USA, 2019. ACM.

R44

C. Jard and T. J´eron. TGV: Theory, Principles and Algorithms: A Tool for the Automatic Synthesis of Conformance Test Cases for Non-Deterministic Reactive Systems. Software Tools for Technology Transfer , 7(4):297–315, 2005.

R45

M. Krichen and S. Tripakis. Black-Box Conformance Testing for Real-Time Systems. In 11th Int. SPIN Workshop on Model Checking of Software – SPIN’04 , volume 2989 of Lecture Notes in Computer Science . Springer-Verlag, 2004.

R46

R. Langerak. A Testing Theory for LOTOS using Deadlock Detection. In E. Brinksma, G. Scollo, and C. A. Vissers, editors, Protocol Specification, Testing, and Verification IX , pages 87–98. North-Holland, 1990.

R47

D. Lee and M. Yannakakis. Principles and Methods for Testing Finite State Machines – A Survey. The Proceedings of the IEEE , 84(8):1090–1123, August 1996.

R48

N.A. Lynch and M.R. Tuttle. An Introduction to Input/Output Automata. CWI Quarterly , 2(3):219–246, 1989. Also: Technical Report MIT/LCS/TM-373 (TM-351 revised), Massachusetts Institute of Technology, Cambridge, U.S.A., 1988.

R49

L. Marsso, R. Mateescu, and W. Serwe. TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation. In D. Beyer and M. Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems – TACAS 2018 , volume 10806 of Lecture Notes in Computer Science , pages 211–228. Springer Int. Publishing, 2018.

R50
1. Milner. Communication and Concurrency . Prentice-Hall, 1989.

R51

A. Petrenko. Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography. In F. Cassez, C. Jard, B. Rozoy, and M.D. Ryan, editors, Modeling and Verification of Parallel Processes – 4th Summer School MOVEP 2000 , volume 2067 of Lecture Notes in Computer Science , pages 196–205. Springer-Verlag, 2001.

R52

M. Phalippou. Relations d’Implantation et Hypotheses de Test sur des Automates a Entr´ees et Sorties . PhD thesis, L’Universit´e de Bordeaux I, France, 1994.

R53

I. Phillips. Refusal Testing. Theoretical Computer Science , 50(2):241–284, 1987.

R54

A. Pnueli. Specification and development of reactive systems. In H.J. Kugler, editor, Information Processing 86 , pages 845–858. North-Holland, 1986.

R55

J.H. Poore, L. Lan, R. Eschbach, and T. Bauer. Automated Statistical Testing for Embedded Systems. In J. Zander, I. Schieferdecker, and P.J. Mosterman, editors, Model-Based Testing for Embedded Systems , pages 111–146. CRC Press, 2012.

R56

Selenium – Browser Automation. http://www.seleniumhq.org .

R57

Sikuli Script. http://www.sikuli.org .

R58

TorXakis – A Tool for Model-Based Testing. https://torxakis.org .

R59

J. Tretmans. HIPPO: A LOTOS Simulator. In P.H.J. van Eijk, C.A. Vissers, and M. Diaz, editors, The Formal Description Technique LOTOS , pages 391–396. North-Holland, 1989.

R60

J. Tretmans. Test Generation with Inputs, Outputs, and Quiescence. In T. Margaria and B. Steffen, editors, Second Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96) , pages 127–146. Lecture Notes in Computer Science 1055, Springer-Verlag, 1996.

R61

J. Tretmans. Test Generation with Inputs, Outputs and Repetitive Quiescence. Software—Concepts and Tools , 17(3):103–120, 1996.

R62

J. Tretmans. Model Based Testing with Labelled Transition Systems. In R.M. Hierons, J.P. Bowen, and M. Harman, editors, Formal Methods and Testing , volume 4949 of Lecture Notes in Computer Science , pages 1–38. Springer-Verlag, 2008.

R63

J. Tretmans and L. Verhaard. A Queue Model relating Synchronous and Asynchronous Communication. In R.J. Linn and M.U. Uyar, editors, Protocol Specification, Testing, and Verification XII , number C-8 in IFIP Transactions, pages 131–145. North-Holland, 1992.

R64

F. Vaandrager. On the Relationship between Process Algebra and Input/Output Automata. In Logic in Computer Science , pages 387–398. Sixth Annual IEEE Symposium, IEEE Computer Society Press, 1991.

R65

Vaandrager, F. Model Learning. Commun. ACM , 60(2):86–95, January 2017.

R66

M. Volpato and J. Tretmans. Towards Quality of Model-Based Testing in the ioco Framework. In Int. Workshop on Joining AcadeMiA and Industry Contributions to testing Automation – JAMAICA’13 , pages 41–46, New York, NY, USA, 2013. ACM.

R67

R.G. de Vries and J. Tretmans. Towards Formal Test Purposes. In E. Brinksma and J. Tretmans, editors, Formal Approaches to Testing of Software – FATES’01 , number NS-01-4 in BRICS Notes Series, pages 61–76, University of Aarhus, Denmark, 2001. BRICS.