Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

An interactive software is a computer application which reacts, throughout its execution, to various sources of events. In particular, it produces a perceptible representation of its internal state [1, 2]. However, the usability of an interactive application can be appreciably impacted by the delays of propagation of data and events and by its variations, i.e. latency and jitter. The problem is striking for applications involving tactile interactions or augmented reality, where the shifts between interaction and representation can make the system unusable [3, 4]. Yet, while latency constraints are expressed at specification, they are often taken into account only very late in the development processes, generally by experimental a posteriori measurements, when the system is fully implemented. For instance, in some air traffic control systems such as radar visualization or remote tower, latency in the visualization of aircrafts position (and the shifts between their real position) is evaluated during experiments. Instead of redesigning the software, this may conduct to dimension the spacing limits between aircrafts [5], with direct consequences on the capacities of air traffic management.

More generally, when focusing on aeronautical software systems, the processes of certifications described in the DO-178C/ED-12C offer an important place to formal checking. We want to take the opportunity to use formal tools and techniques to handle latency in interactive software. We are particularly interested in the Smala language, dedicated to interactive systems.

2 Djnn and Smala

SmalaFootnote 1 is a language that has been designed to effectively support the development of reactive applications. Smala is built on the top of a set of C libraries named DjnnFootnote 2. Djnn provides a core library that implements the execution engine allowing to run a tree of components [6].

Fig. 1.
figure 1

Tree of Djnn components for an interactive software

Full size image

Once the tree is loaded and started, the core library starts an event loop that fairly manages the events coming from the environment. On arrival, events are dispatched to the tree components. The control structures contained in this tree specify an activation graph through which the events are propagated Fig. 1.

Djnn provides libraries with various components, ranging from components for arithmetic, logic, finite state machines to graphical shapes, style components, and geometric transformations. Three rendering engines are available, one based on the Qt toolkit, another one based on Cairo, and a third one based on OpenGL.

It is possible to build a tree of components by directly using these libraries and the C language. However the task is akin to those of writing an abstract syntax tree. Thus, we designed Smala so as to provide a dedicated syntax with specific symbols that helps to visualize the interaction between components. Smala comes with a compiler that transforms the Smala program into a program written in the C language.

2.1 Smala Applications

Here we describe a part of a demo we developed with Smala to show some interesting points of the language. The objective was to implement a Navigation Display (ND), a standard navigation tool integrated in modern cockpits of airplanes, enhanced with interaction capacities. The ND was designed to be integrated within a full software simulator of an Airbus A320 (Prepar3D/A320 FMGS). In this paper, we will focus on the design of the interaction with a waypoint to show the expressiveness of the smala language.

Fig. 2.
figure 2

Navigation Display Experiment and design of interaction with a waypoint

Full size image

A flight plan mainly consists in a sequence of waypoints specifically selected for a flight before the take off. During the flight, the pilot in command might want to alter the flight plan (e.g. for meteorological reasons) and head the plane directly to another waypoint. We implemented this action on the ND with a touch command that triggers the flight management system to head to the selected waypoint. A sketch of the interaction is shown in Fig. 2: after a touch on a waypoint, a box appears with the text “DIRECT TO”, that will stay for 3 seconds. If the pilot touches this box, the command will be send to the flight management system.

The code for the smala component “waypoint” is shown in Fig. 3. This component has two states: when idle (default state) it is represented with a large triangle, including a small square at its exact position and a text label giving its name. When selected, its color must change to green and we add the box with the text “DIRECT TO”. The basic graphical components of smala are used (Rectangle, Polygon, Colors...) and a finite state machine (FSM) is explicitely programmed to represent both states and the triggers that change the states. Thus, the component will be selected when a press will be detected inside the triangle (idle.pol.press). It will return to the idle state when either a timeout occurs or if a press is detected inside the “DIRECT TO” box (selected.rdt.press). That last action will trigger the sending of a specific message on the communication bus that links the software to the simulator.

Fig. 3.
figure 3

Smala code for a waypoint

Full size image

As a real-world example, we also completely developed the HMI of Volta, the first conventional all-electric helicopter [7]. The HMI has been built concurrently by a programmer and a graphic designer, demonstrating another powerful aspect of our approach: the strict separation of concerns between the design of the visualization and the implementation of interactions.

3 Our Approach to Handle Latency

3.1 Formal Activities Around Djnn/Smala

Although Smala is still under development, we already could experiment formal techniques for checking properties of Smala programs. For instance, we exploited the characteristics of the graph of activation [8]. This graph, deduced from the Smala code, provides all the possible activation relationships following the occurrence of an event. Thus, we managed to formally check attainability properties (i. e., an entry always ends up generating an expected exit or an alarm is always turned off in a certain configuration) or causal activation relationships (i. e., a displayed error message will never be covered by another).

In addition, with the experience gained from previous work on dedicated language and formal validation [9], we experimented in [10] the transformation of Smala code into Petri nets, with the idea to precisely define an operational semantics for Smala and to benefit from the associated formal tools and techniques. As a result, the semantics of Smala is currently under publication in a dedicated paper.

Our medium-term prospects concern the prolongation of the previous studies (based on the graph of activations) and the study of formal proof techniques applied to Smala code (translation into Caml and use of COQ, translation into Event-B).

3.2 Towards Handling Latency

We want to focus on software layers. Indeed, handling latency can be made at the hardware level with specific tools [11]. However, the end-to-end approaches existing today [12] do not allow to understand the specific issues related to software architecture choices. They are only usable to measure the latency when the system is in its validation phase.

The classical formal approach to handle latency in software systems is to consider their Worst-Case Execution-Time (WCET) [13]. WCET tools and techniques allow to verify timing properties. They are primarily made for real-time systems, and Smala programs are not. Nevertheless, since the control flow of Smala programs can be described as a tree, tree-based techniques for computing WCET could be applied. Moreover, the execution engine is being rewritten to comply with the last version of the operational semantics which is a good level to address latency issues [14].

Relying on the operational semantics, we plan to add into Smala the reification of latency properties. This should allow the programmer to add runtime adaptations (e.g. simplification/enhancement of the visualization to comply with latency constraints) and to optimize the redrawing of the graphical scene.

At last, to limit the known impacts of the operating system on latency, we are experimenting some specific versions of Djnn that can be run on OS-less (’bare’) systems. This approach should result in an autonomous and complete software platform to handle latency.

4 Future Work

To achieve these goals, we aim at allowing the developer of interactive software to handle latency as a whole, during each phases of the software life cycle. Thus, this implies the conception of software tools for the measurement, visualization, specification, and formal checking of the different properties. These tools will make possible, during the design time, the objective evaluation of various software architecture solutions. At last, a methodology for designing interactive systems with latency constraints, based on these tools, should be designed.