Volume 18 Number 4 (Nov. 2023)
Home > Archive > 2023 > Volume 18 Number 4 (Nov. 2023) >
JSW 2023 Vol.18(4): 185-199
doi: 10.17706/jsw.18.4.185-199

Combined Formal Modeling and Model Transformation Based on AADL and Object-Z

Zhengling Guo1, Zining Cao1, 2, 3, 4*

1College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China.
2Science and Technology on Electro-optic Control Laboratory, Luoyang, China.
3Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 210023, China.
4MIIT Key Laboratory of Pattern Analysis and Machine Intelligence, Nanjing, China.

Abstract—Formal methods have become more and more widely used in safety-critical software engineering. A system should be specified with a formal model such as automata, Petri nets, and process algebras to be formally verified. We investigated the AADL combined with Object-Z modeling approach for subsequent formal verification work. The advantage of this is that object-oriented ideas can be used for the AADL modeling process. The space-saving effect is achieved by using class inheritance and polymorphism to extract commonalities. In this paper, we present a new formal model with a more powerful ability——OZIA expressed in the language Object-Z. The transformation rules from the AADL-Object-Z model to the OZIA model are defined to support formal verification. Finally, an example illustrates our results with the Aircraft Landing Process case study.

Index Terms—Object-Z, AADL behavior annex, OZIA, model transformation


Cite: Zhengling Guo, Zining Cao, "Combined Formal Modeling and Model Transformation Based on AADL and Object-Z," Journal of Software vol. 18, no. 4, pp. 185-199, 2023.

Copyright © 2023 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0)

General Information

ISSN: 1796-217X (Online)
Frequency:  Quarterly
Editor-in-Chief: Prof. Antanas Verikas
Executive Editor: Ms. Yoyo Y. Zhou
Abstracting/ Indexing: DBLP, EBSCO, CNKIGoogle Scholar, ProQuest, INSPEC(IET), ULRICH's Periodicals Directory, WorldCat, etc
E-mail: jsweditorialoffice@gmail.com
  • Mar 01, 2024 News!

    Vol 19, No 1 has been published with online version    [Click]

  • Jan 04, 2024 News!

    JSW will adopt Article-by-Article Work Flow

  • Apr 01, 2024 News!

    Vol 14, No 4- Vol 14, No 12 has been indexed by IET-(Inspec)     [Click]

  • Apr 01, 2024 News!

    Papers published in JSW Vol 18, No 1- Vol 18, No 6 have been indexed by DBLP   [Click]

  • Nov 02, 2023 News!

    Vol 18, No 4 has been published with online version   [Click]