logoReal User's Guide

  1. Getting Started
    1. Getting REAL Up and Running
    2. Creating an Enumeration
    3. Adding Objects to the Enumeration
    4. Removing Items from the Enumeration
    5. Editing Properties
  2. Enumeration Objects
    1. Enumeration
    2. Requirements
    3. System Interfaces
    4. Stimuli
    5. Responses
      1. Outputs
      2. Named Responses
    6. Named Responses
    7. Predicates
      1. Stacked Predicates
      2. Deleting Predicates
    8. Mappings
      1. Extended Mappings
      2. Actions
      3. Setting Predicates
    9. States
    10. State Variables
  3. Enumeration File Types
    1. HTML Output
  4. Enumeration Validation

Getting Started

Getting REAL Up and Running

The current distributions of REAL can be downloaded from http://sourceforge.net/projects/realsbs/files/?source=directory. Download the zip file for your architecture and OS. REAL does not need to install anything. Just unzip the download and open the REAL directory. To run REAL execute the REAL application (Real or Real.exe), using a method appropriate for your OS.

A JRE, based on Java 1.6 or later, must be installed in your OS to run the application. To download a compatible Java distribution version, you need go here: http://www.oracle.com/technetwork/java/javase/downloads/index.html.

Possible Exceptions When Running REAL

REAL uses a built in web browser that may require prior setup on some systems. If you have problems viewing the HTML tab in REAL, go here for more information: http://www.eclipse.org/swt/faq.php#browserplatforms. A possible solution for 32-bit Linux JDK systems is to set the MOZILLA_FIVE_HOME path to the xulrunner directory containing the needed libraries. Don't forget to set the LD_LIBRARY_PATH to include MOZILLA_FIVE_HOME.

Creating an Enumeration

Open the "File"->"New"->"Real Model" menu item.

This will bring up the wizard for creating a new Real Model. Enter or choose a file path with the extension .real or .pse (see Enumeration File Types) for the new model.

REAL currently allows modeling of Enumeration objects only. Once the model is created, click the Enumeration object at the top of the Outline View to select it.

Notice the Properties view the bottom of the screen now has two properties: "Title" and "Description". Whenever an object in the enumeration is selected, its readable and editable properties will be shown in this view. To edit Properties, click on the cell under the "Value" column next to the name of the property to be edited. If the property can be edited, a cell editor will appear (see Editing Properties).

Besides the Enumeration, most modeled objects can be edited directly in their respective tables. However, the Enumeration can always be selected from the Outline Page.

Adding Objects to the Enumeration

The following objects can be added directly to the enumeration at any time by the user: Requirements, SystemInterfaces, Stimuli, Outputs, Named Responses,Predicates, and State Variables. There are three ways to add objects: Tables, the Menu, and the Outline Page. To add an object using a table, click a tab corresponding to one of the objects previously listed. For example, to add a Requirement, click the "Requirements" tab. Right-clicking on an an empty row of a table will bring up a selection-based pop-up menu. To add a new object of the table's underlying type, select "New Child"->Object_to_Add (e.g., "New Child"->"Requirement").

If there are objects already present, right-clicking any of them will bring up a similar menu, where "New Child" is replaced by "New Sibling." In this case "New Child" and "New Sibling" perform the same action (i.e. adding a new object to the table).

Adding new objects using the Menu is similar to adding them using the table. Click the "Real Editor" menu item, and depending on what is currently selected, there will be one of two familiar options. If no item is selected (either in a table or in the Outline Page), then the "New Child" option will be present. Otherwise, the "New Sibling" option appears. Again, these actions perform the same function.

To add objects using the Outline Page simply right click on any of the parent items. Right-clicking on the Enumeration item will bring up the "New Child" option. This option allows for the addition of any of the addable items (see above). Right-clicking on a specific parent item (i.e. Requirements, Stimuli, etc.) will bring up the "New Sibling" or "New Child" options. The "New Child" will allow the addition of objects corresponding to the parent being clicked. The "New Sibling" will allow the addition of any addable object type.

Note that adding different items has different effects on the underlying enumeration. For more details on the effects of adding a specific object see that object's section in the guide.

Removing Objects from the Enumeration

Removing items is very similar to adding items. Any item that can be added can be removed. One difference to note is that the menu for removing items is the "Edit" menu. To remove objects using the "Edit" menu, select a removable object and click "Edit"->"Delete".

Alternatively, right-click to remove an object (either in a table or the Outline Page), and select the "Delete" action.

Just as when adding objects, there are different effects on the enumeration when removing different objects.

Editing Properties

Properties are the attributes and references of particular objects. For example, a Stimulus has the following properties: "Short Name", "Long Name", "Description", "Sources", and "Requirements". "Short Name", "Long Name", and "Description" are string type attributes, while "Sources" and "Requirements" are multi-valued references to other objects (in particular System Interfaces and Requirements).

Properties of objects can be edited in two ways: Tables or the Properties view. To edit properties using a table, simply click on the cell of the object's property in its corresponding table. (Column names identify properties in tables.)

A cell editor appropriate for the property will appear. Editing attributes is generally done using an in-place text editor, while editing references requires a pop-up menu or dialog.

Not all properties can be edited, and properties that cannot be edited will not display a cell editor.

Editing properties using the Properties view is similar to using a table. Selecting an object will bring up the object's property list in the Properties view. Properties are listed in alphabetical order and use the same cell editors as the table. To edit a property, click the cell next to the property's name and use the cell editor.

Enumeration Objects

Enumeration

The enumeration object is the parent of all other objects. There is only one enumeration object per REAL model. An enumeration has two attributes: Title and Description.

Requirements

REAL Requirements are the functional requirements of the system being specified. REAL requirements are text based, but can be linked to other resources via a URL. A requirement has two attributes: Tag and Text. The tag is the unique name of the requirement used to reference it throughout the rest of the enumeration. The text is a complete description of the requirement and is where a URL can be entered and converted in the HTML.

Changing the tag of a requirement will change the name of all references to that requirement. The tag must be made up of non-whitespace characters.

System Interfaces

The system Interfaces define the system boundary. A system interface has two attributes: Name and Description. The Name attribute is used to identify the interface throughout the enumeration. The Description attribute is a complete description of the interface, and is where the URL can be entered and converted in the HTML.

A system interface also has one reference: Requirements. The requirements trace the interface back to the functional requirements.

Changing the name if the system interface will change the name of all references to that interface. The name must be made up of non-whitespace characters.

Stimuli

The Stimuli are events that result in information flow from outside to inside the system boundary. A stimulus has three attributes: Short Name, Long Name, and Description. The short name attribute is used to identify the stimulus throughout the enumeration. The long name attribute is a succinct, but descriptive, name for the stimulus. A Long Name should be considered the proper name, and the Short Name should be as short as possible to make mappings and states easier to read. The Description attribute is a complete description of the stimulus and is where a URL can be entered and converted in the HTML.

A stimulus also has two references: Sources and requirements. The sources are the system Interface(s) where the stimulus event can occur. The Requirements trace the stimulus back to the functional requirements.

Changing the Short Name of a stimulus will change the name of all references to that stimulus. Because the mappings must ordered length-lexicographically, changing a stimulus short name can result in a reordering of the enumeration.

After changing stimulus a to d ...

The Short Name must be made up of non-whitespace characters. Also, a Stimulus must have at least one source Interface.

Adding a Stimulus will subsequently create a new Mapping for each canonical sequence (State) in the enumeration. If there are no canonical sequences other than the empty sequence (e.g. the enumeration is empty), then the initial lambda state will be added along with the a Mapping for the added Stimulus.

Deleting a stimulus will remove any Mappings whose Action references that stimulus. If any of the removed mappings are extended, then some remapping is done to preserve Mappings and States that refer to the removed mappings.

After stimulus a is deleted ...

Responses

Responses are externally observable system events, often involving information transfer from inside to outside the system boundary. A response has two attributes: Name and Description. The Name attribute identifies the response throughout the enumeration. The Description attribute is a complete description of the output and is where a URL can be entered and converted in the HTML.

A response also has one reference: requirements. The requirements trace the output back to the functional requirements.

Changing the name of a response will change the name of all references to that output. The name must be made up of non-whitespace characters.

There are two types of responses: Outputs and named responses.

Outputs

The Outputs are responses that can be independently produced by the specified system. An output has one additional attribute: Long Name. The Long Name attribute is a succinct, but descriptive, name for the output.

An output also has one reference: Destinations. The destinations are the system interfaces where the output can be observed. An output must have at least one destination.

Named Responses

Named Responses are groups of outputs that can be produced simultaneously (where the definition of simultaneous is system-specific).

A Named Response also has one reference: Outputs - the list of Outputs that make up the Named Response.

Predicates

Predicates are are conditional statements that can be evaluated as true or false. One or more Predicates can be applied to a single stimulus to produce two or more Actions. These Actions can be viewed as "just-in-time" stimuli. On or more predicate is applied to a sequence's new stimulus to partition it into a set of events predicated on particular system conditions. A predicate has two attributes: Name and Condition. The Name attribute is used to identify the predicate throughout the enumeration. The Condition attribute is a statement that is either true or false. The Condition is also where a URL can be entered and converted in the HTML.

A predicate also has one reference: Requirements. The requirements trace the predicate back to the functional requirements.

Changing the name of a predicate will change the name of all references to that predicate. The name must be made up of non-whitespace characters.

Stacked Predicates

Stacked predicates refer to multiple predicates applied to a stimulus. A predicate can be applied to a predicated stimulus as long a that predicate is different from those already applied. Predicates applied to stimuli imply a binary tree structure with the each parent node represented by a predicate, each branch represented by a true/false value of the predicate's condition, and each leaf node represented by a sequence.

Deleting Predicates

Deleting a predicate that has been previously applied to a stimulus will result in a dialog being displayed to the user.

A list of mapping groups is displayed. Each group represents the leaves of the implied predicate tree. (Each leaf correspondes to one mapping.) The user is prompted to select one mapping (or none) for each group. After the user presses "OK", each mapping that that was not selected will be removed. If a mapping was selected it will retain the equivalence, trace, and response information but have its the deleted predicates removed. If no mapping was selected then, a new illegal mapping will be added with the deleted predicate removed.

If any of the removed mappings are extended, then some remapping is done to preserve mappings and states that are dependent on the removed mappings.

After predicate p2 is deleted ...

Mappings

Mappings are associated with sequences of stimuli, possibly modified by predicates. Each individual stimulus or stimulus/predicate combination is referred to as an Action. Each sequence is mapped to its equivalence and response information. A mapping has three attributes: Name, Length, and Legality. The Name and Length attributes are derived from the individual actions that make up the sequence and are not directly editable by the user. The Legality attribute is a boolean value. Legal mappings are those sequences that are possible within the specified system or its environment. Illegal mappings are impossible sequences.

A mapping also has six references: Prefix, Action, Responses, Response Trace, Equivalence, and Equivalence Trace. The Prefix is a sequence associated with a previous mapping. The Action is the new stimulus/predicate combination, appended to the Prefix to complete the sequence associated with the mapping. The Responses are output events produced by the Action, given the system status resulting from previous actions in the prefix. The Response Trace is used to identify the functional requirements that dictate the specified Response(s). The Equivalence indicates that the responses to any future actions is the same, regardless of whether we start from this mapping's sequence or that of the equivalent sequence. The equivalent sequence can only be one that is length-lexicographically less than the sequence for the current mapping. If there is no Equivalence for a legal mapping then the mapping is extended. Finally, the Equivalence Trace is used to trace the equivalence decision for the mapping back to the requirements.

Extended Mappings

Extended mappings are mappings whose sequences are legal and have no equivalence to a previous sequence. To extend a legal mapping set its equivalence to the empty value.

To extend an illegal mapping, either set its Legal attribute to true or set its Response to a non-empty value. Likewise, changing the legal attribute of an extended mapping from the legal to illegal will result in the mapping no longer being extended.

If a mapping is changed from the extended to not extended, then some remapping is done to preserve later mappings and states that are dependent on the removed mapping.

After removing the equivalence of mapping a to <lambda>, a is extended...

If a mapping is extended, then a new State is created and added to the Enumeration. This operation also updates the Canonical Sequence Analysis.

Actions

An Action is a combination of a Stimulus and one or more predicates. An action essentially partitions a stimulus, based on the predicate list. Each predicate represents a parent node in binary tree structure. Each branch of the node is represented by the true/false value of the predicate. An action with no predicates in its list implies there is no partitioning of the stimulus. Although each mapping has only one action, an action with predicates infers a connection to other mappings and therefore other actions. This is the result of the tree structure of the predicate partitioning. In the tree, each leaf node is associated with a mapping and therefore a particular action.

Setting Predicates

Predicates are explicitly added to or removed from a mapping action using a menu command and dialog: Editing REAL Predicates. .

States

The canonical sequences are the sequences from Mappings that are legal and extended. Note that the lambda sequence is not displayed on the Mappings tab but is also a canonical sequence, mapped to the initial state (also called lambda). The canonical sequences of the enumeration correspond to States of a finite state machine, specifically a Mealy machine. A state has one attribute: Name. The name is derived from the canonical sequence representation of the state, and cannot be set by the user.

A state also has one reference: State Var Values. State Var Values is short for state variable values and is a list representation of State Variables and assigned values for a particular state.

State Variables

State variables are used to partition the state space of the enumeration parametrically. A state variable has three attributes: Name, Values, and Description. The Name attribute identifies the state variable throughout the enumeration. The Values attributes is a list of strings that are the possible values that can be assigned to this state variable. The Description attribute is a complete description of the state variable and is where a URL can be entered and converted in the HTML.

Making any changes to the state variables of the enumeration will result in the updating of the Canonical Sequence Analysis.

Changing the name of a state variable will change the name of all references to that state variable. Removing values from the Value list of a state variable will result in the change any current assignments of that value to be unset.

Adding a state variable adds a new unset assignment to every State and updates the Canonical Sequence Analysis.

Assigning State Variables

Initially, State Variables have no value assigned to them. To edit the assignment, open the editor of the State Var Values reference for the state.

Next select a variable from the list on the left. There are two ways to set a value: double-click or select. To set a value using double-click simply double click the value. To set a value using a selection, select the value and press the "Set Selection" button. Notice there is an extra value called "[ANY]". This is a catch-all value that is used to indicate that the variable can have any value for this particular state. For more information see the section on the Canonical Sequence Analysis.

Changing the variable assignments for a state causes the canonical sequence analysis to be updated.

Canonical Sequence Analysis

The canonical sequence analysis is used to determine if the state variable assignments cover the entire state space (complete) and do not overlap (disjoint). The canonical sequence analysis can be checked at any time by clicking the tool bar icon at the top left of the interface labeled "CSA".

The analysis tells whether there are any unset variables, uncovered states, or overlapping states. If there are no overlapping states, then the "Disjoint" label appears. If there no uncovered states, then the "Complete" label appears on the icon.

State Box

The State Box specification describes a finite state machine derived by combining the Enumeration and the Canonical Sequence Analysis. The State Box specification is expressed as a set of tables - one for each stimulus. Each table gives the initial state, any required predicates, final state, and response for all possible transitions caused by the specified stimulus. The state box can be viewed in the HTML tab once the canonical sequence analysis is complete and disjoint.

Enumeration File Types

There are two types of enumeration files that REAL can open: real and pse. Real files are the default XMI serialization format of REAL, and use the .real extension. Pse files are created by the prototype enumeration tool, Proto_Seq, and use the .pse extension. To be backwards compatible with Proto_Seq, an enumeration with stacked Predicates cannot be saved as a pse file. Otherwise, use the "File"->"Save As" menu action to convert between file types.

HTML Output

REAL creates an HTML version of the current enumeration in the HTML tab.

The HTML tab is updated automatically whenever the enumeration is updated. Aside from displaying all the current enumeration information, the HTML tab also displays the state box specification.

The tab can also server as a web browser, allowing URLs in the object descriptions to be converted to hyperlinks. For example: [url=https://sqrl.eecs.utk.edu]sqrl[/url]. The "Back", "Forward", "Stop", "Refresh" buttons all work as standard browser functions. The "Goto Enumeration" button will return the user to the enumeration HTML. Likewise, switching tabs or updating the enumeration in any way will refresh the HTML tab to the enumeration HTML.

To export the HTML of the enumeration to a file, select "File"->"Export HTML".

Follow the directions of the wizard and choose a location to export the HTML.

Enumeration Validation

Validation of the enumeration provides a mechanism to ensure the Enumeration object and its children conform to a set of constraints and invariants. Validation can be performed on an object using menu items. To validate an object using the Menu, select the object and click "Real Editor"->"Validate". Similarly, right-clicking an object will bring up a pop-menu with the "Validate" action.

For the most part, there is no need to validate an object regularly because the interface ensures that most constraints and invariants hold. Because validation can take some time to finish (depending on the enumeration size), it is recommended that the user only validate if they suspects something is wrong with their model.

Hint: To validate every object in the enumeration, validate the enumeration object in the Outline Page.