Formal Analysis of Abstract Behavioural Models Using Automated Deductive Reasoning

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

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.**