# Presentation: 772582

## Slide 1

## Aeronautical Regulations Should BeRigorously Developed Too!

**Aeronautical Regulations Should Be****Rigorously Developed Too!**

**The Sixth NASA Langley Formal Methods Workshop**
- _Eduardo R. L__ó__pez Ruiz_, Yves Ledru and Michel Lemoine

**A Formal Framework for Modeling and Assessing Regulations**

**Notes:**
In aeronautics, formal methods have already been used to specify, analyze and verify aeronautical safety critical systems. This has provided a means of improving the design of such systems prior to their implementation. 

However, we believe that such an approach should not be limited to this type of implementation, but that it should also be extended to the environment around such systems. An important (and key) part of which, are the regulations. 

Therefore, we argue for the use of a formal framework to model and assess these regulations.

## Outline

- Aeronautical Regulations
- Introduction
- Some Case Studies
- An Overview
- Modeling the Regulations
- Integrated Methodology
- Conclusions

**Notes:**
Now, the presentation that I’m going to do here today does not fully follow the abstract submitted, but it is in reality a complement to it. 

A comment that we get is that not all aspects of standards could be specified. We, on our part, do not claim to be able to specify all of the regulations and standards, but we will present to you which types of regulations we have been able to work on, how we have approached them and in which context we have carried out our work

So, this is the outline that I propose to you. I’m going to start off with an overview of aeronautical regulations.... Then I will discuss the manner in which we’ve set about to model the regulations. And finally, before concluding, I will try to bring all of these elements together by describing our methodology

## Aeronautical Regulations - Introduction

- The purview of **aeronautical regulations** is:
-  the facilitation of civil aviation and
-  the prevention of *accidental events* and *intentional acts*, which are detrimental to civil aviation

- Prevention and mitigation of **accidental events**

- Prevention of **intentional acts**

**Safety Regulations**

**Security Regulations**

**Notes:**
The chief objective of civil aviation authorities worldwide is to constantly guarantee the safety and security of the air transport system while, at the same time, facilitating its development. 

For this reason, they have promoted the use of some standardized practices and specifications that target its most detrimental risks. 

At the international level; these specifications and practices are accorded through non-legally binding treaties, but at the national level, these specifications are legally enforced through a regulatory framework.

## Aeronautical Regulations – Some Case Studies

**EDEMOI**
**ICAO’s Annex 17 – *****Security**** -Safeguarding International Civil Aviation against Acts of Unlawful*
**European Regulation (EC) 2320/2002** - *Common rules in the field of civil aviation security*
**NACRE**
**FAR/CS 25 -** *“Airworthiness standards: Transport category airplanes”*

**Notes:**
The methodology which we will describe later has been used in the following projects:

The first, EDEMOI, focused in assessing the regulations that prescribe ground-based security standards. So, the project sought to do this by modeling the security relevant specifications of passengers, their baggage, the different airport areas and the aircraft. This meant specifying parts of ICAO Annex 17, and European Regulation 2320

On the other hand, the NACRE project focused in identifying the design and construction incompatibilities that would arise from a new concept passenger cabin. Noticeably, the safety requirements that would be affected by using “unconventional” seating arrangements for economy and first-class passengers. So, in this project, parts of the FAA’s FAR and the CS  25 were modeled and analyzed. 
You can find the bibliographical trail to these projects through our abstract.

## Aeronautical Regulations - An Overview

**Aeronautical Regulations - An Overview**

- Regulations are validated following a *"peer review"* process

**Notes:**
Now, given that we want to provide a complementing methodology to help improve the development of aeronautical regulations, we have to take a look into the current rulemaking process. Both the FAA and the EASA follow a common procedure for producing rules. Consisting of four phases...     In this procedure proposed regulations are validated using a "peer review" process. However, their own operational feedbacks cast doubt into the effectiveness of this approach...

(@) We know that regulations are : they are written using natural language and so they are inherently ambiguous documents
And furthermore, regulations increasingly cover a wider sphere of application...leading to many interrelationships amongst them
(@) But regulators wish that their regulatory text have one, and only one, possible interpretation Unambiguousness, they don’t want it to contain contradicting policies or assertions Consistency , 
and they want them to exhaustively cover all the possible scenarios within its domain of application Robustness   Moreover, they want the to be evolvable
Additionally ...(@)

## Aeronautical Regulations - An Overview

*Regulations* provide an organizational makeup, which has two components:
-  the horizontal (*temporal*) and
-  the vertical (*hierarchical*) component

- Both are prone to a **regression **
*(i.e. a trend or shift toward a higher risk level)*
- Vertical Component:
-  **Must be congruous/compatible upstream**
-  Can be more restrictive downstream

**Notes:**
(Additionally...) Regulations provide an organizational makeup of safety and security requirements with two components:(@) 
a temporal component , which relates to the amendments undergone by the regulations through the years, and (@)
a hierarchical component, which reflects how lower level regulations are derived from higher level texts
(@) Both components are susceptible to regressions since, independently of their origin and dimension, amendments or specializations can lead to the (unwilling) introduction of new errors. This is especially true for the hierarchical or vertical component, as this component eventually needs to be more restrictive downstream while having to remain compatible upstream.
(@) For example, here we can see a simple comparison between hierarchical levels and between versions. 

## Aeronautical Regulations - An Overview

- They associate each **applicability criterion** to
- a set of ***safety**** *and ***security*** **requirements**

**Requirements**

**Applicability**
**Criteria**

**Regulations**

- The *Applicability Criteria* describe:
-  a **general** **element** or,
-  an **element in a specific state**

- The *Requirements* describe the attributes, capabilities, characteristics,
- or qualities that have been recognized as necessary

**Notes:**
If we now take a closer look into regulations, we can say that regulations associate each applicability criterion to a set of safety and security requirements. (@) 

These requirements, on their part, are linked to the known (or likely) safety risks that they address. (@)

But, what do we refer to by « applicability criteria » and requirements? In fact the applicability criteria are in essence a discriminant. They describe elements  or elements in a specific (valid) state, upon which a given requirement is imposed. 
Whereas requirements, from an engineering sense, identify a necessary attribute, capability, characteristic, or quality of such element. To illustrate, ...(next slide)

In fact, both the applicability criteria andare chosen on the basis that they are criterion relevant to the known (or likely) safety risks. Therefore they imply a knowledge of the contextual environment.

NOTE: This implies the definition of the A.C. (domain of the regulations) and it imposes that all A.C. be linked with a requirement (def. Function)

## Aeronautical Regulations - An Overview

**Aeronautical Regulations - An Overview**

**ICAO Annex 6 - §6.18.2 **From 1 January 2005,
- all turbine-engined aeroplanes of a maximum
- certificated take-off mass in excess of 5,700 kg
- or authorized to carry more than 19 passengers
- shall be equipped with an airborne collision
- avoidance system (ACAS II).

**Notes:**
(To illustrate...) we are going to examine article 6.18.2. from ICAO’s Annex 6, which states that « all turbine-engined aeroplanes of a maximum certificated take-off mass in excess of 5700kg (12,500 lps) or carrying more than 19 PAX shall be equipped with an airborne collision avoidance system (ACAS II) » . 
(@).....(@) (@) (@) 
Higlight importance of each part.
 (End....)

However, (@) today, there is a new paradigm – the VLJs- aircraft with the same performance as larger jets, but with a MCTOW inferior to the 5.7 tons and carrying less than 19 PAX.

It is important to mention that a lot of background and contextual knowledge is required to correctly specify the elements and delineate their transitions between states (if any). This knowledge is usually not found within the regulatory texts, as they are rarely self sufficient documents. 

## Modeling the Regulations

**Modeling the Regulations**

**Linguistic ->** Appropriateness of the text
- Readability, semantics, syntax, pragmatics...
- Unambiguous
**Logical ->** Regulatory principle
- Is it consistent? Is it robust?
**Procedural->** Feasibility of the requirements
- Can it be implemented?

**Notes:**
Finally, the regulatory requirements. 

We target ambiguity at the linguistic level

Consistency and robustness at the logical level

And, sometimes, this has a consequence on the implementation  aspects, as the procedures are developed in accordance with the regulatory principles

## Modeling the Regulations

**Modeling the Regulations**

- We have borrowed tools and techniques from software engineering,
- to describe the regulation’s*** static ***(structural) and ***dynamic*** aspects

- Relevant Infrastructure

**Notes:**
We have borrowed tools and techniques from software engineering to specify and model the applicability criteria along with the contextual knowledge around these elements, such as their structure, their attributes, their allowed operations and relationships. (@)

For example, the static description included the passengers and their baggage, the airport areas and their different requirements, the aircraft interior, ground and air personnel. 
The dynamic aspects focused on the requirements and consequences of the passenger screening process, but also included the check-in process as well as other the nominal and non-nominal passenger behaviors inside the airport.
Requirements to attain the Right-to-Board (i.e. the check-in )and those needed to obtain the Authorization-to-Board (i.e. Screening Checkpoint)

## Integrated Methodology

- Identify the text essential properties
- Filter parasite words, establish key-concepts dictionary
- and identify applicability criteria

- UML Model of the Text Structure
- Delineate its Structure and (inter)link its parts

- UML Model of its Elements and their Environment
- Illustrate applicability criteria and its permutable states

- Formal Model (Z – Alloy combination)

**Alloy**
- Used as a property model checker

**Z**
- Animating and testing targeted
- behaviors/situations

- Original Regulatory Text

- Refinement Level

- 1

- 2

- 3

- 3.a

- 3.b

- ...

**Notes:**
But we also wanted to offer a methodology with multiple refinement levels
With the first level providing the regulatory state-of-affairs, by delineating the regulation’s structure and interrelationships. In practice, this aspect is useful for Document Management and traceability. It also facilitates amendments and regression identification. This requires having identified the text essential properties.
.........Then, the UML model of its elements and environment helps fight the inherent ambiguity of the document and it can be used to facilitate its comprehension/translation as a language-independent reference 
The graphical models created can serve as a reference model and as a support for the evolution of standards.

The Formal specification further elaborates the graphical model but it requires a strong familiarity with the notation.  Benefits from refined pre- and post-conditioning abilities. 
The formal model can be used as a property model checker or for the animating and testing of targeted situations

## Integrated Methodology

**Notes:**
We have used the following methodology to model some aeronautical safety and security requirements. 

(Describe process...)

## Conclusions

- Rigorous formal models of the affected aeronautical regulations were studied and animated to:
- 	(1) help identify the impacts of proposed amendments of regulations and procedures, and
- 	(2) to infer possible solutions for the incompatibilities.
- Used in **NACRE project** - New Aircraft Concepts REsearch
- Used in **EDEMOI project** – Modeling Airport Security
- To be used in **e-COPILOT **-** **Commercial single-pilot aircraft
- To be used in **ISAP **- Integrated System for Air Transport Protection
- A tool in the integration of **VLJ **– Very Light Jets – into European Airspace

**Notes:**
To conclude we know that it is not possible to model all of the regulations. Through the modeling of ICAO’s Annex 17, Regulation (EC) 2320/2002 and FAR/CS 25, this methodology has been proven compatible with the modeling of some Regulations. And, even though these represents a non-negligible part of aeronautical regulations, we are conscious that the usefulness of this methodology may be limited.

However, mathematically-based methods provide the right means to guarantee a better validation process. The methodology described previously has been integrally or partially used in the following European and French projects:

NACRE used in the assessment of the safety properties for a concept passenger cabin 
EDEMOI help evaluate airport security regulations
e-COPILOT used in the assessment of the safety properties for a commercial single-pilot aircraft

- Thank you for your attention
**Eduardo Lopez****	**  	**eduardo.lopez-ruiz@onera.fr**
- Yves Ledru                                 	yves.ledru@imag.fr
- Michel Lemoine                         	michel.lemoine@onera.fr