From cfd2dc332edc36040b5869595b7398d092369ea9 Mon Sep 17 00:00:00 2001 From: pimjager Date: Thu, 10 Dec 2015 16:58:47 +0100 Subject: [PATCH] Investigation improved, added conclusion which model we will use --- a3/1modelinvestigation.tex | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/a3/1modelinvestigation.tex b/a3/1modelinvestigation.tex index e8d10c9..f0f6718 100644 --- a/a3/1modelinvestigation.tex +++ b/a3/1modelinvestigation.tex @@ -12,11 +12,16 @@ be a fitting model for our SUT as the behaviour of TCP is such that a TCP client is in a certain state (connection closed, listening, connection established, etc.) and the TCP client transitions between those states based upon input coming from another connected client. -In this case an LTS, in which the interactions would be initiated by the -remote client, would be a fitting model for our SUT. +In this case an LTS, would be a fitting model for our SUT. An LTS would not be a fitting model in case it would be desirable to model the behaviour when wrong input (such as wrong sequence numbers) is given to the SUT. +An LTS could model this behaviour, but more expressive models exists (see below) +which would limit the size of the model. + +In this case we chose to model the SUT as a LTS. Since LTSs provide the +functionality to express the desired properties of the SUT, that is, that the +SUT transitions through states as described in the TCP specification. \paragraph{Mealy Machines} Mealy Machines are an extension of LTS in which each label is a tuple of input -- 2.20.1