Model verification with extended regular expressions is very useful. In theory, most properties concerning the behavior of a model can be expressed with rules and be written in text files as the input to the rule checker. However, it is not an easy task to write such a rule file with extended regular expressions. The rules in the file may contain errors themselves. As a consequence, the result of this largely manual verification process is unreliable.
This approach can be greatly improved by developing a method to automatically generate rules from other formalisms such as UML sequence diagrams. (However, there is a large gap between the protocol specified in natural language and formal specifications.) The future work in this area will mostly focus on making this approach practical by developing more tools and reducing human intervention.
Model checking, since it is much more formal than model verification, overcomes some of the vulnerabilities of model verification. For example, if a property is formally proved to exist in a model, it always holds no matter how many simulations are made. However, for model verification to reach this certainty, an infinite number of simulations are usually required.
Model checking of DCharts is not easy. This is mainly because DCharts support variables and arbitrary actions that modify those variables. The result of this modification is hardly predictable statically. A promising approach of model checking is to transform DCharts into other formalisms such as PetriNets [42], and formally check the properties of the new models. Graph grammars [43] [44] [45] [33] are useful for model transformation, because of their well-developed theory. In view of this, the future work in the area of model checking will mainly focus on possible transformations from DCharts models to other formalisms by means of graph grammars.