Abstraction in model-driven engineering

点击翻译按钮获取中文摘要

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.