The work Package 2 of the project Mefisto is entitled "Formal specification and verification of user interfaces". As stated in the technical annex, the purpose of this part of the project is to give precise and unambiguous specifications of the tasks to perform in ATC domain, of the possible user behaviour and of the software prototypes to develop. The dimensions of the specifications performed will be suitable to support the development process in an industrial environment. An advantage obtained from the development of these formal specifications will be the possibility to reason about their properties to check whether usability and safety requirements are satisfied. This deliverable deal with part of work produced in the Work Package 2. More precisely, this part of work concerns formal specification of interactive systems. This deliverable describes a formal specification technique dedicated to the formal specification of interactive systems and its application to an Air Traffic Control en-route case study that has been selected in Mefisto project.
The deliverable is split into three documents:
Deliv
4/1: The ICO formal specification technique
This document presents the exhaustive formal definition of the Interactive Cooperative Objects (ICO) formal specification technique. It encom passes the presentation of several formal specification techniques at the basis of the ICO formalism. As ICOs can be seen as being at the top of a pyramid of formal specification techniques, we represent here the evolution from basic Petri nets to ICOs.
This document can be used in different ways:
All the sections of this document follow the same structure. First we present and informal definition of the notation used, then the formal definition is given . This structuring aims at allowing people without a strong background in formal methods to understand the concepts. The document is structured as follows. Section 1 introduces the basic notions of Petri nets. First the syntax is presented, the its associa ted semantics is introduced. Section 2 presents the concepts of Objects Petri nets. These concepts are introduced making references to basic Petri nets introduced in the section 3. Section 4 introduces the Cooperative Objects formalism that is based on th e Objects Petri nets. Section 5 presents the ICO formalism dedicated to the formal specification of interactive applications. Lastly, section 6 presents a complete example of the use of the ICO formalism on a simple application.
Deliv 4/2: Formal Specification of the DRUIDES prototype
This document presents the use of the ICO formalism on the Druides application. The Druides application is a prototype for en-route air traffic control featuring data-link communications facilities. The case study has been pr ovided by CENA and the gathering of information has been performed through various kinds of media:
The aim of this document is threefold:
The use of the formalism follows its formal definition presented in Deliv 4/1. The document is structured as follow. After a short introduction in section 1, section 2 presents in an informal way the Druides application as well as the structure that has been chosen for the specification. Section 3 presents the specification itself. This section follows step by step the structuring introduced in section 2. Last section (section 4) presents two executions of the specific ation. One is dedicated to a non-modal interaction while the other one shows how modal interaction is used in one case in the Druides case study and how it has been specified using the ICO formal specification technique. Druides, as it is a radar screen, allows controllers to handle planes in a graphical way. Using the ICO formalism we describe in Deliv 4/2 most of its features. Indeed, all the possible clearances that can be built using Druides are described in the specification. The data link menu (i.e. how to send data-link requests to planes) is not describe as it is a set of popup menus and submenus, and except the hugeness of its description, it does not present any difficulty to model.
Deliv 4/3: Specification of Middles Touch Screen using Interactive Cooperative Objects
This document presents the use of the Interactive Cooperative Objects formalism for the specification of the touch screen of Middles Air Traffic Control case study. The formalism is used a s presented in Deliv4/1 that describes the semantics and the use of the formalism. As this specification is complementary to the one of Druides in Deliv 4/2 we often refer to this former specification while presenting Middles functionalities. Middles introduces new features compared to Druides. In particular, it introduces a touch screen called touch spots screen . In the first section of the document we present a part of the touch screen specification, in which all the specificities are taken into account. However, in order to make the document simpler and easier to read the complete data link handling and the notion of delayed clearances are not described. In some cases, we have added some screen shots extracted from the tool prototyped by CENA to illustra te parts of the rendering.
Home Overview Contact list Planning of Work Documents Workspace Related Links Statistics