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.

Notice: This blog post uses mustache includes to load “snippets” into sbuilder formal model. Sbuilder has since been extended with a snippets loader extension points. For an example, refer Specification Driven Development Demo, particularly instructions to create formal model, and more precisely sbuilder.yaml configuration.

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:

Advertisements

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: