Sbuilder Roadmap

Introduction

This post argues that instead of deploying Sbuilder to support an upfront design step, it should be embedded into a framework. The post entry describes enhancements required in the current 0.2.3 version, and identifies a need for a proof of concept to better understand the feasibility of the proposal.

This post is a visio document in in Sbuilder documentation.

Getting Started

Document Context

This post assumes that the reader is familiar with Sbuilder -tool. A good starting point is Sbuilder documentation presenting background information, Uses’s Guides, and Developer’s Guides. The post links extensively to Sbuilder live documentation, and understating of Gherkin -language used in the Cucumber tests is assumed.

Accessing the Code

Clone GIT repository for tla-sbuilder for the implementation of Sbuilder -tool

git clone https://github.com/jarjuk/tla-sbuilder

and check out version 0.2.3 used in this post:

(cd tla-sbuilder; git checkout tags/0.2.3 )

Clone GIT repository for sbuilder example

git clone https://github.com/jarjuk/sbuilder-example

and check out version 0.0.8 used in this post:

(cd sbuilder-example; git checkout tags/0.0.8)

Current Status

Sbuilder Implementation

At the time of writing this blog entry, the latest version of Sbuilder -tool is 0.2.3. Documentation includes User’s and Developer’s Guides, and live documentation in the form of Cucumber tests.

Sbuilder creates runnable specification model in TLA+ language by composing together interface model, domain model, and specification snippets from Sbuilder code repository. 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.

Natively Sbuilder supports loading interface models in Swagger version 2.0 format. Version 0.2.3 defines an extension point for loading API meta data. A plugin, using this extension point, to load Salesforce API metadata, has been implemented.

Sbuilder GEM is bundled with an example application {1}, {2}, {3}. Another example application is in a GIT repository.

Need for Embedded Sbuilder

Modeling Pipeline

Sbuilder README -document version 0.2.3 presents “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.

process.jpg

(Click the image for a larger version)

Creating a runnable specification model for an implementation has been reported to bring benefits. However, trying to introduce a separate modeling step to contemporary software development practices is not easy, to say the least:

  • Business owners have their focus in the business, and today, quite often, in the profit of the next quarter. Ideas, which generate positive cash flow in a long run, are not likely to make it to the short list to push forward in the near future.
  • Staff managers see the large costs involved in building, and maintainining, the capability needed by the design step.
  • Project managers may be afraid of extra work, and see risks in finishing projects within budget, if amount of design work is increased
  • An average software developer may be aware of formal methods, but tend to see them more for academic use, and not suitable for real world applications.

Embedded Sbuilder

The impediments, such as the ones presented in the previous chapter, could removed, or at least reduced, if a specification model for an application could be generated automatically.

The picture below presents the idea of embedding Sbuilder into a framework enabling specification model to be generated automatically: Sbuilder defines extension points for loading API interfaces, service semantics, correctness properties, and setups. Framework developer uses these extension points to write plugins, and to embed Sbuilder to a framework. Compontent developer defines interfaces, creates implementation, and model, for components running on the framework. Application developer composes an application using the components, and some glue code. Specification model is created automatically using interface definitions, component models, the glue code. The resulting application model is automatically checked to conform the expected behavior.

embedded-architecture.jpg

(Click the image for a larger version)

The next chapter discusses in more details about the status of Sbuidler -tool, and the enhancements needed to enable embedded Sbuilder.

Enhancements to Sbuilder

Enhance API Loader

Sbuilder version 0.2.3 implements [{1}, {2}, {3}] an API load extension point for loading data types, and interface operations into Sbuilder. After the API load step, a domain model is created using resolver mappers, mapping the names of interface parameters, and definitions, to domain names.

In embedded mode, API loader should allow loading domain model into Sbuilder, as part of API load step, or in a separate step after API load.

Add Properties Loader

Currently, Sbuilder implements possibility, invariant, and assumption -properties. To allow checking correctness of service invocations in a target system, Sbuilder should be added support to define temporal properties. In embedded Sbuilder, it should also be possible to load properties dynamically using an API.

The graph below represents the state space generated for setup4 in version 0.0.8 of sbuilder example. Nodes with yellow color represent time tick 0, pink for tick 1, blue for tick 2, green for tick 3, and gray for tick 4. Diamond shape marks stable states, when no service is executing, i.e. in the initial state, when the previous service has finished execution, or in the final state, when all setup steps have been executed.

setup4.jpg

(Click the image for a larger version)

Expressing temporal properties should allow user to specify constraints (safety properties) on valid sequences of stable states in state space like the one presented above. Plugin implementation takes care of mapping of application state expressions to expressions in the specification model.

----

Footnote: Sbuilder already defines in-transaction -operator, which can be used in identify stable states.

Add Service Loader

Currently, Sbuilder uses static specification snippets from Sbuilder code repository to create runnable specification code. Sbuilder should be added the support to load specification snippets also from external sources.

In a simple scenario, service loader plugin may generate specification snippets using information, which has already been loaded into Sbuilder. For example, service implementation of basic CRUD services may be created using mustache -generator and data-model within Sbuilder -tool.

In a more complex scenario, service loader plugin parses target language, and translates it to TLA+ language snippets. In this case, plugin looks up symbols in Sbuilder, when mapping target language elements to names used within Sbuilder.

Pruning unreachable specification snippets from the resulting specification code should be possible for all snippets, originating from Sbuilder internal code repository, or from an external source.

Add Setup Loader

Sbuilder uses setups to complete runnable specification code, with each setup giving context for an execution. A setup

A setup also maps interfaces to service implementations. Normally this mapping is common for all setups, reflecting the fact that setups represent changes in execution context, and not within the application itself.

It is not reasonable to assume that an application developer on a Sbuilder framework could be trained to craft setup configurations in Sbuilder. Sbuilder should be extended to allow dynamic setup loading.

Basically, a plugin creating setups in Sbuilder works much like test case generator for an implementation. However, unlike an implementation test generator, a setup loader plugin should control binding of input parameters to avoid “evaluating too large sets” in the specification model.

Roadmap

Enhancements outlined in the previous chapter require that Sbuilder should accept configurations, made currently using static files, dynamically via API interfaces. In SBuilder, this involves some refractoring and implementation work, but the effort should not be prohibitive large.

Embedding Sbuilder to a framework is more elusive to define, and obviously depends on the target framework. A proof of concept is required, with the goal to understand at least:

  • number of idiosyncratic concepts, which need to be revealed to framework developers, or component developers
  • constraints imposed on application development, or the application structure in general
  • how scalability issues can be resolved, this includes currently identified issues, and most likely some new ones
  • how well the specification model balances sensitivity and specificity

The picture below sketches steps to increase understanding in these questions:

  • enhance Sbuilder: implement the required extension points in Sbuilder
  • choose traget frawork: current candidates
  • Write Plugins and Embed: indefity minimal viable way to achieve the goals listed above, prepare to iterate Sbuilder API interfaces
  • Create demo application: to get model running, and gain understanding
  • Documentation: in this blog

RoadMap.jpg

Fin

The post has proposed an idea to navigate around resistance involved, when trying to introduce a paradigm change in software development. The focus has been in documenting the what, instead of the how. The interesting question is, whether formal methods could be successfully applied also in smaller organisations.

Advertisements

4 thoughts on “Sbuilder Roadmap

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