Table of Contents
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
sbuilderusing 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
sbuilderusing 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
sbuildermust 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.
In pursuing to create usable formal models
sbuilder uses several heuristics. For example, it
- partially automates formal-model construction.
sbuildercore accepts interface definitions, which are translated into TLA+ language implementation. For some simple cases,
sbuilderplugins 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.
Sbuilderallows 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.
Sbuildercan 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
sbuilderallows 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:
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
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
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
Features to add:
The picture blow gives an overview, how an Intermediate API Language (IAL)/Metamodel layer could help in supporting heterogeneous API ecosystems.
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
sbuilder-ethereumrefractored to use the IAL/Metamodel layer
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-ehtereumis 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
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
- 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.
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
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
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
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