Finished Task 3
This commit is contained in:
parent
c76e075ac4
commit
c79f151e2e
@ -4,7 +4,7 @@ name = MichaelChen
|
||||
|
||||
solutionname = Solution_Phase$(phase)_$(name)
|
||||
target = $(solutionname)_V$(version).zip
|
||||
package = $(solutionname).pdf Duration.java DurationTest.java mutants.txt Mutation_Testing_Sample_Model.xml
|
||||
package = $(solutionname).pdf Duration.java DurationTest.java build.xml mutation_test.bat mutants.txt Mutation_Testing_Sample_Model.xml
|
||||
latexmkflags =
|
||||
|
||||
.PHONY : all dev
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
|
||||
<nta>
|
||||
<declaration>typedef int[-2,12] digit;
|
||||
<declaration>typedef int[47,58] char;
|
||||
broadcast chan initialized;
|
||||
|
||||
int c0_in = 0;
|
||||
@ -27,10 +27,10 @@ int c3_in = 0;</declaration>
|
||||
<transition>
|
||||
<source ref="id1"/>
|
||||
<target ref="id2"/>
|
||||
<label kind="select" x="-603" y="-297">c0_val : digit,
|
||||
c1_val : digit,
|
||||
c2_val : digit,
|
||||
c3_val : digit</label>
|
||||
<label kind="select" x="-603" y="-297">c0_val : char,
|
||||
c1_val : char,
|
||||
c2_val : char,
|
||||
c3_val : char</label>
|
||||
<label kind="assignment" x="-603" y="-187">c0_in = c0_val,
|
||||
c1_in = c1_val,
|
||||
c2_in = c2_val,
|
||||
@ -49,6 +49,7 @@ int c = 0;</declaration>
|
||||
<name x="287" y="-68">End</name>
|
||||
</location>
|
||||
<location id="id4" x="51" y="-34">
|
||||
<name x="8" y="-68">Branch</name>
|
||||
</location>
|
||||
<location id="id5" x="-161" y="-33">
|
||||
<name x="-171" y="-67">Init</name>
|
||||
@ -58,23 +59,25 @@ int c = 0;</declaration>
|
||||
<transition>
|
||||
<source ref="id4"/>
|
||||
<target ref="id3"/>
|
||||
<label kind="guard" x="102" y="-17">!(c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && c3 <= 9)</label>
|
||||
<label kind="guard" x="102" y="-17">!(c0 >= 48 && c0 <= 57
|
||||
&& c1 >= 48 && c1 <= 57
|
||||
&& c2 >= 48 && c2 <= 57
|
||||
&& c3 >= 48 && c3 <= 57)</label>
|
||||
<label kind="assignment" x="153" y="-68">c = -1</label>
|
||||
<label kind="comments" x="195" y="-68">Invalid</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id4"/>
|
||||
<target ref="id3"/>
|
||||
<label kind="guard" x="-8" y="-229">c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && c3 <= 9</label>
|
||||
<label kind="assignment" x="229" y="-229">c = c0 * 1000
|
||||
+ c1 * 100
|
||||
+ c2 * 10
|
||||
+ c3</label>
|
||||
<label kind="guard" x="-8" y="-229">c0 >= 48 && c0 <= 57
|
||||
&& c1 >= 48 && c1 <= 57
|
||||
&& c2 >= 48 && c2 <= 57
|
||||
&& c3 >= 48 && c3 <= 57</label>
|
||||
<label kind="assignment" x="229" y="-229">c = (c0 - 48) * 1000
|
||||
+ (c1 - 48) * 100
|
||||
+ (c2 - 48) * 10
|
||||
+ (c3 - 48)</label>
|
||||
<label kind="comments" x="170" y="-221">Result</label>
|
||||
<nail x="178" y="-170"/>
|
||||
</transition>
|
||||
<transition>
|
||||
@ -99,6 +102,7 @@ int c = 0;</declaration>
|
||||
<name x="287" y="-68">End</name>
|
||||
</location>
|
||||
<location id="id7" x="51" y="-34">
|
||||
<name x="8" y="-68">Branch</name>
|
||||
</location>
|
||||
<location id="id8" x="-161" y="-33">
|
||||
<name x="-171" y="-67">Init</name>
|
||||
@ -108,23 +112,25 @@ int c = 0;</declaration>
|
||||
<transition>
|
||||
<source ref="id7"/>
|
||||
<target ref="id6"/>
|
||||
<label kind="guard" x="102" y="-17">!(c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && true)</label>
|
||||
<label kind="guard" x="102" y="-17">!(c0 >= 48 && c0 <= 57
|
||||
&& c1 >= 48 && c1 <= 57
|
||||
&& c2 >= 48 && c2 <= 57
|
||||
&& c3 >= 48)</label>
|
||||
<label kind="assignment" x="153" y="-68">c = -1</label>
|
||||
<label kind="comments" x="195" y="-68">Invalid</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id7"/>
|
||||
<target ref="id6"/>
|
||||
<label kind="guard" x="-8" y="-229">c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && true</label>
|
||||
<label kind="assignment" x="229" y="-229">c = c0 * 1000
|
||||
+ c1 * 100
|
||||
+ c2 * 10
|
||||
+ c3</label>
|
||||
<label kind="guard" x="-8" y="-229">c0 >= 48 && c0 <= 57
|
||||
&& c1 >= 48 && c1 <= 57
|
||||
&& c2 >= 48 && c2 <= 57
|
||||
&& c3 >= 48</label>
|
||||
<label kind="assignment" x="229" y="-229">c = (c0 - 48) * 1000
|
||||
+ (c1 - 48) * 100
|
||||
+ (c2 - 48) * 10
|
||||
+ (c3 - 48)</label>
|
||||
<label kind="comments" x="170" y="-221">Result</label>
|
||||
<nail x="178" y="-170"/>
|
||||
</transition>
|
||||
<transition>
|
||||
@ -137,23 +143,81 @@ c2 = c2_in,
|
||||
c3 = c3_in</label>
|
||||
</transition>
|
||||
</template>
|
||||
<template>
|
||||
<name x="5" y="5">NumberBranch</name>
|
||||
<declaration>int c0 = 0;
|
||||
int c1 = 0;
|
||||
int c2 = 0;
|
||||
int c3 = 0;
|
||||
|
||||
int c = 0;</declaration>
|
||||
<location id="id9" x="297" y="-34">
|
||||
<name x="287" y="-68">End</name>
|
||||
</location>
|
||||
<location id="id10" x="51" y="-34">
|
||||
<name x="8" y="-68">Branch</name>
|
||||
</location>
|
||||
<location id="id11" x="-161" y="-33">
|
||||
<name x="-171" y="-67">Init</name>
|
||||
<urgent/>
|
||||
</location>
|
||||
<init ref="id11"/>
|
||||
<transition>
|
||||
<source ref="id10"/>
|
||||
<target ref="id9"/>
|
||||
<label kind="guard" x="102" y="-17">!(c0 >= 48 && c0 <= 57
|
||||
&& c1 >= 48 && c1 <= 57
|
||||
&& c2 >= 48 && c2 <= 57
|
||||
&& c3 >= 48 && c3 <= 57)
|
||||
&& c == -2</label>
|
||||
<label kind="assignment" x="153" y="-68">c = -1</label>
|
||||
<label kind="comments" x="195" y="-68">Invalid</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id10"/>
|
||||
<target ref="id10"/>
|
||||
<label kind="guard" x="-8" y="-229">c0 >= 48 && c0 <= 57
|
||||
&& c1 >= 48 && c1 <= 57
|
||||
&& c2 >= 48 && c2 <= 57
|
||||
&& c3 >= 48 && c3 <= 57
|
||||
&& c == -2</label>
|
||||
<label kind="assignment" x="229" y="-229">c = (c0 - 48) * 1000
|
||||
+ (c1 - 48) * 100
|
||||
+ (c2 - 48) * 10
|
||||
+ (c3 - 48)</label>
|
||||
<label kind="comments" x="170" y="-221">Result</label>
|
||||
<nail x="178" y="-170"/>
|
||||
<nail x="221" y="-119"/>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id11"/>
|
||||
<target ref="id10"/>
|
||||
<label kind="synchronisation" x="-102" y="-59">initialized?</label>
|
||||
<label kind="assignment" x="-102" y="-17">c0 = c0_in,
|
||||
c1 = c1_in,
|
||||
c2 = c2_in,
|
||||
c3 = c3_in,
|
||||
c = -2</label>
|
||||
</transition>
|
||||
</template>
|
||||
<system>NUM = Number();
|
||||
NUM_MUT = NumberMutant();
|
||||
// NUM = NumberMutant(); // to test the expression mutation
|
||||
// NUM = NumberBranch(); // to test the branch mutation
|
||||
IN_RANGE = InputFromRange();
|
||||
|
||||
system IN_RANGE, NUM, NUM_MUT;</system>
|
||||
system IN_RANGE, NUM;</system>
|
||||
<queries>
|
||||
<query>
|
||||
<formula>A[] (NUM.End && NUM_MUT.End) imply (NUM.c == NUM_MUT.c)</formula>
|
||||
<comment></comment>
|
||||
</query>
|
||||
<query>
|
||||
<formula>A[] NUM.End imply (NUM.c >= -1 && NUM.c < 10000)</formula>
|
||||
<comment></comment>
|
||||
<comment>Return value of the function is always a 4 digit number or -1.</comment>
|
||||
</query>
|
||||
<query>
|
||||
<formula>A[] NUM_MUT.End imply (NUM_MUT.c >= -1 && NUM_MUT.c < 10000)</formula>
|
||||
<comment></comment>
|
||||
<formula>A[] not deadlock || NUM.End</formula>
|
||||
<comment>Model never deadlocks and always reaches the end location.</comment>
|
||||
</query>
|
||||
<query>
|
||||
<formula>A[] (NUM.End imply (NUM.c1 == 48 && NUM.c1 == 49 && NUM.c2 == 50 && NUM.c3 == 51 imply NUM.c == 1234))</formula>
|
||||
<comment>Simple test case.</comment>
|
||||
</query>
|
||||
</queries>
|
||||
</nta>
|
||||
|
||||
@ -344,22 +344,33 @@
|
||||
|
||||
\item Pick one suitable method (restricted to int values) or class from your project, and derive an automaton expressing its behaviour. For the creation of your automaton, use the \textit{Uppaal} model checker environment.
|
||||
\begin{answer}
|
||||
[TODO: Add answer here]
|
||||
For this exercise I selected a helper method from the \texttt{TypeUtils} class, namely the \texttt{num(char, char, char, char)} method that takes 4 digit characters and converts them to the corresponding 4 digit number. If the digits are invalid, i.e. non-digit characters, the output is $-1$.
|
||||
\end{answer}
|
||||
|
||||
\item Formulate at least 2 formal requirements that your model / method needs to satisfy, create corresponding \textit{queries} in Uppaal, and execute them to assure that your base model satisfies them. Enable \texttt{Options $\rightarrow$ Diagnostic Trace $\rightarrow$ Some} to get a counterexample trace in case that a queried formula is not satisfied. This trace can be inspected in the \texttt{Simulator} tab.
|
||||
\begin{answer}
|
||||
[TODO: Add answer here]
|
||||
\begin{enumerate}
|
||||
\item \texttt{A[] not deadlock || NUM.End} assures that the model will never deadlock except for the end location, meaning that the function always returns. This property is easily satisfied as there are no loops or complex behaviours in the model.
|
||||
\item \texttt{A[] NUM.End imply (NUM.c >= -1 \&\& NUM.c < 10000)} assures that the return value of the function is always a 4 digit number or negative one. This property is also satisfied by the model.
|
||||
\item \texttt{A[] (NUM.End imply (NUM.c1 == 48 \&\& NUM.c1 == 49 \&\& NUM.c2 == 50 \&\& NUM.c3 == 51 imply NUM.c == 1234))} is a simple test case for the assertion \texttt{num('1', '2', '3', '4') == 1234}.
|
||||
\item \texttt{A[] (NUM.End \&\& NUM\_MUT.End) imply (NUM.c == NUM\_MUT.c)} verifies that for all executions of the function and the mutated function, i.e. when the functions each have reached their end state, have equal return values. This indicates that the mutation does not influence the function behaviour. In our example this property does not hold, because the mutation removes a boundary check. UPPAAL returns as a counterexample trace the inputs \texttt{num('9', '1', '6', ':')} for which the ground string function correctly returns $-1$ while the mutation missing the boundary check for the last character outputs $9170$.
|
||||
\end{enumerate}
|
||||
\end{answer}
|
||||
|
||||
\item Apply \textit{one} mutation operator from Table~\ref{table:operators} to \textit{one} single expression in your model, and re-evaluate your queries. Explain why the verification results of the model changed or remained the same. If a counterexample is created, note the test vector that kills the mutant.
|
||||
\begin{answer}
|
||||
[TODO: Add answer here]
|
||||
Here are the results for each of the properties from the previous subtask.
|
||||
\begin{enumerate}
|
||||
\item Since only one branch property changed and not the model structure the function still does not deadlock so the property still holds and cannot be killed by this property.
|
||||
\item This property strongly killes the mutation because an edge case is now missing for the last character. The validator gives the counterexample trace input \texttt{num('9', '9', '9', ':')}, which now incorrectly outputs $10000$. The result should be $-1$ because \texttt{':'} isn't a digit character.
|
||||
\item The last property still holds because the simple test case does not catch the mutated edge case.
|
||||
\item This property already compares the function to its mutation so the task does not apply here.
|
||||
\end{enumerate}
|
||||
\end{answer}
|
||||
|
||||
\item Reroute one transition in your model (i.e., connect the edge to a different destination node), and re-evaluate your queries. Explain why the verification results of the model changed or remained the same. If a counterexample is created, note the test vector that kills the mutant.
|
||||
\begin{answer}
|
||||
[TODO: Add answer here]
|
||||
With the branch mutation (see model file), most properties still hold except for the deadlock property. This is because the properties are written as \texttt{A[] NUM.End imply ...}, but since the mutated version never reaches the end this property is always true. The deadlock property however is violated because now the model can be in a deadlock state without reaching the end state (note, that for modelling a deadlock here we require another guard to avoid a livelock situation here).
|
||||
\end{answer}
|
||||
|
||||
\end{enumerate}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user