Deployed e5eb9aa with MkDocs version: 1.6.0

introduction/index.html

@@ -875,10 +875,10 @@ <h1 id="what-is-hanfor">What is Hanfor?<a class="headerlink" href="#what-is-hanf
 <li>Requirement Check</li>
 <li>Test Generation</li>
 </ol>
-<p>
-<figure><img src="../img/hanfor_method.svg" title="Figure 1" /><figcaption>Figure 1: The Hanfor tool discovers requirement defects and derives test specifications from a given set of informal requirements.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/hanfor_method.svg" />
+  <figcaption>Figure 1: The Hanfor tool discovers requirement defects and derives test specifications from a given set of informal requirements.</figcaption>
 </figure>
-</p>
 <h2 id="requirement-formalization">Requirement Formalization<a class="headerlink" href="#requirement-formalization" title="Permanent link"> #</a></h2>
 <p>To make it possible for a computer to check a set of requirements for a given criteria, it has to "understand" the semantics of the requirements. This could be achieved by using formal languages, which usually share the fact that they are rarely understandable for humans.</p>
 <p>In this method we make use of a simple pattern language. The language is based on a restricted English grammar and hence looks like natural language. Requirements formalized in this specification language can automatically be translated into logics.</p>
@@ -953,10 +953,10 @@ <h3 id="specification-language">Specification Language<a class="headerlink" href
 </code></pre></div>
 </details>
 <p>Figure 2 shows the toolchain for the translation of an informal requirement into a formalized version. In the first step, the informal requirement, given in natural language, is translated into the specification language. This process is done manually. The requirement expressed in the specification language is then automatically translated into a formula in realtime logic (the Duration Calculus).</p>
-<p>
-<figure><img src="../img/toolchain_language.svg" title="Figure 2" /><figcaption>Figure 2: A specification language for real-time requirements is used as an intermediate step in the translation from informal to formalized requirements.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/toolchain_language.svg" />
+  <figcaption>Figure 2: A specification language for real-time requirements is used as an intermediate step in the translation from informal to formalized requirements.</figcaption>
 </figure>
-</p>
 <h2 id="requirement-check">Requirement Check<a class="headerlink" href="#requirement-check" title="Permanent link"> #</a></h2>
 <p>The <strong>Hanfor</strong> tool chain checks requirements for the following three correctness properties: </p>
 <ul>
@@ -985,15 +985,15 @@ <h3 id="realtime-consistency-rt-consistency">Realtime-consistency (rt-consistenc
 </ul>
 </div>
 <p>Consider the two real-time requirements given above. The set of the two requirements is consistent. Figure 3 gives an example of an interpretation of 'A', 'B', and 'C' (in form of a timing diagram) that satisfies both requirments.</p>
-<p>
-<figure><img src="../img/example_consistency.svg" title="Figure 3" /><figcaption>Figure 3: Consistency of the set of requirements {Req3, Req4}. 'A' and 'B' occur at the same point in time for one time unit, then '!C' for two time units satisfies Req4, and 'C' occurring at time 5 satisfies Req3.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/example_consistency.svg" />
+  <figcaption>Figure 3: Consistency of the set of requirements {Req3, Req4}. 'A' and 'B' occur at the same point in time for one time unit, then '!C' for two time units satisfies Req4, and 'C' occurring at time 5 satisfies Req3.</figcaption>
 </figure>
-</p>
 <p>However, there are assignments for which the requirements are in conflict, as depicted in the example trace (Figure 4). If 'A' and 'B'change values as shown in the figure, than at time 5, Req4 would only be satisfied if 'C' remained <em>false</em> while Req3 would only be satisfied if 'C' changed to <em>true</em>.</p>
-<p>
-<figure><img src="../img/example_rtinconsistency.svg" title="Figure 4" /><figcaption>Figure 4: Witness for the rt-inconsistency of the set of requirements {Req3, Req4}. From time 4 on, the system steers toward inevitable rt-inconsistency.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/example_rtinconsistency.svg" />
+  <figcaption>Figure 4: Witness for the rt-inconsistency of the set of requirements {Req3, Req4}. From time 4 on, the system steers toward inevitable rt-inconsistency.</figcaption>
 </figure>
-</p>
 <p>There are several possibilities to resolve the rt-inconsistency in a set of requirements, e.g. by erasing, changing or adding requirements.</p>
 <div class="admonition example">
 <p class="admonition-title">Example 2 (Cont.): Resolving rt-inconsistency</p>
@@ -1053,10 +1053,10 @@ <h2 id="test-generation">Test Generation<a class="headerlink" href="#test-genera
 <p>Formalized requirements can be used to automatically generate test specifications. An automatic test generation helps to reduce the time needed to write test specifications with a high coverage rate. The efficiency during development can be increased and the maintainability costs can be reduced.</p>
 <h3 id="algorithm">Algorithm<a class="headerlink" href="#algorithm" title="Permanent link"> #</a></h3>
 <p>Testing requires information about observability. The system variables are therefore categorized into input, output, and hidden (i.e. internal) variables. A sequence of inputs deterministically causes the valuation of the output variable. Figure 5 shows an abstract view of a two-input system with the variables <em>A</em>, <em>B</em> and <em>C</em>. </p>
-<p>
-<figure><img src="../img/hanfor_testing_system.svg" title="Figure 5" /><figcaption>Figure 5: System <em>S</em> with input variables <em>A</em>, <em>B</em>, and output variable <em>C</em>.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/hanfor_testing_system.svg" />
+  <figcaption>Figure 5: System *S* with input variables *A*, *B*, and output variable *C*.</figcaption>
 </figure>
-</p>
 <p>The test generation algorithm automatically generates system tests that are based only on the formalized requirements (i.e. do not depend on an additional system model). It generates at least one test case per output variable, but as most as many test cases such that every requirement is tested. Each generated test indicates the requirements that it is based on.</p>
 <p>It is ensured that the generated tests may not lead to false positives (i.e. the test case fails, although the system state is conform with the requirements).
 In case that there exist untestable requirements, the algorithm lists the set of untestable requirements.</p>
@@ -1090,15 +1090,15 @@ <h3 id="test-cases">Test Cases<a class="headerlink" href="#test-cases" title="Pe
 <h2 id="tool-support">Tool support<a class="headerlink" href="#tool-support" title="Permanent link"> #</a></h2>
 <p>Hanfor takes as input an exported .csv file from Doors and stores the requirements. Figure 7 shows a screenshot of requirements imported into a Hanfor session.
 There are two IDs, the Hanfor ID and the Doors ID, so that the two databases can be synchronized. The informal requirements are listed in the column 'Description'. Once a requirement is formalized in the specification language, it is listed in the column 'Formalization'. </p>
-<p>
-<figure><img src="../img/screenshot_hanfor_session.png" title="Figure 6" /><figcaption>Figure 6: Requirements exported into a Hanfor session.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/screenshot_hanfor_session.png" />
+  <figcaption>Figure 6: Requirements exported into a Hanfor session.</figcaption>
 </figure>
-</p>
 <p>Clicking on a requirement opens the modification page of the requirement (Figure 8). The requirement can be formalized in the specification language by using the drop-down lists for both scopes and patterns. The variables can be specified manually by using the autocomplete function of the signal database.</p>
-<p>
-<figure><img src="../img/screenshot_hanfor_req.png" title="Figure 7" /><figcaption>Figure 7: Modification window of a single requirement.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/screenshot_hanfor_req.png" />
+  <figcaption>Figure 7: Modification window of a single requirement.</figcaption>
 </figure>
-</p>
 <p>For more information about the usage of Hanfor, please have a look at the usage section.</p>
 
 

references/pea.html

@@ -864,21 +864,21 @@ <h2 id="representation-of-peas">Representation of PEAs<a class="headerlink" href
 <p>Figure 1 shows a phase event automaton representing the following requirement:</p>
 <div class="highlight"><pre><span></span><code>req1: Globally, it is always the case that if &quot;R&quot; holds for at least &quot;5&quot; time units, then &quot;Q&quot; holds afterwards.
 </code></pre></div>
-<p>
-<figure><img src="../img/example_pea.svg" title="Figure 1" /><figcaption>Figure 1: Phase event automaton modeling requirement <em>req1</em>.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/example_pea.svg" />
+  <figcaption>Figure 1: Phase event automaton modeling requirement *req1*.</figcaption>
 </figure>
-</p>
 <p>First we will have a look at the different components that are used to depict a PEA. </p>
 <p><strong>Variables:</strong><br>
 The variables and time constants that occur in the PEA are directly coming from the corresponding requirement. <em>req1</em> contains two boolean variables, namely "R" and "Q", and the timing constant "5". Each timing constant is related to a unique clock variable. The timing constant and its corresponding clock variable can be found in the PEA as a boolean time constraint, e.g. "c0&lt;5".
 The boolean variables can occur as unprimed variables (e.g. Q) and primed variables (e.g. Q'). Unprimed variables are related to the current point in time whereas primed variables are related to a point in time in the future.</p>
 <p><strong>Phases:</strong><br>
 The PEA consists of locations or phases, and edges representing transistions between the phases.
 Each phase of the PEA consists of a unique name, a phase invariant and a clock invariant. E.g. consider the PEA phase given in Figure 2. The name is "st01W", the phase invariant is given by the expression "R" and the clock invariant by the time constraint "c0&lt;=5". If a phase has an incoming edge that has no source, we call it "initial".</p>
-<p>
-<figure><img src="../img/pea_location.png" title="Figure 2" /><figcaption>Figure 2: Exemplary phase of a PEA defined by its name, phase invariant, and clock invariant.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/pea_location.png" />
+  <figcaption>Figure 2: Exemplary phase of a PEA defined by its name, phase invariant, and clock invariant.</figcaption>
 </figure>
-</p>
 <p><strong>Transitions:</strong><br>
 Each transition between phases is labeled with a boolean expression called "guard" and may additionally carry a clock reset statement. The guard may contain primed and unprimed variables as well as timing constraints. A transition from one phase to another can only be taken if the guarding expression is satisfied: This means that the guarding expression must evaluate to <em>true</em> under the current valuation (for unprimed variables and the clock constraint) together with the subsequent valuation (for the primed variables). If there is no constraint the guard is trivially satisfied and hence set to <em>true</em>.</p>
 <h2 id="run-of-a-pea">Run of a PEA<a class="headerlink" href="#run-of-a-pea" title="Permanent link"> #</a></h2>
@@ -953,10 +953,10 @@ <h2 id="run-of-a-pea">Run of a PEA<a class="headerlink" href="#run-of-a-pea" tit
 </div>
 <h2 id="timing-diagram">Timing Diagram<a class="headerlink" href="#timing-diagram" title="Permanent link"> #</a></h2>
 <p>As the tupel representation of a run is not necessarily intuitive, we often depict a run in form of a timing diagram. Below you find the timing diagram representation of the run described in Example 1. </p>
-<p>
-<figure><img src="../img/example_pea_run.png" title="Figure 3" /><figcaption>Figure 3: Timing diagram representation of a run included in the PEA of <em>req1</em>.</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/example_pea_run.png" />
+  <figcaption>Figure 3: Timing diagram representation of a run included in the PEA of *req1*.</figcaption>
 </figure>
-</p>
 
 
 

usage/workflow.html

@@ -962,10 +962,10 @@ <h2 id="start-hanfor">Start Hanfor<a class="headerlink" href="#start-hanfor" tit
 <div class="highlight"><pre><span></span><code>python3<span class="w"> </span>app.py<span class="w"> </span>-c<span class="w"> </span>example_input/example_input.csv<span class="w"> </span>--header<span class="o">=</span><span class="s1">&#39;{&quot;csv_id_header&quot;: &quot;ID&quot;, &quot;csv_desc_header&quot;: &quot;Description&quot;, &quot;csv_formal_header&quot;: &quot;Hanfor_Formalization&quot;, &quot;csv_type_header&quot; : &quot;Type&quot;}&#39;</span><span class="w"> </span>awesome_tag
 </code></pre></div></p>
 <p>you can now reach Hanfor by visiting <a href="http://127.0.0.1:5000">http://127.0.0.1:5000</a></p>
-<p>
-<figure><img src="../img/hanfor01.png" title="This is how Hanfor looks like after you started it" /><figcaption>Hanfor requirement overview</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/hanfor01.png" />
+  <figcaption>Figure 1: Hanfor requirement overview.</figcaption>
 </figure>
-</p>
 <h2 id="preprocessing">Preprocessing<a class="headerlink" href="#preprocessing" title="Permanent link"> #</a></h2>
 <p>By default, all rows now have the status <strong>Todo</strong>. 
 It might be the case that you want to change this for a certain set of rows to another status.</p>
@@ -982,10 +982,10 @@ <h2 id="formalization">Formalization<a class="headerlink" href="#formalization"
 <p>Order your requirement overview by <strong>Pos</strong>, by clicking on the table column.</p>
 <h3 id="req1">REQ1<a class="headerlink" href="#req1" title="Permanent link"> #</a></h3>
 <p>To formalize this requirement, we click on the ID <strong>REQ1</strong> to open then formalization-modal:</p>
-<p>
-<figure><img src="../img/hanfor02.png" title="This is how a formalization modal looks like" /><figcaption>Formalization modal</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/hanfor02.png" />
+  <figcaption>Figure 2: Formalization modal.</figcaption>
 </figure>
-</p>
 <ol>
 <li>Click on <strong>+</strong> to add a new formalization and then on <strong>..(click to open)</strong></li>
 <li>We now have to select a <em>Scope</em> and a <em>Pattern</em>.</li>
@@ -996,10 +996,10 @@ <h3 id="req1">REQ1<a class="headerlink" href="#req1" title="Permanent link"> #</
 If you save a requirement, Hanfor will automatically create the used variables and derive their type.
 You can examine and even alter them in the section <strong>Variables</strong>, for the case that Hanfor did not derive a variable-type correctly.</li>
 </ol>
-<p>
-<figure><img src="../img/hanfor_req1_formalization.png" title="This is how we formalize REQ1" /><figcaption>Definition of Scope and Pattern</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/hanfor_req1_formalization.png" />
+  <figcaption>Figure 3: Definition of Scope and Pattern.</figcaption>
 </figure>
-</p>
 <p>The same procedure can be applied to REQ2 - REQ6</p>
 <h3 id="req7-and-req8">REQ7 and REQ8<a class="headerlink" href="#req7-and-req8" title="Permanent link"> #</a></h3>
 <p>REQ7 and REQ8 are different.
@@ -1020,10 +1020,10 @@ <h3 id="req7-and-req8">REQ7 and REQ8<a class="headerlink" href="#req7-and-req8"
 formalized requirement. To fix that, to go the <strong>Variables</strong> section and open the <code>MAX_TIME</code> variable.
 You see that Hanfor derived the type <code>bool</code>, but we actually want it to be of type <code>CONST</code> as the variable represents time units. Change the type and
 also assign a value, for example <code>50</code>.</p>
-<p>
-<figure><img src="../img/hanfor_var_maxtime.png" title="This is how you should edit the MAX_TIME variable" /><figcaption>Example for the <code>MAX_TIME</code> variable</figcaption>
+<figure>
+  <img alt="" loading="lazy" src="../img/hanfor_var_maxtime.png" />
+  <figcaption>Figure 4: Example for the `MAX_TIME` variable.</figcaption>
 </figure>
-</p>
 <p>For REQ8 you should have: 
 <div class="highlight"><pre><span></span><code>Globally, it is always the case that if &quot;var3&quot; holds, then &quot;var4 == 1&quot; holds after at most &quot;MAX_TIME&quot; time units.
 </code></pre></div></p>