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.