Formal Analysis of Abstract Behavioural Models Using Automated Deductive Reasoning

随着软件被用于提高世界上如此多的系统和设备的实用性、价值和便利性，软件开发人员面临着管理复杂性和确保质量的重大挑战。创建和使用新的抽象级别是帮助管理复杂性的解决方案之一。 模型驱动工程（MDE）将抽象和分析的思想结合在一起。 在创建模型时，工程师将他们对正在开发的系统的知识编成法典。使用抽象概念创建模型使工程师能够专注于他/她想要编码的重要细节，而不会牺牲模型的未知/不相关方面的精度。汽车、航空航天和运输行业（仅举几例）已经接受了MDE，因为它在提高基于软件的系统的安全性、可靠性和整体管理方面具有潜在的价值。 该提案的重点是为抽象的行为模型开发自动化的形式化方法。形式化方法是用于产生高质量的基于软件的系统的分析方法。诸如模型检查之类的形式化技术象征性地和详尽地检查系统的模型的行为（即，对于所有可能的状态和输入值）。这种分析可以发现模型中的不一致（冲突）、不完整性（缺失案例）和错误。 在开发过程中越早创建模型，就越早实现分析模型的优势。然而，由于不动点计算的迭代性质，具有无限状态空间而不使用抽象的模型的模型检查通常被认为超出了一阶逻辑（FOL）推理机的范围。 基于我们最近的研究结果表明，强大的一阶求解器可以表达一些模型检测问题，而无需不变量，迭代或抽象，我们建议研究使用自动演绎技术进行模型检测。我们将研究建模符号和最佳实践，性能优化，方法（反例和用户反馈）和应用程序。 这项研究的结果将有显着的影响，基于软件的系统的开发，允许创建，形式化的分析，并在直观的抽象层次上编写的模型的修订非常早在MDE过程。

As software is being used to increase the utility, value, and convenience of so many systems and devices in our world, software developers face the significant challenges of managing complexity and assuring quality. Creating and using new abstraction levels is one of the solutions to help manage complexity. Model-driven engineering (MDE) brings together the ideas of abstraction and analysis. In creating models, engineers codify their knowledge of the system under development. Creating models using abstract concepts frees the engineer to concentrate on the important details that s/he wants to codify without sacrificing precision for unknown/irrelevant aspects of the model. The automotive, aerospace, and transportation industries (to name just a few) have embraced MDE for its potential value in improving the safety, security and overall management of software-based systems. This proposal focuses on developing automated formal methods for abstract, behavioural models. Formal methods are analytical methods for producing high quality software-based systems. Formal techniques such as model checking examine the behaviour of a model of a system symbolically and exhaustively (i.e., for all possible state and input values). Such analysis can find inconsistencies (conflicts), incompleteness (missing cases), and errors in the models. The earlier that models can be created in the development process, the earlier that the advantages of analyzing the models can be realized. However, model checking of models with infinite state spaces without the use of abstraction is usually considered beyond the realm of first-order logic (FOL) reasoners because of the iterative nature of the fixed point computation. Based on our recent results showing that powerful first-order solvers can express some model checking problems without invariants, iteration or abstraction, we propose to investigate the use of automated deduction techniques for model checking. We will investigate modelling notations and best practices, performance optimizations, methodology (counterexamples and feedback to the user), and applications. The results of this research will have significant impact on the development of software-based systems by allowing the creation, formal analysis, and revision of models written at an intuitive level of abstraction very early in the MDE process.