Table of Contents
- 1. Sbuilder
- 2. Ruby
- 3. Amazon Web Services
1.1 Background Information
Read an article “How Amazon uses formal methods”
Emerging API Ecosystems
blog entry argues that managing on-line openness has become more important for businesses with the emergence of API ecosystems, and, in the future, it will be even more important as blockchain technologies mature. To help in managing on-line openness this post suggests modeling API ecosystem.
A Tool To Generate Runnable Specification Models in TLA+ language
Announcing Support for Ethereum
Specification Driven Development
post argues that Application Management should use a design model, a representation describing aspects of a system that is not easily, or sufficiently, captured through implementation, in managing on-line openness in IT. The post introduces development architecture and specification driven process resulting to better systems, ease in system development management, ease in system test management, and generally allowing better control of IT development, and explains, how to keep design model and implementation in sync, and how scaling up of the approach is achieved.
Sbuilder Roadmap v3 – aka Introduce Simple ‘Specification Driven Development’ Demo and Point Out Improvements
post introduces Simple “Specification Driven Development” Demo as a way to adapt Formal Methods to application development, also for existing applications. Benefits can be gained immediately in Test Management of System Tests, when using formal model to generate API traces, which are mapped as unit tests on existing application, and the aggregate result of individual unit tests interpreted as an execution of a “virtual” system test – easier to that managing the system test as single unit.
An analysis section identifies several less than optimal development architecture arrangement in the demo, and points out needs for improvements.
Sbuilder Roadmap v2
Sbuilder Roadmap v1
1.3 User’s Guide
SBuilder User’s Guide Blog Series
- Truffle install: documents steps to install Truffle Ethereum development environment to Node-js.
- Sbuilder install: shows steps to install sbuilder-eth GEM to Truffle Ethereum development environment. After installation a minimal configuration is used to validate that the installation was successful.
- Managing state space generation in Sbuilder: expolore, how to state space explosion manifests itself in formal models created by Sbuilder -tool, and how state space explosion can be controlled by limiting cardinality of domain sets in application data model.
- Simple Bank contract: use a simple 10 line Solidity contract containing two (subtle) “bugs” (=violations of correctness promise), and a demonstrates, how to use invariants in Sbuilder to find these violations.
- Sbuilder generated correctness criteria: demonstrates using Sbuilder generated correctness criteria. The criteria presented include ensuring correctness of 1) contract function return values, 2) contract type, and 3) account balances on blockchain.
- Demonstrate Sbuilder Translation Results (Wallet-1): use a very contrived example to demonstrate, how to include manually crafted TLA+ snippets into a formal model created by SBuilder. The main purpose is to 1) show, how to bind TLA code with Solidity interfaces, 2) understand TLA -files generated in Sbuilder translation, and 3) explain, how Sbuilder “possibility” operator relates to model checking formal model correctness. A more realistic example of using manual TLA+ to specify is given in another post.
- Translate Solidity Automatically (Wallet-2): explains how to integrate manually crafted and automatically translated TLA+ snippets to work together in a Sbuilder formal model.
- API Trace Extension Point (Wallet-3): presents how API traces, generated for sbuilder formal models, can be inspected, and how the output can be modified using api-call-init extension point of tla-trace-filter -tool.
Using Sbuilder to Model Business IT Systems
1.4 Developer’s Guide
post examines TLA+tools model checker performance, as a number of states processed per second, when model checking formal models generated by Sbuilder. It finds the performance to be CPU bound, but scalable to match real world applications.
The blog entry demonstrates, how Setups in Sbuilder can be used to manage state space explosion, and associates setups with Use Case Slices to make the idea of managing state space size more comprehensible for developers. Ideally, a Use Case Slice, identified in development, is configured as an Sbuidler Setup and added into a repository for Regression Verification. The objective is to increase confidence in application correctness, and to make QA more efficient with faster feed back because a formal model
- can be executed without the need to have it installed on real production environment, and
- the model checker can effectively check all possible executions in the formal model.
Using Sbuilder to Model a Salesforce Application
2.1 Neo4j stuff
- installing and configuring development server
- starting and stopping development server
- create API session
- creating nodes and relationships using
- using fixed Cypher query language strings
- using Cypher query language strings with parameters
post tests schematron-nokogiri GEM using example case from Combining Schematron with other XML Schema languages.
post demonstrates using Nokogiri::XML::Builder to create a XML document, and schematron-nokogiri to validate the XML document created. Validation schema is built following literate programming principles.
2.3 A Case For RPSPEC Custom Matcher
post first demonstrates, how RSPEC built-in include matcher works in validating one rule, and presents an extension for validating a set of rules.
3 Amazon Web Services
3.1 How I Learned to Stop Worrying and Love AWS
- part1: entry summarizes tools and services Amazon offers for infrastructure management, and presents a personal opinion, and rationale, how to start using them
- part2 : discusses, how to deal with the complexity of CloudFormation templates, and proposes a solution separating configuration data from AWS templates
- part3: introduces aws-must tool, and shows how, an existing CloudFormation JSON can be transformed, in a step-by-step fashion, to Mustache templates with YAML configuration data
3.2 Announcing aws-must-templates
- part1: explains how a YAML configuration can be processed by aws-must tool using aws-must-templates to produce a CloudFormation JSON template.
- part2 : goes trough a scenario starting with installation of aws-must-templates, generating a CloudFormation stack configuration, extending generation process, provisioning CloudFormation stack on Amazon Platform, configuring Test Runner, and using the Test Runner to validate infrastructure correctness
3.3 Using OpenSSH on AWS Platform
- post presents an idea to solve challenges in Amazon EC2 Instance IP Addressing. In short, we synchronize Amazon EC2 instance metadata automatically in OpenSSH Client Configuration file allowing SSH connections to be established using names stored in EC2 Tags. We give an example, and use it to introduce a tool, called aws-ssh-resolver, implementing the idea.
3.4 EC2 Keypairs
blog post demonstrates, how an OpenSSH key can be imported to Amazon platform, how to verify fingerprints, and how to use the keys on a CloudFormation EC2 instance.
3.5 Nat Instance on AWS
blog post uses aws-must-templates to create “a VPC with a public subnet and private subnet, and a network address translation (NAT) instance in the public subnet” similar to scenario 2 in Amazon VPC documentation. Focus is in describing steps needed to setup the environment, to create the stack, and to test the provisioned result on Amazon platform.