Formal specification at model-level of model-driven engineering using modelling techniques. (16th April 2022)

• Record Type: Journal Article
• Authors: Jnanamurthy, H.K.; Henskens, Frans; Paul, David; Wallis, Mark
• Is Part Of: International journal of computer applications technology. Volume 67:Number 4(2021)
• Page Start: 340
• Page End: 350
• Publication Date: 2022-04-16
• Subjects: model-driven development -- formal specification -- formal verification -- temporal logic -- model-driven architecture; Technology -- Data processing -- Periodicals; 620.00285
• Languages: English
• ISSNs: 0952-8091

Abstract

Nowadays Model-Driven Engineering (MDE) is gaining more popularity due to high-level development leading to a faster generation of executable code, which reduces manual intervention. Verification is crucial at different levels of model-based development. Model-based development, along with formal verification process, assures the developed model satisfies software requirements described in formal specifications. Owing the inadequate knowledge of formal methods (complex mathematical theory), software developers are not adopting formal methods during software development. There are several approaches in the literature available to transform MDE models into formal models directly for formal verification, and these approaches require an additional input of formal specifications to verification tools for formal verification. But these methods have not addressed the problem of formal specifications at the model level. In this paper, we design a modelling framework using modelling techniques, which allows specifying formal properties at the model level, automatically extracting formal specifications and formal models from developed application models, which are used for formal verification. The proposed method allows full automation and reduces the time for formal verification process during the development life-cycle. Furthermore, the method reduces the complexity of learning formal specification notations (specifications specified at the model level are automatically converted into formal specifications), which are required to input verification tools for formal verification.