ReSA Web Editor

Download ReSA Editor Plugin
Download Consistency-checker Plugin
Evaluation Form
ReSA Editor Plugin Installation Consistency-checker Plugin Installation
  1. Go to Help->"Install New Software".
  2. On the "Work with" line, press "Add" button
  3. Select "Archive" and browse to the downloaded ZIP file.
  4. Install by following the installation wizard.
  1. Prerequisite: follow the ReSA Editor Plugin Installation
  2. Extract the Consistency-check ZIP file into a preferred location, e.g., C:/
  3. Install the plugin, except this time you select "Folder" instead of "Archive"
  4. Add location "[Extracted ZIP file directory]/z3amd64bit/" to the Path environment variable - configures the solver.

Documentation (Short Version)

Long version: ASL Documentation (Draft)

Natural language is the de facto requirements specification language in industry. It is intuitive and flexible, that is, it allows engineers choose different words, phrases, and syntax to specify requirements. However, it sometimes lead to ambiguous, incomprehensible, and vague specifications.

In contrast, template-based specification methods, for instance requirements boilerplate consist of templates (also known as requirements boilerplates), which are recurring patterns of requirements specifications in practice. Due to the rigid syntactic structures of these templates, using the template-base methods reduce ambiguity and improve readability of specifications, however, they are usually less flexible, and lack meta-model for extensibility.

The ReSA language combines the benefits of natural language and template-based specification methods. ReSA is constrained natural language, which uses similar syntax and semantics to English. Therefore, requirements specified in ReSA (ReSA specifications) are comprehensible, both by technical and non-technical people. Moreover, ReSA is tailored to specifying requirements specifications of embedded systems, that it, it implements concepts from embedded systems, by considering recurring specification scenarios in the design of the language.

The ReSA data types implement generic embedded system concepts, described in the table below.

Concept Description
System refers to any physical or logical entity that can process an input and return an output, e.g., the Adjustable Speed Limiter system, Cruise-control system
Parameter refers to the input and output parameters of a system, e.g., vehicle speed, vehicle speed set by the driver, torque force, etc.
Device the input and output devices of a system, e.g., sensors and actuators, human-machine interfaces, etc.
State refers to the operational and dynamic state of a system and its components, e.g., ASL activated, ASL deactivated, ASL enabled, etc.
Mode refers to the collection of operational capabilities and activities to achieve system objective, e.g., ASL mode, Cruise-control mode, etc.
Event refers to the internal or external occurrences that need to be handled by a system
Entity Can refer to any type of model element. It is the super concept of the rest of the concepts. It is used to instantiate elements whose types don’t match any other concepts.
Embedded system concepts

In ReSA, the primitive data types consist of types that implement the embedded concepts (also known as domain-specific types), and Numeric data types such as Int and Float. In addition, the language allows Literal,and Text types, introduced to improve flexibility and expressiveness of the language.

The domain-specific instances are declared inline as <Instance>:<Type>, e.g., "ASL":system, "vehicle speed":parameter, etc. However, Numeric instances are specified in place holders, for which their data types are implicitly stated through syntactic rules.

The coordinating conjunctives and, or connects two or more clauses to create compound clauses. The subordinating conjunctives such as if, when, while, after, etc., are used to connect main and subordinating clauses.

A clause is a grammatical unit, usually accepted by many to express more thought than a phrase but less than a sentence. There are several classes of clauses in English, but in ReSA, we consider only a specific class of clauses, known as the Adverbial clauses.
  1. Primitive clause, e.g.,
    "ASL":system shall be activated
  2. Complex clause, e.g.,
    ("ASL":system shall be activated if ASL is enabled)
  3. Main clause, e.g.,
    ASL shall be activated AND "ASL active":status shall be send to "the driver":user
  4. Subordinate clause, e.g.,
    if "vehicle":entity is "running":mode and "ASL":indevice is pressed
ReSA supports the following classes of specifications, classified merely based on syntax.
  1. Simple specification - starts with a single right-angle bracket, e.g.,
    > "ASL":system shall be activated within 500msec.
  2. Complex specification, starts with a double right-angle bracket, e.g.,
    >> if "ASLButton":indevice is pressed, ASL shall be activated within 500msec.
  3. Nested-complex specification, starts with a double right-angle bracket, e.g.,
    >> after ASL is enabled, [if "ASLButton":indevice is pressed, ASL shall be activated within 500msec.]
  4. Structured specification
    1. Conditional, e.g.,
      if ASLButton is pressed then
        ASL shall be activated within 500msec.
      endif
    2. Nested-conditional, e.g.,
      if vehicle is running or (vehicle is prerunning) then
        if ASLButton is pressed then
          ASL shall be activated within 500msec.
        endif
      endif
Currently, the requirements specified in ReSA (or ReSA specifications) have translations into Boolean logic. The translation consists of Boolean propositions and arithmetic expressions, and these Boolean expressions can be analyzed formally to detect specification defects. The consistency-checker plugin of the ReSA toolchain performs the translation, and then encodes the Boolean expressions in SMT-LIB format, which is analyzed by the Z3 SMT solver . The plugin, powered by the solver, checks if the ReSA specifications are consistent or not. If inconsistent, the plugin reports to the user with the set of specifications that contributed to inconsistency, also known as unsatisfiable core.