<h3><fontcolor="#336699">Creating a Glossary</font></h3>
To model the problem domain, a glossary can be created. The glossary is automatically linked to the requirements specifications. Using the glossary it is easily visible whether the agreed vocabulary is used in all descriptions.
A glossary is used to capture the vocabulary of the problem domain. Once created, the glossary is automatically linked to the requirements specifications. Using the glossary it is easily visible whether the agreed vocabulary is used in all descriptions.
<br><br>
To create a new glossary, select <i>Glossary</i> in the context menu of a requirements analysis.
Within a formal specification different kind of models like component architectures, state machines, etc. can be used.
For more information see <i>Modeling and simulation</i>. Formal specifications can be the tested automatically with test suites and can be refined to the architecture level, for both see <ahref="model_testing.html">Test Model</a>.
For more information see <i>Modeling and simulation</i>. Formal specifications can be used as input for the generation of test cases
<ahref="model_testing.html">Model-based Testing</a>. The conformance of the architecture implementation with the formalized requirements
can be tested as described in <ahref="refinement_testing.html">Refinement Testing</a>.
@@ -169,7 +171,7 @@ The button <i>Export in ReqIF standard</i> opens a dialog, where all textual req
<h3><fontcolor="#336699">Verification</font></h3>
MIRA contains automated verification and there is the possibility to save the results of manual checks.
MIRA offers support for automatic verification of requirements. Furthermore, it also offers the possibility to save the results of manual checks.
<br><br>
...
...
@@ -191,11 +193,11 @@ The list is extracted from a XML-Template, which can be modified. At the moment,
<h3><fontcolor="#336699">Connection of use case and component architecture</font></h3>
In the section <i>Detail</i> of a use case a simple connection between use case and component architecture can be done:
In the section <i>Detail</i> of a use case, a simple connection between use case and component architecture can be done:
<ul>
<li>connecting the scope of the use case with component of the component architecture</li>
<li>connecting the trigger of the use case with input of the component architecture</li>
<li>connecting the pre-condition, min. guarantee, success guarantee of the use case with status of the state automaton of the component architecture</li>
<li>setting the scope of the use case to be a component of the component architecture</li>
<li>connecting the trigger of the use case with an input port of the component architecture</li>
<li>connecting the pre-condition, min. guarantee, success guarantee of the use case with states of a state automaton of the component architecture</li>
</ul>
When the scope of a use case is connected with a component, then the reference to this use case is also listed below the component. So you can easily see which use cases belong to one component.
<i>MSC Entities</i> represent different instances which will interact with each other. They can be connected by holding the <i>Ctrl-Button</i> on your keyboard while clicking on one <i>MSC Entity</i> and dragging with the mouse to another <i>MSC Entity</i>.
The result of this action is a <i>Message</i> between the two entities that has an <i>Exit</i> and an <i>Entry</i>. All of these objects can be renamed in the <i>Properties</i> section.
<i>MSC Entities</i> represent different instances which interact with each other. They can be connected by holding the <i>Ctrl-Button</i> on your keyboard while clicking on one <i>MSC Entity</i> and dragging with the mouse to another <i>MSC Entity</i>.
The result of this action is a <i>Message</i> between the two entities that has an <i>Exit</i> and an <i>Entry</i>. All these objects (entities, messages, ...) can be renamed in the <i>Properties</i> section.
<br><br>
<imgsrc="./pictures/MSC.conect_MSC_Entities.png">
...
...
@@ -59,9 +59,9 @@ The result of this action is a <i>Message</i> between the two entities that has
A <i>Loop</i> defines a certain repetition of <i>Messages</i>. Conditions for start and end of the loop can be set in the properties section.
<br><br>
A <i>Condition</i>defines a predicate. For <i>Conditions</i> a condition expression can be set in the properties section.
A <i>Condition</i>is a predicate that the system must satisfy at a certain time moment. For <i>Conditions</i> a condition expression can be set in the properties section.
<br><br>
Both can be added to your message sequence chart by pulling it into the <i>MSC Specification</i>, resizing it and bringing it in the appropriate position.
Both conditions and loops can be added to your message sequence chart by pulling them into the <i>MSC Specification</i>, resizing them and bringing them in the appropriate position.
<i>Loops</i> and <i>Conditions</i> can be associated with more than one <i>MSC Entity</i>.
<br><br>
The following picture shows an example for a <i>MSC Specification</i> including every object mentioned in the above sections:
@@ -116,6 +116,10 @@ The ports, which are highlighted in blue rectangles, should associate with the p
<br>Figure 6: Example of a mode component structure.
<br><br>
<!--
MODE DIAGRAMS DO NOT HAVE DATA YET
<h4><font color="#336699">Data State Variables</font></h4>
Data State Variables (DSVs) are internal variables that can be accessed in all modes of the corresponding mode automaton.
...
...
@@ -127,6 +131,8 @@ To edit such a variable to a mode automaton, click the <i>Mode Data</i> tab in y
<br><br>
The way to edit the variable is described in <a href="state_automaton.html"><i>State Automaton</i></a>. Please check there for more information about Data State Variable.
With a refinement specification it can be tested whether a concrete (implemented) component shows the same behavior as an abstract component or a functional specification.
Steps to create a refinement test suite:
<ul>
<li><b>Step 1</b> - Right click on the concrete component in the model navigator and select "Refinement Specification"
After choosing the abstract component the representation and interpretation functions for the refinement specification are automatically generated. Their purpose is to specify the mapping of the input and output ports from the abstract to the
concrete component and the other way round (see picture below). If necessary they can transform the values.
After choosing the abstract component the representation and interpretation functions for the refinement specification are automatically generated. Their purpose is to specify the mapping of the input and output ports from the abstract to the
concrete component and the other way round (see picture below). If necessary they can transform the values.
@@ -16,17 +16,17 @@ Contracts-based Specification for Components.
</head>
<body>
<h2><u><fontcolor="#336699">Creating a Patterns based Specification for a Component</font></u></h2>
<h2><u><fontcolor="#336699">Creating Contracts based Specifications for Components</font></u></h2>
Components are used both as secification of requirements as well as for modeling the architecture.
Components are used both as specification of requirements as well as for modeling the architecture.
Whenever we use components, we can specify their black-box behavior with the help of contracts.
In AF3 we distinguish among four kinds of contracts:
<ul>
<li><b>Assumptions</b> represent invariants over the input ports of a component. Simply said, assumptions are what a certain component
expects as valid input from the environment (e.g. a certain input port has values between some range or that
expects as valid input from the environment (e.g. a certain input port has values within a certain range;
some input port has a value that is always bigger than the value of another port).</li>
<li><b>Guarantees</b> represent invariants over the output ports of a component. Guarantees are conditions that a certain component
promises to the environment. </li>
promises to its environment. </li>
<li><b>Basic Contracts</b> represent logical expressions of the form "if inputs satisfy assumption A then component outputs will satisfy the guarantee G
(after a certain number of steps)"</li>
<li><b>Advanced Contracts</b> represent complex conditions about the relation between the inputs of a component and the outputs
...
...
@@ -34,7 +34,7 @@ promises to the environment. </li>
</ul>
A temporal logics specification is made of one or more contracts (assumptions, guarantees, basic/advanced contracts).
The main place where the assumptions, guarantees and basic contracts are defined during the specification phase is the "Contracts View".
The main place where the assumptions, guarantees and basic contracts are defined during the specification phase is the "Contracts Specification" view.
