Formal specification at model-level of model-driven engineering using modelling techniques
by H.K. Jnanamurthy; Frans Henskens; David Paul; Mark Wallis
International Journal of Computer Applications in Technology (IJCAT), Vol. 67, No. 4, 2021

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.

Online publication date: Thu, 21-Apr-2022

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computer Applications in Technology (IJCAT):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com