Next: How to use the language help topics, Previous: Modelling events not visible to the outside world but leading to external visible behaviour, Up: System Decomposition [Contents][Index]
The Dezyne modelling language syntax closely resembles C, C++ and Java, making it easy to work with in terms of data types, scope, and so forth. But you must keep in mind always that the Dezyne Modelling language is truly a modelling language, not a language that directly compiles at the same level of abstraction as C/C++/Java, even though it looks and feels like these familiar languages. Instead, verified Dezyne models ultimately generate real C/C++/Java source code, which in turn goes through standard C/C++/Java compilers or interpreters to become actual machine-executable code.
Models are compiled by Dezyne into formal language which is then model checked (formally verified) by checking every possible path through the communication and state structures of the modelled system, seeking problems such as interface incompliancies, deadlocks, live-locks, race conditions and unhandled events. Each path has steps like "component A presents information x via interface I to component B, and component B responds through interface I, perhaps now or perhaps later (or perhaps never), with information y intended for A, then A presents y or some transformation of y via interface J to component C, …” Sequences matter, but timing does not matter except for the problem case of “never returns”. Dezyne will either find no problems, or it will find one and tell you, the model developer, the exact sequence of communications and actions that leads to the problem.
From this viewpoint, Dezyne and its modelling language are both a specification tool and an exploration tool. You do not need to concern yourself up front about, say, infinite loops or deadlocks; just design what seem to be correct interfaces and component states, and then verify the model. Dezyne will tell you if your conceptual model has a flaw. You might be surprised by what Dezyne tells you. In fact, the power of Dezyne is precisely here: Dezyne uncovers complex, subtle, hard-to-find bugs in your communications and behaviour logic – before you write or generate even one line of C, C++ or Java!