Next: Defensive Design, Previous: Execution Semantics, Up: Dezyne [Contents][Index]
Dezyne provides automated, formal verification of a number of properties of interfaces, of components, and of components in relation to their interfaces6.
By running dzn verify, Dezyne code is translated to
mCRL2 code and fed to a “verification
pipeline”, i.e., a series of mcrl2 and dzn commands
(See Invoking dzn verify).
The checks that Dezyne offers are of properties that are notoriously hard for humans to get right in all their detail, and which are relatively easily translatable to process algebra.
These properties concern the ordering of events, synchronous versus asynchronous calls and transactions, deadlock, unreachable code, livelock, and strict adherence to contract. Verifying a component together with its provides and requires interfaces ensures that the component behaves correctly in its environment according to the specified behavior. It also ensures that all possible error paths are fully and correctly handled.
All properties that Dezyne verifies on interface and component level are compositional, which implies, e.g., that as system consisting of verified components that do not deadlock, is also free of deadlock.