Verifying LTL Properties on Hierarchical Systems: Application to Aircraft Autopilot

In this paper, we are interested in verifying temporal properties of hierarchical systems when states are refined by automata. The system is modeled by hierarchical automata and temporal properties are expressed by the LTL (linear temporal logic). We present a technique to cope with state explosion problem induced by the complexity of the system. The first aim is to define a refinement relation between hierarchical automata. We show that this relation preserves the LTL properties under some conditions. The advantage is that the model checking is done only on an abstraction with few states and the property is preserved in the following refinement process of systems. The second part concerns only local properties specified on the new introduced automata when the systems is refined from the abstract model. We show how to verify an usual class of patterns without using the model checking technique. The proposed approach is illustrated by a simple autopilot control.