Announcing Sbuilder Ethereum

Introduction

This post announces sbuilder-ethereum, a tla-sbuilder plugin, to translate Ethereum implementations in Solidity language into in TLA+ language formal models to be model checked using TLA+ Tools.

:More:

Advertisements

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.

:More:

Using Sbuilder to Model an Application

Introduction

This post explains, how to build a runnable specification model for a Salesforce application in sbuilder-demo GIT repository using tla-sbuilder -tool. The example uses Salesforce API plugin to extract interface specification from Salesforce API metadata.

This post is part part of tla-sbuilder documentation.

:More:

Using Sbuilder to Model Business IT Systems

Introduction

This post uses an example to demonstrate, how business IT system modeling can be supported using Sbuilder -tool. The example mimics a simple Pet Store application with two services. One of the services is used to manage pets, and the other one to manage tags.

The presentation is quite long and technical. Hopefully, comments associated with the YAML, and TLA+ language example snippets, help to follow the idea being presented.

:More:

A Tool To Generate Runnable Specification Models in TLA+ language

Introduction

This post introduces Sbuilder (aka Specification Builder) -tool. Sbuilder generates runnable specification models in TLA+ language for business IT system. Specification model can be verified using TLA+Tools, and parts of it can be presented as implementation blueprints to developers.

:More: