Lambda the Ultimate

Hi at all,
I'm an italian student and I'm working on a thesis about semantic verification of xml models in MDA (Model Driven Architecture) context.
MDA is an OMG standard based on visual programming languages and automatic generation of code.
In particoular i'm working on a framework that allows programmers to define SOA three tiers web applications.
The programmer can define frontend and backend of these applications in terms of workflows (i.e. graphs).
The problem is that the syntax of these visual programming languages (the graphs for frontend and backend) is underconstrained, so a programmer can define senseless combinations of states.
There are at least two types of errors:

1) Two (type of) states are connected with a transition, but this transition is semanticaly senseless

2) Two (type of) states are connected with a transition, but a pre/post-condition involving other states doesn't hold. For example a transition between two (type of) states is admitted if and only if there is a transition from the fomer/latter state to another state.

The first type of constraints is easy to impose: a simple table could be added to the framework so these type of senseless cuold be checked on-the-fly.

The second type of constraints involve more complex reasoning, and i think there are basically two types of solutions:

a) To check the models (graphs) defined by the programmers, using techniques inherited from Model Checking (formal verification). In this case the control is a post-development control.

b) To define a precise syntax and semantic using graph grammars. I'm quite ignorant in the domain of graph grammars, so i don't know if these instuments are intended for this purpose.

I'm writing to you 'cause i think the problem about syntax and semantic of visual programming languages is undertheorized.
The first solution i proposed has some problems: model checking is intended to check concurrent system, and not to check the problem i described. On the other and, logic, and CTL logic in particoular, is general enough to represent every type of constraint. Still, there are some computational complexity problems (i.e. state explosion).
The second solution is only a vague idea: i don't know graph grammars...
I would like some opinions, references, suggestions or something else.
I know this post is quite general, but there are too much questions that i will describe later, on demand, in order to avoid to write a too long post.
Best regards,

Alberto