Modelling the Application Layer of an Air Traffic Telecommunications Network using CCS

Dilian Gurov

Swedish Institute for Computer Science

Box 1263

S-164 28 Kista, Sweden

E-Mail: dgurov@sics.se

Bruce Kapron

Department of Computer Science

University of Victoria

Victoria, B.C.

CANADA V8W 3P6

E-mail: bmkapron@uvic.CA

Introduction

The Aeronautical Telecommunications Network (ATN) is being defined by the International Civil Aviation Organization (ICAO) as a digital network for aeronautical communications, via a collection of Standards and Recommended Procedures (SARPS). We have developed, using the SARPS for components of the Application Layer of this network, a model defined in the process algebra language CCS. Using this model and a widely-available verification tool (the Concurrency Workbench,) we have verified that our model satisfies important safety and liveness properties which are specified in the relevant SARPS.

Methodology

Modeling

We modeled the Context Management (CM) Application Service Element (ASE). This application provides the capability to establish a logon between peer ground systems, and between ground and aircraft systems. To obtain a CCS description of the CM-ASE from the ATN SARPS, we followed the approach given below.

First, we identified the architecture, that is the static part of the CM, namely:

the components;
the interface of the components, i.e. all input and output actions (ports) through which the components communicate with their environment;
the internal actions of the components (such as timeout events);
the communications between components which are not visible to the environment of the whole CM.

Then, we considered the dynamics of the components, namely:

we identified the main states of a component, namely the states in which the component is offering its environment the possibility to communicate through more than one action;
what sequences of actions lead from one main state to another.

The SARPS do not follow the above modelling paradigm. The behaviour of the CM is given through separate descriptions of different aspects, such as descriptions of the data, of the valid sequences of messages, and state tables. All these descriptions had to be investigated to answer the above questions and to produce a faithful CCS description. A problem which arose in our approach is that in considering an AE without having modelled the supporting services lead to difficulties in ascertaining aspects of causality, namely which agents initiate various events. In the SARPS, no distinction is made between internal and external events. Also, it is not clearly specified how the different protocols are supposed to interleave. Without this information it is impossible to guarantee certain properties like deadlock avoidance.

Verification

Having developed a model, we then proceeded to verify various properties of the system. These fall into two categories. First, we checked standard safety properties, such as deadlock and livelock avoidance. We also interpreted message sequence charts given in the SARPs as liveness properties, and checked that these were satisfied by the CCS model. All properties were expressed in the mu-calculus, a very powerful logic for expressing temporal properties of systems. The checking was done automatically, using the Concurency Workbench of North Carolina (CWB-NC).

The Model

The model is written in CCS, in the format specified for CWB-NC

******************************************************************************
* cm.ccs  
*
* The Context-Manager-ASE of the ATN SARPs.
*
******************************************************************************

******************************************************************************
* CM-Air-ASE:

proc	CM-Air = CM-Air-IDLE

proc	CM-Air-IDLE =
	  d-start-ind-cmupdate.'cm-update-ind.'d-start-rsp-neg.CM-Air
	+ d-start-ind-cmcontact-req.'cm-contact-ind.CM-Air-CONTACT
	+ cm-logon-req.'d-start-req-cmlogon-req.CM-Air-LOGON

proc	CM-Air-LOGON =
	  d-start-cnf-pos.'cm-logon-cnf-pos.CM-Air-DIALOGUE
	+ d-start-cnf-neg.'cm-logon-cnf-neg.CM-Air
	+ cm-user-abort-req.'d-abort-req-user.CM-Air
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Air
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Air
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Air
	+ t.'d-abort-req-provider.'cm-provider-abort-ind.CM-Air	
	  *** Logon Timout ***

proc	CM-Air-CONTACT =
	  cm-contact-rsp.'d-start-rsp-pos.CM-Air
	+ cm-user-abort-req.'d-abort-req-user.CM-Air
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Air
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Air
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Air

proc 	CM-Air-DIALOGUE =
	  d-data-ind-cmupdate.'cm-update-ind.CM-Air-DIALOGUE
	+ d-data-ind-cmcontact-req.'cm-contact-ind.CM-Air-CONTACT-DIALOGUE
	+ d-end-ind.'cm-end-ind.'d-end-rsp-pos.CM-Air
	+ cm-user-abort-req.'d-abort-req-user.CM-Air
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Air
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Air
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Air

proc	CM-Air-CONTACT-DIALOGUE =
	  cm-contact-rsp.'d-data-req.CM-Air-DIALOGUE
	+ cm-user-abort-req.'d-abort-req-user.CM-Air
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Air
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Air
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Air


******************************************************************************
* CM-Ground-ASE:

proc 	CM-Ground = CM-Ground-IDLE

proc 	CM-Ground-IDLE =
	  d-start-ind-cmlogon-req.CM-Ground-IDLE1
*	+ d-start-ind-cmforward-req.CM-Ground-IDLE2
	+ cm-update-req.'d-start-req-cmupdate.CM-Ground-UPDATE
	+ cm-contact-req.'d-start-req-cmcontact-req.CM-Ground-CONTACT
*	+ cm-forward-req.'d-start-req-cmforward-req.CM-Ground-FORWARD
proc 	CM-Ground-IDLE1 =
	  t.'cm-logon-ind.CM-Ground-LOGON
	+ t.'d-start-rsp-neg.CM-Ground	
	  *** Choice resolved by the respective Version Numbers ***
proc	CM-Ground-IDLE2 =
	  'cm-forward-ind.'d-start-rsp-pos.CM-Ground
	+ 'd-start-rsp-neg.CM-Ground

proc	CM-Ground-LOGON =
	  cm-logon-rsp-pos.'d-start-rsp-pos.CM-Ground-DIALOGUE
	+ cm-logon-rsp-neg.'d-start-rsp-neg.CM-Ground
	+ cm-user-abort-req.'d-abort-req-user.CM-Ground
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Ground
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Ground
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Ground

proc	CM-Ground-UPDATE =
	  d-start-cnf-neg.CM-Ground
	+ cm-user-abort-req.'d-abort-req-user.CM-Ground
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Ground
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Ground
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Ground
	+ t.'d-abort-req-provider.'cm-provider-abort-ind.CM-Ground	
	  *** Update Timeout ***

proc	CM-Ground-CONTACT =
	  d-start-cnf-pos.'cm-contact-cnf.CM-Ground
	+ cm-user-abort-req.'d-abort-req-user.CM-Ground
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Ground
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Ground
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Ground
	+ t.'d-abort-req-provider.'cm-provider-abort-ind.CM-Ground	
	  *** Contact Timeout ***

proc 	CM-Ground-DIALOGUE =
	  cm-update-req.'d-data-req-cmupdate.CM-Ground-DIALOGUE
	+ cm-contact-req.'d-data-req-cmcontact-req.CM-Ground-CONTACT-DIALOGUE
	+ cm-end-req.'d-end-req.CM-Ground-END
	+ cm-user-abort-req.'d-abort-req-user.CM-Ground
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Ground
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Ground
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Ground

proc	CM-Ground-CONTACT-DIALOGUE =
	  d-data-ind.'cm-contact-cnf.CM-Ground-DIALOGUE
	+ cm-user-abort-req.'d-abort-req-user.CM-Ground
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Ground
	+ d-abort-ind-user.'cm-user-abort-ind.CM-Ground
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Ground

proc	CM-Ground-END =
	  d-end-cnf-pos.CM-Ground
	+ d-abort-ind-provider.CM-Ground
	+ d-abort-ind-user.CM-Ground
	+ d-p-abort-ind.CM-Ground
	+ t.'d-abort-req-provider.CM-Ground	
	  *** End Timeout ***

proc	CM-Ground-FORWARD =
	  d-start-cnf-pos.'cm-forward-cnf-pos.CM-Ground
	+ d-start-cnf-neg.'cm-forward-cnf-neg.CM-Ground
	+ cm-user-abort-req.'d-abort-req-user.CM-Ground
	+ d-abort-ind-provider.'cm-provider-abort-ind.CM-Ground
	+ d-p-abort-ind.'cm-provider-abort-ind.CM-Ground
	+ t.'d-abort-req-provider.'cm-provider-abort-ind.CM-Ground	
	  *** Forward Timeout ***


******************************************************************************
* CM-Air-1, an instance of a CM-Air-ASE:

proc	CM-Air-1 =
	CM-Air[	a1-d-start-req-cmlogon-req / d-start-req-cmlogon-req,
		a1-d-start-ind-cmupdate / d-start-ind-cmupdate,
		a1-d-start-ind-cmcontact-req / d-start-ind-cmcontact-req,
		a1-d-start-rsp-pos / d-start-rsp-pos,
		a1-d-start-rsp-neg / d-start-rsp-neg,
		a1-d-start-cnf-pos / d-start-cnf-pos,
		a1-d-start-cnf-neg / d-start-cnf-neg,
		a1-d-data-req / d-data-req,
		a1-d-data-ind-cmupdate / d-data-ind-cmupdate,
		a1-d-data-ind-cmcontact-req / d-data-ind-cmcontact-req,
		a1-d-end-ind / d-end-ind,
		a1-d-end-rsp-pos / d-end-rsp-pos,
		a1-cm-logon-req / cm-logon-req,
		a1-cm-logon-cnf-pos / cm-logon-cnf-pos,
		a1-cm-logon-cnf-neg / cm-logon-cnf-neg,
		a1-cm-update-ind / cm-update-ind,
		a1-cm-contact-ind / cm-contact-ind,
		a1-cm-contact-rsp / cm-contact-rsp,
		a1-cm-end-ind / cm-end-ind,
		a1-cm-provider-abort-ind / cm-provider-abort-ind,
		a1-cm-user-abort-req / cm-user-abort-req,
		a1-cm-user-abort-ind / cm-user-abort-ind,
		a1-d-abort-req-provider / d-abort-req-provider,
		a1-d-abort-req-user / d-abort-req-user,
		a1-d-abort-ind-provider / d-abort-ind-provider,
		a1-d-abort-ind-user / d-abort-ind-user,
		a1-d-p-abort-ind / d-p-abort-ind ]


******************************************************************************
* CM-Ground-1, an instance of a CM-Ground-ASE:

proc	CM-Ground-1 =
	CM-Ground[
		g1-d-start-req-cmupdate / d-start-req-cmupdate,
		g1-d-start-req-cmcontact-req / d-start-req-cmcontact-req,
		g1-d-start-req-cmforward-req / d-start-req-cmforward-req,
		g1-d-start-ind-cmlogon-req / d-start-ind-cmlogon-req,
		g1-d-start-ind-cmforward-req / d-start-ind-cmforward-req,
		g1-d-start-rsp-pos / d-start-rsp-pos,
		g1-d-start-rsp-neg / d-start-rsp-neg,
		g1-d-start-cnf-pos / d-start-cnf-pos,
		g1-d-start-cnf-neg / d-start-cnf-neg,
		g1-d-data-req-cmupdate / d-data-req-cmupdate,
		g1-d-data-req-cmcontact-req / d-data-req-cmcontact-req,
		g1-d-data-ind / d-data-ind,
		g1-d-end-req / d-end-req,
		g1-d-end-cnf-pos / d-end-cnf-pos,
		g1-cm-logon-ind / cm-logon-ind,
		g1-cm-logon-rsp-pos / cm-logon-rsp-pos,
		g1-cm-logon-rsp-neg / cm-logon-rsp-neg,
		g1-cm-update-req / cm-update-req,
		g1-cm-contact-req / cm-contact-req,
		g1-cm-contact-cnf / cm-contact-cnf,
		g1-cm-end-req / cm-end-req,
		g1-cm-forward-req / cm-forward-req,
		g1-cm-forward-ind / cm-forward-ind,
		g1-cm-forward-cnf-pos / cm-forward-cnf-pos,
		g1-cm-forward-cnf-neg / cm-forward-cnf-neg,
		g1-cm-provider-abort-ind / cm-provider-abort-ind,
		g1-cm-user-abort-req / cm-user-abort-req,
		g1-cm-user-abort-ind / cm-user-abort-ind,
		g1-d-abort-req-provider / d-abort-req-provider,
		g1-d-abort-req-user / d-abort-req-user,
		g1-d-abort-ind-provider / d-abort-ind-provider,
		g1-d-abort-ind-user / d-abort-ind-user,
		g1-d-p-abort-ind / d-p-abort-ind ]


******************************************************************************
* CM-Medium-Air-to-Ground:

proc	CM-M-A1-G1 =
	  a1-d-start-req-cmlogon-req.'g1-d-start-ind-cmlogon-req.CM-M-A1-G1
	+ a1-d-start-rsp-pos.'g1-d-start-cnf-pos.CM-M-A1-G1
	+ a1-d-start-rsp-neg.'g1-d-start-cnf-neg.CM-M-A1-G1
	+ a1-d-data-req.'g1-d-data-ind.CM-M-A1-G1
	+ a1-d-end-rsp-pos.'g1-d-end-cnf-pos.CM-M-A1-G1
	+ a1-d-abort-req-provider.'g1-d-abort-ind-provider.CM-M-A1-G1
	+ a1-d-abort-req-user.'g1-d-abort-ind-user.CM-M-A1-G1


******************************************************************************
* CM-Medium-Ground-to-Air:

proc	CM-M-G1-A1 =
	  g1-d-start-req-cmupdate.'a1-d-start-ind-cmupdate.CM-M-G1-A1
	+ g1-d-start-req-cmcontact-req.'a1-d-start-ind-cmcontact-req.CM-M-G1-A1
	+ g1-d-start-req-cmforward-req.'a1-d-start-ind-cmforward-req.CM-M-G1-A1
	+ g1-d-start-rsp-pos.'a1-d-start-cnf-pos.CM-M-G1-A1
	+ g1-d-start-rsp-neg.'a1-d-start-cnf-neg.CM-M-G1-A1
	+ g1-d-data-req-cmupdate.'a1-d-data-ind-cmupdate.CM-M-G1-A1
	+ g1-d-data-req-cmcontact-req.'a1-d-data-ind-cmcontact-req.CM-M-G1-A1
	+ g1-d-end-req.'a1-d-end-ind.CM-M-G1-A1
	+ g1-d-abort-req-provider.'a1-d-abort-ind-provider.CM-M-G1-A1
	+ g1-d-abort-req-user.'a1-d-abort-ind-user.CM-M-G1-A1


******************************************************************************
* CM-Supporting-Service:

proc	CM-Supporting-Service =
	CM-M-A1-G1 | CM-M-G1-A1


******************************************************************************
* CM-Service-Provider:

proc	CM-Service-Provider =
	( CM-Air-1 | CM-Supporting-Service | CM-Ground-1 ) \ Internals

set	Internals = 
	{ a1-d-start-req-cmlogon-req, g1-d-start-ind-cmlogon-req,
	  a1-d-start-rsp-pos, g1-d-start-cnf-pos,
	  a1-d-start-rsp-neg, g1-d-start-cnf-neg,
	  a1-d-data-req, g1-d-data-ind,
	  a1-d-end-rsp-pos, g1-d-end-cnf-pos,
	  a1-d-abort-req-provider, g1-d-abort-ind-provider,
	  a1-d-abort-req-user, g1-d-abort-ind-user,
	  g1-d-start-req-cmupdate, a1-d-start-ind-cmupdate,
	  g1-d-start-req-cmcontact-req, a1-d-start-ind-cmcontact-req,
	  g1-d-start-req-cmforward-req, a1-d-start-ind-cmforward-req,
	  g1-d-start-rsp-pos, a1-d-start-cnf-pos,
	  g1-d-start-rsp-neg, a1-d-start-cnf-neg,
	  g1-d-data-req-cmupdate, a1-d-data-ind-cmupdate,
	  g1-d-data-req-cmcontact-req, a1-d-data-ind-cmcontact-req,
	  g1-d-end-req, a1-d-end-ind,
	  g1-d-abort-req-provider, a1-d-abort-ind-provider,
	  g1-d-abort-req-user, a1-d-abort-ind-user,
	  a1-d-p-abort-ind, g1-d-p-abort-ind }

The Specification

A number of liveness properties specified in the SARPS (using message sequence charts,) along with a some obvious safety properties, were specfied in the mu-calculus, and verified against the model given about using CWB-NC.

*******************************************************************************
* cm.mu  
*
* Properties of the Context-Manager-ASE described in cm.ccs
*
*******************************************************************************
*
* SAFETY PROPERTIES:  (i.e. properties of type: "AG not bad-property")
*
* no-deadlock	- deadlock "[-{}]ff" is a bad property;
*
* no-livelock	- the possibility of livelock "max Z = Z" is a bad property.
*
*
* LIVENESS PROPERTIES:
*
*  - checking the Message-Sequence-Charts.
*
*******************************************************************************
* Safety Properties:

prop no-deadlock	= AG not [-{}]ff

prop no-livelock	= AG not (max Z = Z)


*******************************************************************************
* Liveness Properties:

prop MSC-1a	= <> 
		  <<'g1-cm-logon-ind>>
		  <> 
		  <<'a1-cm-logon-cnf-pos>> tt	*** DIALOGUE

prop MSC-1b	= <> 
		  <<'g1-cm-logon-ind>>
		  <> 
		  <<'a1-cm-logon-cnf-neg>> tt

prop MSC-2	= <> 
		  <<'a1-cm-logon-cnf-neg>> tt

prop MSC-3	= <> 
		  <<'a1-cm-update-ind>> tt

prop MSC-4	= <> 
		  <<'g1-cm-logon-ind>>
		  <> 
		  <<'a1-cm-logon-cnf-pos>>	*** DIALOGUE
		  <>
		  <<'a1-cm-update-ind>> tt

prop MSC-9	= <>
		  <<'a1-cm-contact-ind>>
		  <>
		  <<'g1-cm-contact-cnf>> tt

prop MSC-10	= <> 
		  <<'g1-cm-logon-ind>>
		  <> 
		  <<'a1-cm-logon-cnf-pos>>	*** DIALOGUE
		  <>
		  <<'a1-cm-contact-ind>>
		  <>
		  <<'g1-cm-contact-cnf>> tt

prop MSC-11	= <> 
		  <<'g1-cm-logon-ind>>
		  <> 
		  <<'a1-cm-logon-cnf-pos>>	*** DIALOGUE
		  <>
		  <<'a1-cm-end-ind>> tt

prop MSC-14	= <> 
		  <<'g1-cm-logon-ind>>
		  <> 
		  <<'a1-cm-logon-cnf-pos>>	*** DIALOGUE
		  <> 
		  <<'g1-cm-user-abort-ind>> tt

prop MSC-15	= <> 
		  <<'g1-cm-logon-ind>>
		  <> 
		  <<'a1-cm-logon-cnf-pos>>	*** DIALOGUE
		  <> 
		  <<'a1-cm-user-abort-ind>> tt