1. Home
  2. >
  3. Technology
  4. >
  5. Analytical Verification
  6. >
  7. Design Verification

ASD:Suite© for rapid software design and defect-Free code 

Performs Wide Range of Design Verification

ASD:Suite's patented verification engine is capable of analyzing a wide range of model properties which control many of the common interfaces and interactions present within software models. Verification detects common errors such as deadlocks, while protecting the entire model's integrity by checking for out-of-range conditions such as queue full or non-determinism.  

Using the ASD:Suite to design your software will insure the following:

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 helping design components in ways that are proven never to cause deadlocks and checking that each component itself does not contain deadlocks. 

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:Suite checks that there are no livelock situations in submitted ASD models.

Guard completeness – A guard is a precondition that, when it is true, allows the specified action to execute. The ASD:Suite 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 guards evaluate to false.

Correctly handled race conditions – The term originates with the idea of two signals racing each other to influence the output first. A race condition or race hazard is a flaw in a software design if the output and/or result is unexpectedly and critically dependent on the sequence or timing of other events. The ASD:Suite will flag this for the designer to handle correctly.  

Invariants – An invariant is a precondition that is always true. In ASD, you can specify an invariant per state. The ASD:Suite 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:Suite checks that there is no such illegal behaviour in submitted ASD models.

No state variable out-of-range errors – The ASD:Suite 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:Suite checks that this situation does not occur in submitted ASD models.

Queue optimisation – 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:Suite 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:Suite 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.