Code generation and Godel's genie
Many of the advantages gained by generating executable code from models are matched by various problems. At any particular level of abstraction, analysis and requirements languages like UML, Z and OCL are wonderful for specifying, with varying levels of precision, the constraints for the next, more-detailed model.
Model-driven architecture and code generation involve executing a series of transformations which use as input the higher level of abstraction to produce the more detailed architecture layer as output. The usual practice is to elaborate additional details of implementation in the more-detailed layer: The logical layer is used to generate the physical layer; the platform-independent model is used to generate the platform-specific model.
The problem with generating executable code is that the model language has been morphed into an implementation meta-language. When there is no room for elaboration because the model contains all the necessary details then the model is itself the implementation. The problem of verification has to be generalised from using the model to verify the implementation to one of verifying the model itself.
Godel's incompleteness theorem essentially says, in this context, that in-principle we cannot verify the model or its elaborated implementation. Hofstadter might say the meta-genie has been let out of the bottle. We verify models by inspection, consistency checking and theorem proving, when possible; likewise we verify implementations by inspection and the closest thing we have to theorem proving, i.e. testing.
The key assumption of testing is that we can verify the implementation against a subset of test vectors representing equivalence sets across the input domain. The key for code generation is that the set of valid assumptions embodied in the model is retained by an isomorphic transformation from the model into the implementation. Model consistency checking does not help if the model is inconsistent or any of its assumptions have been invalidated by the process of elaboration.
Model-driven architecture and code generation involve executing a series of transformations which use as input the higher level of abstraction to produce the more detailed architecture layer as output. The usual practice is to elaborate additional details of implementation in the more-detailed layer: The logical layer is used to generate the physical layer; the platform-independent model is used to generate the platform-specific model.
The problem with generating executable code is that the model language has been morphed into an implementation meta-language. When there is no room for elaboration because the model contains all the necessary details then the model is itself the implementation. The problem of verification has to be generalised from using the model to verify the implementation to one of verifying the model itself.
Godel's incompleteness theorem essentially says, in this context, that in-principle we cannot verify the model or its elaborated implementation. Hofstadter might say the meta-genie has been let out of the bottle. We verify models by inspection, consistency checking and theorem proving, when possible; likewise we verify implementations by inspection and the closest thing we have to theorem proving, i.e. testing.
The key assumption of testing is that we can verify the implementation against a subset of test vectors representing equivalence sets across the input domain. The key for code generation is that the set of valid assumptions embodied in the model is retained by an isomorphic transformation from the model into the implementation. Model consistency checking does not help if the model is inconsistent or any of its assumptions have been invalidated by the process of elaboration.
posted by Daniel Berinson at 8:14 PM
0 comments
