Formal Analysis of Abstract Behavioural Models Using Automated Deductive Reasoning

使用自动演绎推理对抽象行为模型进行形式化分析

• 批准号: RGPIN-2016-03992
• 负责人: Day, Nancy
• 金额: $ 2.26万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=708846
• 关键词: Formal; Analysis; Abstract; Behavioural; Models

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.

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