Using the ASD:Suite
How Verum’s fully integrated ASD development toolset helps developers create defect free code
The functionality of the ASD:Suite enables software architects and designers to achieve significantly increased productivity and quality during the development of a complex software component or system.
With Verum’s ASD:Suite you can:
Verify the behaviour of a software design
The ASD:Suite is the only toolset that provides software developers with the ability to precisely verify 100% of the behaviour of a software design before a single line of software has been written. This is something that is not possible to achieve with a conventionally implemented software system.
Demonstrate that a software design meets system specifications
The ASD:Suite is also the only toolset with the ability to formally show that the design of a software system meets its requirements, for the first time providing complete traceability of requirements through to implementation.
Ensure completeness of software specifications and designs
The ASD:Suite uniquely ensures the completeness of software requirements and designs in a manner that is rigorous, precise and yet completely transparent to all the technical and domain experts involved in the project.
The ASD:Suite step-by-step
Step 1: Modelling
Based on a first list of requirements and a defined system context, the software developer uses the ASD:ModelBuilder to capture, in one or more ASD interface models, the behaviour of the component or system from a black box point of view. An interface model is an abstraction that allows the external behaviour to be defined independently of any specific implementation.
Once all the externally visible behaviour has been specified, the developer uses the model builder to capture the inner behaviour of the component or system in an ASD design model.
All ASD components must have both an interface and a design model.
Step 2: Model checking
The ASD:ModelChecker is used to detect errors in ASD interface design models. Removing these errors ensures that source code generated will work correctly and be defect free.
The table below provides further details about the analysis performed by the model checker.
Step 3: Generating code
Once a model has been verified, with one click of a button the software developer can send the model to the ASD:CodeGenerator. All of an ASD model’s code can be generated automatically in a target source code selected by the user. The code generated is guaranteed to be correct and defect free. It is delivered as human readable source code, formatted to a standardized layout. Stubs can be provided for hand-written code: for example, where an existing algorithm needs to be used.
Analysis performed by the model checker
No deadlocks |
A deadlock is a situation where two or more system components or process threads cannot make progress because they waiting for each other. Deadlocks can be hard to find because the entire system needs to be reviewed to discover them: for example, component A might be waiting for B, which is waiting for C, while C is waiting for A. The ASD:Suite ensures this never happens by:
|
No livelocks |
Livelock is the situation where a system is so busy that it does not or cannot interact with the outside world. An example of a cause of livelock is an infinite loop. The ASD:ModelChecker checks that there are no livelock situations in submitted ASD models. |
Predicate completeness |
A predicate is a precondition that, when it is true, allows the specified action to execute. The ASD:ModelChecker checks that all possible values of associated state variables can actually occur in each state. Otherwise, the system would not know what to do when all predicates evaluate to false. |
No race conditions |
A race condition or race hazard is a flaw in a software design whereby the output and/or result is unexpectedly and critically dependent on the sequence or timing of other events. The term originates with the idea of two signals racing each other to influence the output first. |
Invariants |
An invariant is a precondition that is always true. In ASD, you can specify an invariant per state. The ASD:ModelChecker checks invariants that should always evaluate to true when the system is in each state. |
Absence of illegal behaviour |
An ASD design should make proper use of library components and adhere to their interface specifications. A simple example of illegal behaviour would be trying to turn on a function that has already been turned on. The ASD:ModelChecker checks that there is no such illegal behaviour in submitted ASD models. |
No state variable out-of-range errors |
The ASD:ModelChecker checks that defined ranges of state variables are not exceeded. |
Determinism |
ASD requires all designs to be deterministic. The most common cause of non-determinism is overlapping predicates, which occurs when predicates are specified within a single rule such that more than one of them can evaluate to true at the same time. In this case, there is no defined deterministic choice between the competing rule cases. The ASD:ModelChecker checks that this situation does not occur in submitted ASD models. |
Queue optimization |
An ASD design which has used components with call-back channels also has a queue. This queue is where call-backs are stored before they are processed. A queue size can be set for each ASD design model. The ASD:ModelChecker checks that the queue does not get full, i.e. that it remains non-blocking. |
Implementation vs. specification |
In general, software systems are first specified and then implemented. The implementation must adhere to the specification. The ASD:ModelChecker checks that a component specification has been correctly implemented, both when it is playing the role as a used component and when it is managing its own used components. These are two independent checks. The refinement check makes the connection or the transitivity between the two otherwise independent checks. If the refinement check is broken, it is not guaranteed that the component can both serve its client and use its subordinates correctly. The mathematical term for this is that the design refines its interface – it is a more specific version of it. |
Get in touch
For more information or a product demonstration contact us.
 |
+31-40-2359090 |
 |
+31-40-2359099 |
 |
info@verum.com |
 |
Location |
