¹College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China.
²Science and Technology on Electro-optic Control Laboratory, Luoyang, China.
³Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 210023, China.
⁴MIIT 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

[PDF]

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)