Aerospace is a term used to collectively refer to the atmosphere and outer space. Aerospace activity is very diverse, with a multitude of commercial, industrial and military applications. Aerospace engineering consists of aeronautics and astronautics. Aerospace organizations research, design, manufacture, operate, or maintain aircraft and spacecraft. The beginning of space and the ending of the air is considered as 100 km above the ground according to the physical explanation that the air pressure is too low for a lifting body to generate meaningful lift force without exceeding orbital velocity.

This chapter presents the hybrid Temporal Trace Language (TTL) for formal specification and analysis of dynamic properties of multi-agent systems. This language supports specification of both qualitative and quantitative aspects, and subsumes languages based on differential equations and temporal logics. TTL has a high expressivity and normal forms that enable automated analysis. Software environments for performing verification of TTL specifications have been developed. TTL proved its value in a number of domains.

EUROCONTROL CARE Innovative Research III Problem area It is now generally well realized that the level of safety of air traffic operations depends on the constraints and resources set by people working at the blunt end (e.g. managers), which determine the working conditions and thereby the performance of people (e.g. pilots, controllers) who are directly controlling potentially hazardous processes at the sharp end. Notwithstanding the recognition of the importance of organizational processes for safe operations, formal models describing organizational processes and their effect on safety-relevant scenarios are largely lacking in the current air traffic risk assessment practice.

Each organisation exists or is created for the achievement of one or more goals. To ensure continued success, the organisation should monitor its performance with respect to the formulated goals. In practice the performance of an organization is often evaluated by estimating its performance indicators. In most existing approaches on organization modelling the relation between performance indicators and goals remains implicit. This paper proposes a formal framework for modelling goals based on performance indicators and defines mechanisms for establishing goal satisfaction, which enable evaluation of organizational performance. Methodological and analysis issues related to goals and performance indicators are briefly discussed in the paper. The described framework is a part of a general framework for organization modelling and analysis.