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

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

See

documentation for background information, User's Guide and Developer's Guide
on-line documentation (including Cucumber tests) for more details on configuring Sbuilder, and on features implemented by Sbuilder

Target Systems

Sbuilder supports modeling business IT systems, where 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+ formal model:

API interfaces: Natively Sbuilder accepts RESTfull interface api specification expressed in Swagger v2.0 format. API Loader Extension Point allows importing API confiugration also from external systems, e.g. from salesforce
TLA Snippets: Sbuilder tangles either manually crafted TLA snippets from Sbuilder code repository, or snippets loaded using Snippet Loader Extension Point, with code created for API interfaces. TLA -snippets are also used to specify correctness criteria for the system. Examples of TLA Snippets are:

  * **state**: TLA+ variables modeling *database*

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

  * **procedures**: implementation of target system application *services* as TLA
   [PlusCal](http://research.microsoft.com/en-us/um/people/lamport/tla/pluscal.html)
   procedures in TLA+ language

  * **macros**: TLA PlusCal implementation of common behavior, for
     example to modify system state

  * **invariant**: 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.

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

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.

Two Operating Modes

Sbuilder supports two operating modes:

Modeling Pipeline
Embedded Mode

Modeling Pipeline

Sbuilder can be embedded into "mainstream" software development process to support specification and design up-front, before actually starting the implementation.

In Modeling Pipeline mode, Sbuilder is used to create formal specification model of the application with the objectives 1) to get better understanding, 2) to get the design right, 3) and to write better code for the system being built. more details

See sbuilder-example for a toy example of using sbuilder in Modeling Pipeline mode.

Embedded Mode

Adding a separate task to create a formal specification model calls for commitment, which may be hard to achieve in contemporary software development practices. In order to hide the complexities in creating a formal model, Sbuilder can be embedded into a framework, and to use implementation code in creating formal model of the application.

An example of embedded sbuilder is in sbuilder-ethereum.

Usage

Pre-requisites

Sbuilder -tool requires Ruby 2.1

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

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

Installation

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

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

and run

bundle install

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 on-line documentation 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 into Sbuilder context using Snippet Loader plugin Sbuilder::SnippetLoaderSimple.

For example, put the following code into file src/operator_at_least_two_tags.tla

at_least_two_tags == Cardinality( v_tags ) > 1

and add configuration in snippets section in cnf/sbuilder.yaml, which gives the class name of the plugin to use (Sbuilder::SnippetLoaderSimple), defines metatype (framework-svc), application name (at_least_two_tags), and filename of the snippet in default src -directory (operator_at_least_two_tags.tla). The use of metatype allows single appName to mapped to several unique specNames by adding a metatype specific prefix to the appName. In this example, framework-svc metatype adds empty prefix to appName.

snippets:
  - className: Sbuilder::SnippetLoaderSimple 
    snippets:

      - metatype: framework-svc
        appName: at_least_two_tags
        file: operator_at_least_two_tags.tla

Run bundle exec sbuilder.rb generate, and observe that at_least_two_tags operator, indeed, is included into generated formal model e.g. in file gen/customer1/tla/model.tla:

(* SNIPPET: framework-svc/at_least_two_tags --> at_least_two_tags *)
at_least_two_tags == Cardinality( v_tags ) > 1
(* --END OF SNIPPET-- *)

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.

In order to avoid enumerating too 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.

Configuration

Main configuration file sbuilder.yaml

TBD

Setups modeling environment

TBD

Extending Sbuilder

API Loader Extension Point

Sbuilder defines an API Loader Extension Point to load API interfaces, and data type definitions into Sbuilder context. An API loader is a Ruby class

extending Sbuilder::ApiLoaderPlugin
using Sbuilder::ApiLoader facade to integrate with Sbuilder
satisfying api_loader_facade contract
interacting with Sbuilder as demonstrated in cucumber tests

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

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 into sbuilder.yaml configuration file extend.loaders -section:

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.

Snippet Loader Extension Point

Sbuilder defines an Snippet Loader Extension Point to load TLA snippets into Sbuilder context. An Snippet loader is a Ruby class

extending Sbuilder::SnippetLoaderPlugin
using Sbuilder::SnippetLoaderFacade facade to integrate with Sbuilder
satisfying interface specification snippet_loader_plugin: signature
interacting with Sbuilder as demonstrated in cucumber tests

For a plugin implementation, see an SnippetLoaderSimple example

Snippet loader plugins are activated in the same way as API loader plugins using a configuration in extend.loaders -section in cnf/sbuilder.yaml

An example of using Snippet Loader Plugin was presented earlier in this README.

License

MIT