Formal modelling and analysis of HLA architectural style

The high level architecture (HLA) was accepted as an IEEE standard in the year 2000 as reference architecture and common infrastructure for large scale distributed interactive simulation systems. But the problems caused by the informal description of the standard are widely recognised. The special requirements of HLA formalisation are analysed and considered as a new architectural style. Combined with the comparison of many architecture description languages (ADLs), the formal models of HLA style are introduced with a newly proposed formal language, π-ADL. These models are grouped as specific architectural concepts of composite, component and connector types. With respect to the different HLA concepts, the models are further described by internal behaviour and external interfaces. They are then tested and analysed with a simple HLA example using the π-ADL compiler π-ADLVM. An HLA internal deadlock reason is found automatically. With the formal specification, a new HLA system design environment is established, which improves the efficiency of the system development.