Dear John,
This paper works out some of the embedding of SysML into type theory using a real use case. After working on the engineering design modification of the aircraft for two years leading a team using SysML to construct a composite model of the whole problem. A lot of simulation was used to gather evidence as to what would work or not which got represented back into the composite model. The simulations were valid interpretations of the composite model which included the aircraft to be modified as well as a composite model of the physical operating environment.
After doing this which produced results that the domain experts did not expect and initially rejected, I decided to see what it would take to formalize the entire model and prove the conclusions relative to the assumptions represented in the models. The embedding worked well. It enabled me to learn where more expressiveness was needed within SysML, e.g., the need for DL class constructions are used extensively to represent assumptions. The paper deals only with the static case but I think that it is generally clear how to represent the 4D stuff. The most practical inference rules are not clear to me.
- Henson
