Combining Formal Methods and MDE Techniques for Model-driven System Design and Analysis

摘要: The use of formal methods, based on rigorous math- ematical foundations, is essential for system specificatio n and proof, especially safety critical systems. On the other hand, Model-driven Engineering (MDE) emerging as new approach to software development systematic models primary artifacts throughout engineering life-cycle by com- bining domain-specific modeling languages (DSMLs) with mod el transformers, analyzers, generators. This paper presents our position experience combining flexibility automa tion MDE rigorousness preciseness methods achieve significant boosts in both productivity a nd quality model-driven design analysis An in-the-loop integration proposed where, one principles are used engineer language tool- set around method its practical adoption systems life cycle, and, same context endow precise (possibly) executable semantics perform written those languages. A concrete scenario presented terms Abstract State Machine Eclipse Modeling Framework. allows using Framework Machines seamless way, shown case study. Keywords-Formal methods; Model Driven Engineering; Ab- stract Machines; model semantics; execution