Modeling and Analysis of the Landing Gear System with the Generalized Contracts
Abdelkader Khouass, christian attiogbé, mohamed messabihi
TL;DR
The paper addresses the escalating complexity of open, heterogeneous systems by introducing the Minarets method, which uses generalized contracts organized by facets to model, compose, and verify interacting components across languages. It extends traditional Assume-Guarantee reasoning with multi-facet contracts and employs PSL as a unifying specification language, enabling facet-by-facet verification using tools like ProMeLa, SPIN, UPPAAL, and ALDEC Active-HDL. Through the Landing Gear System case study, the authors demonstrate normalization, facet decomposition, cross-language modeling, and multi-tool verification, illustrating how their approach reduces integration and analysis difficulty. The work advances practical contract-based verification for heterogeneous architectures and suggests tool-supported workflows to handle facet interdependencies and compatibility concerns in future research.
Abstract
Nowadays, there are several complex systems in different sectors such as aviation, air traffic control ...etc. These systems do not have a precise perimeter, they are open and made of various specific components built with different languages and environments. The modeling, assembly and analysis of such open and complex heterogeneous systems are challenges in software engineering. This paper describes how the Minarets method decreases the difficulty of modeling, composition and analysis of the well known case study of the landing gear system. The method consists in: equipping individual components with generalized contracts that integrate various facets related to different concerns, composing these components according to their facets and verifying the resulting system with respect to the involved facets as well. The proposed method may be used or extended to cover more facets, and by strengthening assistance tool through proactive aspects in modeling, composing multi-facets contracts and finally the verification of the heterogeneous systems.