Title: Formal specification at model-level of model-driven engineering using modelling techniques

Authors: H.K. Jnanamurthy; Frans Henskens; David Paul; Mark Wallis

Addresses: School of Electrical Engineering & Computing, University of Newcastle, Newcastle, New South Wales, Australia ' School of Electrical Engineering & Computing, University of Newcastle, Newcastle, New South Wales, Australia ' School of Science & Technology, University of New England, Armidale, New South Wales, Australia ' School of Electrical Engineering & Computing, University of Newcastle, Newcastle, New South Wales, Australia

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.

Keywords: model-driven development; formal specification; formal verification; temporal logic; model-driven architecture.

DOI: 10.1504/IJCAT.2021.122345

International Journal of Computer Applications in Technology, 2021 Vol.67 No.4, pp.340 - 350

Received: 22 Apr 2020
Accepted: 07 Nov 2020

Published online: 21 Apr 2022 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article