Readme Releases

Sbuilder - A Specification Builder for TLA+ Tools - $Release:0.2.2$

A tool to generate runnable specification models in TLA+ language for target systems. Specification model can be verified using TLA+ Tools, and parts of it can be presented as implementation blueprints to developers.

See

• documentation for backgroun information, User's Guide and Developer's Guide

• live documentation (Cucumber tests) for more details on configuring Sbuilder, and on features implemented by Sbuilder

Target Systems

Sbuilder supports modeling typical business IT systems, where a system architecture identifies

• interfaces: entry point providing access to services within the system. Application interface is the public entry point, and infrastructure interface is the internal entry point allowing aggregation of (application) services from smaller units.

• services: unit of functionality accessible over interfaces. Infrastructure service is not directly accessible over application interface, as opposed to application services

• database: persistent data store, which services may access, and modify.

Runnable Specification Code

Sbuilder combines three main elements to create runnable TLA+ Specification Code:

1. Interface specification: Natively Sbuilder accepts RESTfull interface api specification expressed in Swagger v2.0 format. Plugin system allows importing API confiugration also from external systems, e.g. from salesforce

2. Specification extension: Sbuilder tangles manually crafted code snippets from Sbuilder code repository with the code generated using inteterface specifications. The manual code snippets use TLA+ language to model behavior and correctness criteria of the target system.

3. Setups: To complete runnable code Sbuilder uses setups. A setup is a sequence of interface operations, and their input parameters. In addition, a setup may define domain cardinalities, or domain values. The tools allows defining multiple setups, each setup resulting to a complete, runnable TLA+ code, allowing system model to be run in various environment context

Sbuilder uses following categories to organize specification snippets in its code repository:

• state: TLA+ variables modeling database

• operator: TLA+ language constructs, which enable "to define all the data structures and operations that occur in the specification"

• transaction: pseudo code implementation of common behavior in modifying system state

• service: pseudo code implementation of target system application services using PlusCal procedures in TLA+ language

• infrastructure: pseudo code implementation of target system infrastructure services using PlusCal procedures in TLA+ language

• interface: implementation of application interface extension points using PlusCal macros in TLA+ language

• correctness: operator definitions, and INVARIANT directives in TLA+ language specifying properties, which must be not violated in specification executions

• possibility: optional operator definitions to increase confidence in correctness invariants

• assumption: operator definitions, in TLA+ language specifying properties on specification model constants, which must be not violated.

Sbuilder can generate implementation blueprints as depicted in section modeling pipeline below. Implementation blueprints are html-pages including code snippets from Sbuilder code repository, or code generated based on interface specifications.

Modeling Pipeline

The picture below gives an overview, how Sbuilder -tool can be deployed in an "mainstream" software development process.

The objective for creating a specification model is to get better understanding, to get the design right, and to write better code for the system being built - and thereby to justify the extra effort needed in modeling.

We assume that services are currently implemented based on informal service specification documents written in English. We also assume that service interface is available in a machine readable format.

In the picture, process enhancements are highlighted in a box labeled "Pseudo code modeling". The output of the process enhancement are implementation blueprints, which are made available for developers at the side of current service implementation documentation. An implementation blueprint for a service contains pseudo code snippets extracted from specification model, relevant for implementing a particular service.

Pseudo code modeling includes following tasks:

• accept API specification input: Machine readable interface specification is translated to TLA+ language.

• create domain model: Interface parameters are mapped to domains. In this task, we define domain resolvers in Sbuilder -tool, and add TLA+ operators, and assumptions to verify that the resulting domain model conforms to service specification. In practice, creating a formal domain model results in "Gaining better understanding" of the informal specification.

• specify correctness: In the spirit of Test Driven Development, specifying correctness precedes specifying behavior. In this task, we interpret test cases, (hopefully) presented in the informal service specification, as TLA+ language operators and invariants.

• model behavior: Modeling behavior includes creating pseudo code service implementation in TLA+ language. In this task, when we have formal correctness criteria expressed in TLA+, running model checker points out traces leading to violations any of the criteria, and helps us in "Getting design right".

• create implementation blueprint: In the final task, modeler defines web pages for implementation blueprints. A blueprint collects relevant TLA+ snippets in Sbuilder code repository, together with any other useful documentation, to help in implementing a specific service. Web pages are made available for service implementation to help developers to "Write better code". Competent developers may understand TLA+ language, but, like in software engineering generally, good comments in pseudo code snippets will make blueprints more approachable.

The picture above defines following roles:

• architect: expert role specifying services, and defining interfaces

• modeler: expert role crafting specification extensions, and using Sbuilder, and TLA+ tools to generate specification code, and to verify its correctness

• developer: expert role implementing IT system interface and service according to the service specification, interface definition, and Sbuilder blueprint.

Usage

Pre-requisites

Sbuilder -tool requires Ruby 2.

To run the specification model created by Sbuilder -tool, you must have Java and TLA+ Tools installed.

Installation

To install Sbuilder Gem, create a Gemfile -file with the content

source "https://rubygems.org"
gem 'tla-sbuilder'

and run

bundle install

TLA+ Tools jar can be obtained from download page, see TLA+ Tools for more instructions on installation.

To Use Pet Store Example Application

Create default directories used by sbuilder in current working directory

bundle exec sbuilder.rb init

Create example configuration

bundle exec sbuilder.rb example pet

To list configuration files created for pet store example

ls cnf

To list specification extensions in TLA-sbuilder code repository

ls src/pet

To generate all setups in petstore example

bundle exec sbuilder.rb generate -t src/pet/

To run model checking for setup pet1 using TLA+tools jar in ~/java/tla/tla2tools.jar

export CP=~/java/tla/tla2tools.jar
(cd gen/pet1/tla; java -cp $CP pcal.trans model)
(cd gen/pet1/tla; java -cp  $CP tlc2.TLC setup)

and observe Model checking completed. No error has been found. to conclude that correctness invariants for the model are not violated.

In setup pet1, it is NOT possible to reach a state where predicate

at_least_two_tags == Cardinality( v_tags ) > 1

holds. This is because setup steps in cnf/extend_petstore_run1.yaml do not call interface operation /tags(post).

To show that it is NOT possible to reach a state, where at_least_two_tags holds, run

(cd gen/pet1/tla; java -cp  $CP tlc2.TLC possible_tag_with_invalid_address)

and observe Model checking completed. No error has been found..

However, steps for setup pet3, defined in cnf/extend_petstore_run3.yaml, do call /tags(post) twice, making it possible to reach a state where predicate at_least_two_tags holds.

The possibility to reach this state can be demonstrated running

(cd gen/pet3/tla; java -cp $CP pcal.trans model)
(cd gen/pet3/tla; java -cp  $CP tlc2.TLC possible_tag_with_invalid_address) 

and observing Error: Evaluating invariant possible_tag_with_invalid_address failed.

Create Own Model

See cucumber test for more details.

Create default directories used by sbuilder in current working directory

bundle exec sbuilder.rb init

Create extension templates for including specification extensions in default in TLA-sbuilder code repository into specification model.

bundle exec sbuilder.rb extend

Remove .example from all files in cnf directory

Generate example setups:

bundle exec sbuilder.rb generate

To run the model checking for setup default using TLA+tools jar in ~/java/tla/tla2tools.jar

export CP=~/java/tla/tla2tools.jar
(cd gen/default/tla; java -cp $CP pcal.trans model)
(cd gen/default/tla; java -cp  $CP tlc2.TLC setup)

Create TLA snippets in directory src, and include template snippets to generated code using mustache syntax.

For example, put the following code to

at_least_two_tags == Cardinality( v_tags ) > 1

file src/operator_at_least_two_tags.tla, and include it to specification code by adding following line into src/operator

{{>operator_at_least_two_tags.tla}}

Manage State Space Explosion, and Allow Scaling

State space explosion is inherent problem in model checking, the theory behind TLA+ tool.

Sbuilder tries to avoid problems due to state space explosion by controlling, how environment invokes interface operations, and in effect, by throttling number of states generated during model checking.

To avoid enumering to0 large sets Sbuilder allows

• fixing input parameter bindings in an interface operation. In cases, where domain sizes are not a problem, SBuilder allows TLA+ tool to use non-deterministic choice for input parameter values.

• using reduced domain ranges, when checking assumptions on resolved domains.

In TLA+tools, number of states/sec decreases as specification code volume increases (see a benchmark results for more details).

SBuilder tries to avoid problems due to increase in specification code by offering run time option --filter-src, which parses TLA+ snippets and runs static call flow analysis to prune off unused snippets from specification model. Parser is in alpha phase, in case of error, use option --filter-list to continue after parser error, and to configure manually modules call flow analyzer would otherwise omit from the specification code.

Extending Sbuilder

Sbuilder defines an extension point to add API loader plugins. An API loader is a Ruby class

• using Sbuilder::ApiLoader facade to integrate with Sbuilder

• satisfying api_loader_facade contract

• used as demonstated in cucumber tests

For a plugin implementation example, see an Swagger API loader in Sbuilder:

• implementation

• rpsec test

For example, to activate Sbuilder API loader plugin Sbuilder::Interfaces::Salesforce::SalesforceLoader implemented in tla-sbuilder-salesforce Gem using configuration hash shown below, add the following YAML snippet to sbuilder.yaml configuration file sub-section extend.loaders:

extend:
      loaders:
          - gem: tla-sbuilder-salesforce
            className: Sbuilder::Interfaces::Salesforce::SalesforceLoader
            configuration:
                  client_id: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxdaYTBJBssnuS0bvkraFcSSlC9EQZngf97yspdbh8iV_EV
                  client_secret: xxxxxxxxxx476009913
                  username: xxxxxxxev@gmail.com
                  password: 'xxxxxxxx'
                  security_token:  'xxxxxxxxxxVnEZjYP9cUZix9'

API instances are configured using entries referring plugin className in sbuilder.yaml interfaces array. For example, the entry for an Salesforce API instance entry.

 interfaces:
    -  className: Sbuilder::Interfaces::Salesforce::SalesforceLoader
       file: salesforce-api.yaml
       cache: sf

In the example, file -property points to a plugin configuration file, and cache property gives name prefix for files, which the plugin may use to cache API content to speed up generation phase.

License

MIT