Abstraction in model-driven engineering

形式化方法（FM）可以揭示基于计算机的系统中的关键逻辑错误。像英特尔、微软和罗克韦尔柯林斯这样的公司，以及像NASA这样的安全关键系统生产商，都在调查FM，以便在产品部署之前找到漏洞。FM对系统行为进行象征性和详尽的评估。有了这些改进的评估软件质量的能力，我们可以(1)为令人兴奋的应用程序构建具有增加设计复杂性的系统，例如无人驾驶飞机；(2)在关键任务系统（如空中交通管制和医疗设备）中依赖软件完成关键任务；(3)降低开发和维护成本，因为在设计周期中较早发现的错误纠正成本较低。模型驱动工程（MDE）是一种新兴且流行的软件工程过程，其中下游开发工件（例如代码）直接从基于软件的系统的模型派生。FM为这些模型赋予了精确的含义，这反过来又使分析这些模型的目的超越了代码的派生。FM应用于MDE的一个主要挑战是状态空间爆炸问题——尽管计算能力迅速提高，但大多数系统仍然太大，甚至无法对有限的行为集进行详尽的探索。MDE将受益于创建更多抽象模型的能力，以便从系统开发过程的开始就使用它。本研究的目的是研究用户在建模过程中创建的三种类型的抽象是否可以被利用来扩展我们可以在抽象模型的形式分析中探索的状态空间的大小。考虑的三种抽象类型是：语言抽象（由高级建模语言提供的抽象）、结构抽象（如定义）和进化抽象（不完整信息的占位符）。由于这项研究的结果，正式抽象模型将有可能在MDE开发过程中更早地使用，并在整个演化过程中发挥积极的综合作用。

Formal methods (FM) can reveal critical logical errors in computer-based systems. Companies, such as Intel, Microsoft, and Rockwell Collins, and producers of safety-critical systems, such as NASA, are investigating FM to find bugs prior to product deployment. FM evaluate system behaviour symbolically and exhaustively. With these improved capabilities to evaluate software quality, we can (1) build systems with increased design complexity for exciting applications, such as pilotless aircraft; (2) rely on software for critical tasks in mission-critical systems, such as air traffic control and medical equipment; and (3) reduce development and maintenence costs because errors discovered earlier in the design cycle are cheaper to correct. Model-driven engineering (MDE) is an emerging and popular software engineering process in which downstream development artifacts (such as code) are derived directly from a model of a software-based system. FM give a precise meaning to these models, which in turn enables the analysis of these models for purposes beyond just derivation of code. A major challenge in the application of FM for MDE is the state space explosion problem -- the fact that most systems remain too big to explore exhaustively even a finite set of behaviours despite the rapid increase in computing capacity. MDE would benefit from the ability to create more abstract models to enable its use from the beginning of the system development process. The goal of this research is to investigate whether three types of abstractions users create during modelling can be exploited to extend the size of the state space we can explore in formal analysis of abstract models. The three types of abstractions considered are: language abstractions (those provided by high-level modelling languages), structural abstractions (such as definitions), and evolutionary abstractions (placeholders for incomplete information). As a result of this research, it will be possible for formal abstract models to be used earlier in the MDE development process, and play an active, integrated role throughout the evolution process.