The PIACERE IDE includes, as part of its Verification Tool, a suite of useful static-analysis services to help you validate the architecture described in a DOML model. This is particularly useful to catch issues early within the model and save time down the line. 

The DOML Model Checker (DMC) focus is ensuring that a DOML model respects a set of rules about the configuration of its services, enabling users to intercept errors and misconfigurations before the deployment. 

In the last year the DOML Model Checker expanded its capabilities, such as the addition of a “Cloud Service Provider (CSP) Compatibility Tool”, that produces a compatibility matrix, and a “Net Validation Tool” that verifies whether the networks and addresses specified in the model are valid. 

Users can validate DOML models via the IDE interface, by right-clicking on a DOML file and selecting the corresponding option. When the validation is complete, they will be prompted to save the result report, which can be saved as an HTML file, and viewed in any web browser. 

DOML Model Checker 

The tool leverages the Z3 SMT (Satisfiability Modulo Theories) Solver, by Microsoft Research, to build a logical representation of the architecture and components described in the input DOML model, and subsequently tests it against a selection of rules covering the most common issues. The Z3 SMT solver has proven itself as a very efficient and flexible tool in the industry, and therefore it has been adopted as the ‘core’ of the model checker. 

When a rule is violated, the DMC produces a counterexample for it, detailing when possible which elements are involved. 

Build-in rules include, for example: 

• Every virtual machine has an associated Network Interface. 
• Every Network Interface is unique. 
• All elements in the active concretization are mapped to some abstract infrastructure element. 
• All software components are deployed to some node. 
• All infrastructure elements are deployed in the concretization. 

• All virtual machines in an Auto Scale Group in the infrastructure layer should not be mapped in the concrete layer. 

Expert users can extend the model checker set of requirements using a minimal custom language that can be added in the DOML “functional_requirements” section. It allows to write both simple and complex logical expressions through a natural first-order logic, built on the relationships between DOML elements and their attributes. The language also allows to include or exclude certain requirements by ID, as well as adding CSP Compatibility results to the DMC output. 

CSP Compatibility Tool 

This tool verifies that certain elements in the infrastructure have the required properties in order to be deployed on selected Cloud Service Providers. Such information is contained in YAML files to easily update it. At the moment the following properties are verified: architecture, keypair algorithms, operating system. 

The results are displayed as a matrix, with providers as columns and elements as rows. 

Network Compatibility Tool 

Misconfiguration of networks, especially when manually assigning addresses to resources, can cause issues down the line if there is an error or typo. This tool ensures that networks and subnets are properly declared, and that the network addresses of various elements correctly belong to their networks and there is no conflict between them. When there is a conflict, the involved elements are mentioned in the error message. 

Inner workings 

Behind the scenes, the IDE contacts the DMC server API and submits the model in an exchange format based on XML called DOMLX. 

The DMC then builds an internal representation of the model, which is used by the various modules for validation purposes: 

• The model checker uses this information alongside the set of built-in requirements to determine whether the model is valid, by building a Z3 representation of the model and its constraints. 
• The CSP Compatibility Tool checks whether the values associated with certain infrastructure elements of the DOML are supported by selected cloud service providers. 

• The Network Validation Tool ensures that the network addresses and ranges of various elements are not in conflict. 

A report is generated with the details of the results from the selected tool. 

Interfaces 

While the tool is accessible also via Command Line, the PIACERE IDE utilizes a web API to interface with it. With its latest version, it allows clients to retrieve the output either as HTML or as JSON. 

The JSON endpoint can be used to integrate it into pipelines or other software. 

The HTML version is intended to be read by the users and presents a report with the validation results with a clean and legible UI, easily accessible from any web browser. The report may also include the results of the CSP Compatibility Tool, as well as the Network Validation Tool.