Sbuilder Roadmap v2 part 2/2

This post gives a short introduction to sbuilder -tool, and proposes changes (roadmap v2) in the tool for better support to reason on correctness of API ecosystem implementations.

It is the second of two blog entries updating roadmap v1 in sbuilder vision.

Introduction to sbuilder

sbuilder is a tool to generate runnable formal models in TLA+ language for business IT systems. At the time of writing this blog entry the released version of sbuilder is 0.3.4.

sbuilder combines three elements to create runnable TLA+ formal models:

  • API interfaces: to represent entry points providing access to services within the target system, API interfaces are loaded into sbuilder using API Loader Extension Point
  • TLA Snippets: to represent services and persistent state of the target system, and to defines correctness criteria verified in the formal model, TLA Snippets are loaded into sbuilder using Snippet Loader Extension Point
  • Setups: to represent environment of the target system, setup configurations complete the runnable formal model by defining sequence of interface actions, and domain ranges in data model

The formal model can be crafted manually, allowing the use of full expressive power in TLA language. If the target application is simple enough, formal model can be created automatically, as demonstrated for a Solidity language smart contracts on Ethereum platform.

The Objective of sbuilder (and This Blog Entry)

The objective of sbuilder -tool is to create a formal model for reasoning on safety properties of an application to

  • increase confidence in application correctness, and to
  • make QA more efficient, with faster feed back.

These objectives can be achieved because the model

  • can be executed without the need to have it installed on real production environment, and
  • the model checker tool can effectively check all possible executions in the model.

Obviously, creating a formal model is not a panacea, for example

  • sbuilder must use several heuristics to be able to create a usable runnable formal model,
  • the class of applications, for which the tool is applicable, is limited, and
  • errors in the formal model may be left undetected because formal model executions must be pruned to prevent state space explosion

This blog post discusses, how sbuilder could be used in modeling API ecosystems.

Heuristics Used in Creating Runnable Formal Models

In pursuing to create usable formal models sbuilder uses several heuristics. For example, it

  • partially automates formal-model construction. sbuilder core accepts interface definitions, which are translated into TLA+ language implementation. For some simple cases, sbuilder plugins can also translate implementation automatically to TLA+ snippets. To complete a formal model, manually crafted snippets may be added to the model.
  • abstracts data: Abstracting real world data is essential to enable runnable formal models. In sbuilder, each data element in the formal model defines a domain with actual domain values configured using setups.
  • controls state space generation. An inherent problem in model checking is state space explosion. Sbuilder allows defining setups as a sequence of interface operations, and parameter bindings, controlling formal model environmental context, and in effect, throttling state space generation.
  • allows non-deterministic choice in parameter bindings. Parameter bindings to an interface operation can be specified partially allowing model checker to use all possible combinations for the unspecified parameters, in effect allowing model checking to act as a “tester on steroids”.
  • allows controlling parameter binding. In cases, where the cardinality of an interface operation parameter set grows too large (e.g. infinite base domain, cartesian product of base domains), an error is raised, and parameter bindings must be fully specified. However, also in this case, a interface input may define several parameters bindings, again, allowing model checker to check all given possibilities.
  • detects infinite recursion in formal model. An invariant operator can be specified to guard against call stack growing too large in the formal model.
  • limits code size of a formal model. Sbuilder can prune out out code snippets, which are not reachable from the interface operations, or correctness criteria used to verify the formal model.
  • allows checking the possibility to reach a specified state. To increase confidence in correctness sbuilder allows defining possibility operators to demonstrate that a state, which is relevant to some correctness invariant, can, indeed, be reached in the formal model.

Sbuilder Roadmap v2

This chapater presents ideas for extending applicability of sbuilder for creating formal models to reason on correctness of API ecosystem implementations.

Topics covered are:

Support Simulation

Background:

Currently, sbuilder tool creates one formal model representing application in a single point of time. The application formal model can executed using multiple setups, each setup representing a different application environmental context (at the point of time).

API ecosystem, as IT-systems generally, go trough multiple development cycles, and sbuilder should be enhanced to have better support for these cycles.

Features to add:

To add better support for development cycles:

  • an application can be represented with a formal model in multiple points of time
  • a point of time representation of application formal model is composable (using named references), without the need to duplicate elements of the formal model
  • the point of time representation of a environment model (setup) is also composable

Abstract Complex Computation

Background:

Ethereum plugin demonstrates that, for some simple cases, it is possible to create a formal model automatically from an implementation. In general, this will not be possible. However, if an application is partitioned into

  • control flow and simple expressions: language constructs, which can be automatically translated into a formal model. This part includes control structures, simple arithmetic and boolean expressions, and calls to API interfaces in ‘computation’ section.
  • and computation: all other elements of the implementation, which do not fall under the category ‘control flow and simple expresions’. Computation defines API interfaces, called from ‘control flow’ -section.

we could envisage to create a formal model by composing together automatically translated and manually created model snippets, at least for some limited set of applications.

The composite formal model could still be used to check safety properties, if the formal model is more abstract than the implementation. Absence of an error in the formal model means that the error cannot be present in the implementation. However, in case of an safety property violation, both application error, and the possiblity of a false positive, must be considered.

A better understading, how computation modeling can be done, is needed, and should be demonstrated using a case study before committing too much effort in further developing this idea (ref. chapter Case Study).

Features to add:

To have better support for automatically and manually created model snippets

  • manually crafted TLA -components, and automatically translated components can be integrated in the formal model using the services in IAL/metamodel layer (ref chapter Support Heterogeneous API Ecosystems)
  • issue error messages for implementation elements, which cannot be automatically translated into a formal model
  • domain analysis should be able to process abstracted computation elements (see chapter Domain Model Analysis)
  • user documentation for the extension point exists

Support Heterogeneous API Ecosystems

Background:

Currently, sbuilder implements Ethereum -plugin to translate (a subset) of Solidity -language implementations TLA+ -language formal models. In the future, sbuilder should support heterogeneous API Ecosystem with multipe implementation languages such as golang for Hyperledger and and Java for Java EE.

A common metamodel should be extracted from sbuilder-ethereum to allow multiple multiple plugins to render formal model snippets into sbuilder context.

Features to add:

The picture blow gives an overview, how an Intermediate API Language (IAL)/Metamodel layer could help in supporting heterogeneous API ecosystems.

extract-metamodel.jpg

An Intermadiate Api Langauage (IAL)/Metamodel layer

  • abstracts the (low level) formal model in sbuilder, based on TLA-snippets, API interface, and setups (see chapter Introduction to sbuilder), more meaningful (higher level) for implementations
  • helps in documenting translation from implementation language to TLA+ language
  • supports primitives identified in current sbuilder-ethereum -plugin e.g. persistent state, account/contract identity, multilevel transactions, statements, etc., must be kept upward compatible, when new primitives are identified
  • allows translating several (heterogeneous) implementations together into one composite formal model, with implemetation integrrations represented with corresponding primitives in the IAL/metamodel layer1
  • has sbuilder-ethereum refractored to use the IAL/Metamodel layer

Domain Model Analysis

Background:

sbuilder abstracts data using domains defining possible data values for each data element in the formal model. Data abstraction operates in two phases: in the first phase, domain analysis identifies data element domains, and, in the seconds phase, sbuilder setups configure actual domain values.

Data element domains can be identified using domain mappers in sbuilder core. They can also be confiugred using Snippet loader extension point, as demonstrated in sbuilder-ethereum plugin, where units and globally available variables, and contract state variables, are translated to domains.

Domain model analysis should be implemented as common service in sbuilder supporting configurations with multiple plugins loading formal model.

Features to add:

In the future, domain analysis

  • is implemented as common service in sbuilder toolbox, sbuilder-ehtereum is re-fractored to use this common service
  • operates using representation managed by IAL/metamodel level (see chapter Support Heterogeneous API Ecosystems)
  • creates domain names automatically, but accepts also domain names given by user
  • merges domains together, if it finds domains to be equal
  • reports domain model errors, e.g. domain conflicts, missig domains, un-referenced domain definitions

Case Study

Background:

Before committing too much effort in implementation, a case study should be implemented with the objective of identifying possible missing features, and understanding potential usability and scalability problems:

  • identify missing features
  • usability problems
    • understand whether implementation, the tool set, or technology in general, is too complex for a normal user to manage
    • identify possibilities to hide technical details from a user, or the need to improve application consistency
  • scalability problems
    • understand wether the tool-set scales to match real word size system
    • find any bottlenecks in current implementation

Features to add:

The case study should demonstrate typical application development and maintenance errors, and how the toolset helps in identifying these errors:

  • adding a new scenario to an existing use case: Adding a new scenario to a use case opens up a new new execution path failing to implement all the required actions, which were present in the old execution paths.
  • a use case with differently interleaved scenarios: Different interleaving of a use case actions leads to an error.
  • a use case with a rollback: 1) Failing to cancel original transaction correctly . 2) Rollback transaction takes right actions, if run immediately after the original transaction, but fails, when the original transaction has been processed further.

The case study should help in identifying type of applications, which can be modeled using sbuilder -tool:

  • complex computation: A use case implementation, which cannot be translated automatically into a formal model. Computation needs to be manually abstracted, and merged with the automatically generated code snippets.

and, how sbuilder toolset scales with respect to adding more

  • use cases: implementation code, which can be pruned away
  • scenarios: running formal model using several setups
  • use case actions: having more code in the modeled use cases
  • more data: impact of increasing cardinalities in domain model

Error trace

Background:

TLA+ model checker -tool inputs the formal model created by sbuilder -tool, and checks the generated state space for any any property violation. If a violation is found, an error trace with formal model states, leading to the error, is outputted. The output is quite verbose, and hard for a user to comprehend – it should be parsed, and presented to user in more understandable format.

Features to add:

Error trace should be presented to user

  • plain text explanation of the violated property, with the option to show also TLA-formula
  • sequence of interface operations and their parameters bindings leading to the error

Fin

Risks implementing features, which have been correctly identified and analyzed, known knowns, are normally manageable. Probability of risks rise, if features are not thoroughly understood (due to sloppy thinking), known un-knowns, or, if inadequate processes allow surprises, un-known un-knowns. Working on incorrectly identified problems, un-known knowns, is the most catastrophic situation with risks (eventually) realizing in full extend.

In the context of this blog entry, there is more work to be done related to

  • un-known knowns: Applicability of creating a formal model to reason correctness on an API ecosystem implementation, must be questioned:
    • Generally, is there a need to change development practices in future API ecosystems – or does gradual improvement suffice?
    • Does introducing formal methods require too intrusive changes in current development practices?
    • Are formal methods too sophisticated technique to be deployed in common software development?
  • un-known un-knowns: A case study is needed to avoid surprises before implementing features presented in chapters
  • known un-knowns: To get better understanding, and to able to communicate the solution to gain acceptance, a more detailed specification (formalization?) is needed, especially for the ideas presented in chapters

Footnotes:

1

implementation: sbuilder prevents unique implementation names from colliding in the formal model, enabling IAL/Metamodel layer to keep formal model TLA snippets in isolation, and having integrations represented only by interaction primitives

Advertisements

2 thoughts on “Sbuilder Roadmap v2 part 2/2

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s