Welcome to the Architecture Verification Tool’s documentation!

Introduction

Welcome to the documentation page for the Architecture Verification Tool. The primary purpose of the verification tool is to allow a user to verify that a given FaaS architecture complies with a set of functional and non-functional requirements. These requirements are encoded using a new language, based on logic, called the constraint definition language (CDL).

In its primary mode, the tool takes as input a FaaS architecture and a CDL specification, and outputs a list of issues with the FaaS architecture (i.e. a list of violations of the CDL specification). The user can then use this information to correct their FaaS architecture. As correction of a FaaS architecture, and specification of requirements can be a hard task for non-expert users, the tool also provides two additional modes in order to help a user correct a non-compliant architecture, and to aid the user to specify requirements in the CDL.

Technical Overview

The Constraint Definition Language (CDL) provides a way of expressing the high level functional and non-functional requirements of a FaaS architecture. The final version of the associated Verification Tool (VT) will have three main modes of execution, detailed below.

  1. Verification. In this mode, the tool checks whether a given FaaS architecture (expressed as a TOSCA model) complies with the constraints expressed in a given CDL specification.
  2. Correction. In this mode, the tool searches for a modification of a (non-compliant) TOSCA model, in order to make it comply with the constraints in a given CDL specification.
  3. Learning. In this mode, the tool is given examples of valid and invalid TOSCA models, or execution traces, and a partial CDL specification. The tool then searches for an extension of the CDL specification which rules out all of the invalid examples, which maintaining consistency with the valid examples.



A demonstration of the verification and correction modes using a commandline version of the Verification Tool.


Getting Started with the Verification Tool plugin

The verification tool is available as a plugin for Eclipse Che. To request a license to use the plugin, please fill in this form.

Upon obtaining a license, the following lines should be added to the Devfile of your Eclipse Che workspace. Doing so will trigger the installation of the verification tool plugin.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
components:
  - type: chePlugin
    reference: >-
      https://raw.githubusercontent.com/radon-h2020/radon-plugin-registry/master/radon/radon-vt/latest/meta.yaml
  - mountSources: true
    endpoints:
      - name: radon-vt
        port: 5000
        attributes:
          protocol: http
          public: 'true'
          discoverable: 'false'
          secure: 'false'
    referenceContent: |
      ---
      apiVersion: apps/v1
      kind: Deployment
      metadata:
        name: vt-deployment
        labels:
          app: vt
          tier: frontend
      spec:
        replicas: 1
        selector:
          matchLabels:
            app: vt
            tier: frontend
        template:
          metadata:
            labels:
              app: vt
              tier: frontend
          spec:
            containers:
              - name: vt
                image: marklawimperial/verification-tool:latest
                imagePullPolicy: Always
                ports:
                  - containerPort: 5000
    type: kubernetes
    alias: radon-vt

To get started, you can clone the verification tool sample project. This contains a sample TOSCA model and a CDL specification.

_images/clone.gif

The file main.cdl contains the following CDL specification:

import "service_template.tosca";
import <function_conditions.cdl>;

$X.host_node := $X.requirements[$Y].host.node;

eu-west-1.hosted_in = ireland;
eu-west-2.hosted_in = uk;
cn-north-1.hosted_in = china;
us-east-1.hosted_in = us;

all_countries = { uk, us, canada, china, india, ireland };
supported_countries = { uk, us, canada, china, india };
uk.willing = { uk, us, canada, china, india, ireland};
us.willing = { us };
canada.willing = { uk, us, canada };
china.willing = { china };
india.willing = { india, uk };

thumbnail_buckets = { AwsS3Bucket_2, AwsS3Bucket_3 };

create_thumbnails.pre_conditions = {
  supported_countries.includes(input.country_of_origin)
};

create_thumbnails.post_conditions = {
  EXISTS($B : thumbnail_buckets, $B.storage.includes(input.thumbnail))
};

create_thumbnails.invariant_conditions = {
  FORALL($B : thumbnail_buckets,
    $B.storage.includes(input.thumbnail)
    =>
    input.country_of_origin.willing.includes($B.host_node.properties.region.hosted_in)
  )
};

functions = { create_thumbnails };

runtime_variable uploads_1.storage;
runtime_variable uploads_2.storage;

@depth 5;
@show uploads_1.storage;
@show uploads_2.storage;
@show input.country_of_origin;

In this scenario, the architecture consists of several buckets, located in various countries, and a lambda function “create thumbnails”, which stores an image in one of the buckets. The CDL specification expresses that the “create_thumbnails” function must meet certain requirements (given by its pre/post/invariant conditions). These are that, provided that the country of origin is supported, the image should be stored in at least one bucket, and that that bucked must be located in a country with whom the country of origin is willing to share. This implies that for each supported country, the architecture must contain at least one bucket located in a country with whom the original country is willing to share.

Right-clicking on the file “main.cdl” will allow the user to run the verification tool (by clicking the “Verify” option). The tool will then search for inconsistencies between the specification and the architecture, and will return any it finds.

_images/verify.gif

In this case, two inconsistencies are found, which correspond to the two supported countries for whom there is no bucket in which they would be willing to store their data (China and the USA).

Alternatively, it is also possible to start from a blank specification and try your own example. For more information on what it is possible to write in the CDL, please see this document. All files containing CDL specifications should have the extension “.cdl”.