Skip to content

Commit

Permalink
added model based testing documentation
Browse files Browse the repository at this point in the history 
fixed inclusion of epilog.rst
  • Loading branch information
@harcokuppens
harcokuppens committed Sep 23, 2021
1 parent aec3c16 commit 0eb28e6
Show file tree
Hide file tree
Showing 23 changed files with 3,612 additions and 113 deletions.
296 changes: 293 additions & 3 deletions source/bibliography.rst
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,295 @@
Bibliography
=======================================================


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

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] R. 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 Hypoth`eses 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.
1 change: 1 addition & 0 deletions source/command-line.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ solver being used, which we can create using the following commands:
echo 'selected-solver: "cvc4" ' > ~/.torxakis.yaml
From now on ``TorXakis`` will use
`CVC4 <http://cvc4.cs.stanford.edu/>`__ instead of
`Z3 <https://github.com/Z3Prover/z3>`__.
Expand Down
23 changes: 19 additions & 4 deletions source/conf.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,19 +65,34 @@ def __init__(self, **options):
exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']


# internal linking :ref:linkname
# using :ref: we can use sphinx cross referencing in a sphinx document (between possible different rst files in sphinx project)
# however :ref: is only used for internal linking, for external linking you must use the standard restructured text
# however :ref: is only used for internal linking,
#
# external linking linkname_
# for external linking you must use the standard restructured text
# syntax using a role with an ending _ character. You can even separate the link and the target definition.
# However the target definition from standard restructured text only holds for the current rst file.
# ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# The trick to have target definitions hold for all rst files in the sphinx project is to include to each
# rst file the target definitions. We do this by adding an include directive for including hyperlinks.rst
# to the rst_epilog, so that hyperlinks.rst is then automatically include to rst file.
#
#rst_epilog="""
#.. include:: hyperlinks.rst
#"""
rst_epilog="""
.. include:: /epilog.rst
"""
# note: officially include directive only supports a relative file argument
# https://docutils.sourceforge.io/docs/ref/rst/directives.html#including-an-external-document-fragment
# The "include" directive reads a text file. The directive argument is the path to the file to be included,
# relative to the document containing the directive.Unless the options literal, code, or parser are given,
# the file is parsed in the current document's context at the point of the directive.
# however https://stackoverflow.com/questions/44563794/how-to-correctly-include-other-rest-files-in-a-sphinx-project
# said an absolute path ( root is source/ dir) works also and I verified it!


# rst_prolog="""
# .. include:: /prolog.rst
# """

numfig = True

Expand Down
Loading

0 comments on commit 0eb28e6

Please sign in to comment.