Model Checker

Verum’s ASD:ModelChecker is a hosted application that verifies ASD models

Software architects and designers use the functionality of the ASD:ModelChecker to verify interface, design, usage and general models created using Verum’s ASD:ModelBuilder. The hosted application allows the design of a software component or system to be mathematically verified as complete and correct, even before a single line of code has been written.

Application

The ASD:ModelChecker can be used to verify the design of complex individual software components or entire systems. It accepts input from the desktop model builder application and returns the results to the user’s personal computer. ASD models are sent to the model checker over a secure VPN link in encrypted format.

Functionality

Verum’s ASD:ModelChecker carries out an extensive range of ASD model checks that enable developers to formally verify component and system designs before implementation. Specific checks include:

• Compliance with behavioural laws and safety requirements (if any)
• Elimination of concurrency issues such as deadlocks, livelocks and race conditions
• Checking for completeness of predicates and invariants
• Queue optimizations (also known as yoking)

The model checker produces a failures trace analysis plus supporting data for display by the model builder.

Realization

The ASD:ModelChecker is a highly computing intensive application that is run on dedicated server hardware. Verum provides the model checker as a hosted Software as a Service (SaaS), which enables metrics to be collected and management reports provided.

In this section

• Overview
• ASD:Suite
  • Model Builder
  • Model Checker
  • Code Generator
  • Model Viewer
  • Using the ASD:Suite
  • The ASD:Suite Architecture
• ASD Training
  • Starting ASD
  • Mastering ASD
• Services