Radu Mateescu

Roland Groz

Josip Bozic

Hermann Felbinger

Birgit Hofer

Keywords: testing tools, model GALS systems

I would like to thank my PhD advisors

In the first direction, we explore formal techniques for the functional testing of synchronous components. As a case-study, we reconsider the Message Authenticator Algorithm (MAA), a pioneering cryptographic function designed in the mid-80s, and formalize it as a synchronous dataflow. The modeling and validation of the MAA enabled us to discover various mistakes in prior (informal and formal) specifications of the MAA, the test vectors and code of the ISO 1987 and ISO 1990 standards, and in compilers and verification tools used by us.

In the second direction, we explore the formalization and the functional testing of a communication protocol. As a case-study, we reconsider the formalization of the Transport Layer Security (TLS) handshake, a protocol responsible for the authentication and exchange of keys necessary to establish or resume a secure communication. Our model of the TLS version 1.3 has been validated by an approach using our new on-the-fly conformance test case generation tool, named TESTOR, developed on top of the CADP toolbox. TESTOR explores the model and generates automatically a set of controllable test cases or a complete test graph (CTG) to be executed on a physical implementation of the system.

In the third direction, we propose a testing methodology for GALS systems combining the two previous directions. We leverage the conformance test generation for asynchronous systems to automatically derive realistic scenarios (inputs constraints and oracles), which are necessary ingredients for the unit testing of individual synchronous components, and are difficult and error-prone to design manually. Thus our methodology integrates (1) synchronous and asynchronous concurrent models; (2) functional unit testing and behavioral conformance testing; and (3) various formal methods and their tool equipments. We illustrate our methodology on a simple, but relevant example inspired by autonomous cars.

Résumé

Cette thèse porte sur la génération de tests à partir d'un modèle pour les systèmes GALS (Globalement Asynchrones et Localement Synchrones). La combinaison des aspects synchrones et asynchrones en font des systèmes complexes, imposant de recourir à de nouvelles méthodes d'analyse. Pour faire face à cette complexité, nous explorons trois directions :

(1) techniques pour les composants synchrones ; (2) techniques pour les protocoles de communication entre les composants ; et (3) techniques pour des systèmes GALS complets, combinant les résultats des deux directions précédentes.

Dans la première direction, nous explorons des techniques formelles pour le test fonctionnel de composants synchrones. En tant qu'étude de cas, nous reprenons l'algorithme d'authentification de message (MAA), une fonction cryptographique conçue au milieu des années 80. Nous formalisons cet algorithme en tant que flux de données synchrone. La modélisation et la validation du MAA nous ont permis de découvrir diverses erreurs dans les spécifications (informelles et formelles) préalables du MAA, les vecteurs de test et code des normes [START_REF] Iso | Approved Algorithms for Message Authentication -Part 1: Data Encryption Algorithm (DEA)[END_REF]et ISO 1990 ; dans les compilateurs et outils de vérification que nous avons utilisés.

Dans la seconde direction, nous explorons la formalisation et le test fonctionnel d'un protocole de communication. Dans notre étude de cas, nous évaluons le protocole d'établissement d'une liaison sécurisé au niveau de la couche de transport (TLS), responsable de l'authentification et de l'échange de clés nécessaires pour établir ou reprendre une communication sécurisée. Notre modèle de la version 1.3 TLS a été validé par une approche utilisant notre nouvel outil de génération de cas de test de conformité à la volée, nommé TESTOR, développé à partir de la boîte à outils CADP. Cet outil explore le modèle et génère automatiquement un ensemble de cas de tests ou un graphe de test complet (CTG), à exécuter sur une implémentation physique d'un système.

Dans la troisième direction, nous proposons une méthodologie de test permettant d'analyser les systèmes GALS dans leur ensemble. Nous tirons parti de la génération de tests de conformité des systèmes asynchrones pour dériver automatiquement des scénarios réalistes (contraintes d'entrées et oracles), qui sont ardus à concevoir manuellement et sujet d'erreurs. Ainsi, notre méthodologie intègre (1) modèles concurrents synchrones et asynchrones; (2) les tests unitaires fonctionnels et les tests de conformité comportementale; et (3) diverses méthodes formelles et leurs outils. Nous illustrons notre méthodologie sur un exemple simple, mais représentatif inspiré des voitures autonomes.

Chapter 1 Introduction "On March 18, 2018, in Tempe, Arizona at 10pm, for the first time, an autonomous vehicle, more particularly the Uber SUV, hit and killed a pedestrian. Per that report, the Uber car's radar and LiDAR sensors were able to detect an object in the path of the vehicle (the pedestrian) about six seconds before the crash, but it misclassified her as an unknown object, then a vehicle, then finally a bicycle. At 1.3 seconds before impact, the system tried to initiate an emergency braking maneuver, but Uber had deactivated the vehicle's factoryequipped automated emergency braking system to help ensure less erratic testing." [START_REF]Why uber's self-driving car killed a pedestrian[END_REF] This crash, which killed a pedestrian, is the consequence of an error in the system controlling the car. The LiDAR (Light Detection and Ranging) sensor can detect obstacles perfectly well in the dark, with the same precision as in daylight. However, the sensor is only responsible for the perception of the environment and does not make the decision to brake the car, to slow down or to choose another route: these decisions are up to the decision controller of the vehicle, which has to interpret and use the sensor data to initiate appropriate actions.

The Uber car is an example of a critical system, i.e., a system whose failure or malfunction may result in at least one of the following outcomes: death or serious injury to human, loss or severe damage to equipment, and environmental harm. Nowadays, critical systems can be found in almost any domain, such as infrastructure, medicine, nuclear engineering, transport (railway, aviation, automobile, spaceflight). Because a malfunction of these systems might endanger human life or cause an environmental damage, ensuring correct functioning of critical systems is more important than ever.

Testing is still one of the most common practices to ensure that a system does but only what it was designed to do. Testing enables to identify errors in a system and also any missing requirements in the design of a system. Testing can be done manually or using automated tools. One can distinguish three testing approaches. One can either test the internal structure, design, and coding of the system, which is called white box or glass testing. For instance, the system performing the perception of a LiDAR in an autonomous car could be tested by analyzing its internal code. Otherwise, one can test the behavior, without looking at the internal code structure, implementation details and knowledge of internal system internals, which is called black box testing. For instance, the same system performing the perception of a LiDAR can be tested by just focusing on the inputs and observing the outputs without knowing the internal implementation. White-box testing is difficult to achieve, because in order to test the global system one should access all its internal details, which costs time and memory if it is even feasible at all. On the other hand, black-box testing is sometimes too restrictive, especially when testing security systems, where the principal information is hidden in the internal system. Between black-box and white-box testing, an intermediate testing approach exists, called grey-box testing, where the dynamic behavior of the system is described e.g., using high-level models in terms of states and transitions systems (also called automata). Grey-box testing is based entirely on the requirements and specifications. In this dissertation, we focus on grey-box testing, and more particularly using formal methods for testing [START_REF] Bernot | Software testing based on formal specifications: a theory and a tool[END_REF][START_REF] Gaudel | Testing can be formal[END_REF], as it is required for the validation of critical systems [MLD + 13].

Formal methods are mathematically well-founded techniques designed to assist the development of correct complex systems [START_REF] Garavel | Formal Methods for Safe and Secure Computers Systems[END_REF]. A central idea of formal methods is to consider systems as mathematical objects that can be described and analyzed rigorously. For the description, formal methods are often associated with computer languages having a formal semantics that could either describe the properties expected from a system or the observable behavior of the system. For the analysis, formal methods are often equipped with tools, ensuring that the system will function as expected, under certain assumptions. A formal model can be used to verify and test a system. An important difference between testing with formal methods and traditional testing techniques is the capacity of formal methods to automatically analyze and test a large amount of possible and (by construction) relevant behaviors of the system, and not only a few ones. Relevant behaviors characterize interesting situations, including the ones that the system should do, that the system should not do, and the ones stressing the system. This is essential for critical systems, where the correct functioning of the system has to be mathematically demonstrated, and not only estimated.

Model-Based Testing (MBT) [BJK + 05] is a grey-box testing technique taking advantage of a formal model of a system to automate the generation of relevant test cases. Here, the model represents the expected behavior of the system, in other words, it should contain all possible behaviors of the system. The model can also include a description of the system's environment, so as to precisely describe what the system expects from its environment, i.e., what the environment can do, and what it cannot do. Relevant test cases are then generated from this model, to ensure that the tester examines the system behavior from as many angles as possible. A test case is a set of step-by-step instructions to test if the system behaves as required. A test case usually contains the test steps, the expected result, and the verdict corresponding to the result of the test execution. The MBT technique is particularly suitable for concurrent systems, such as communication protocols [START_REF] Willemse | A case study in formal methods: Specification and validation of the om/rr protocol[END_REF], distributed systems [START_REF] Graf-Brill | A Model-based Certification Framework for the EnergyBus Standard[END_REF], and multiprocessor architectures [START_REF] Garavel | System design of a cc-numa multiprocessor architecture using formal specification, model-checking, cosimulation, and test generation[END_REF]. The model describes the system's requirements, thus the test cases generated are directly linked to these requirements, which allows readability, understandability, and maintainability of the test execution. Model-based testing also helps to ensure a repeatable scientific basis for testing and has the potential to measure the coverage of the system's behavior [START_REF] Utting | The role of model-based testing[END_REF]. Moreover, it is a way to reduce effort and cost and improve the quality of testing [BJK + 05]. In this thesis we focus primarily on model-based testing of a specific kind of critical systems, namely those that contain a reactive controller.

Reactive controllers [START_REF] Berry | Real time programming: Special purpose or general purpose languages[END_REF][START_REF] Halbwachs | Synchronous programming of reactive systems[END_REF] are characterized by the fact that they continuously interact with their environment, by observing it (via input sensors) and modifying it (via output commands) to obtain the desired behavior. A simple example is the control of the room temperature by commanding a heater. The synchronous approach [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] to reactive systems programming supposes that the controller operates triggered by a clock, such that at each clock pulse the system computes the outputs from the current inputs and its internal state before the next clock pulse. Thus, time can be considered as discrete and computation as atomic. There is no need to consider fluctuation and clock synchronization difficulty, such as unpredictable message delay, different speed of components, and physical distance. The conjunction of component actions at the same clock pulse constitutes an action of the whole system. This synchronous approach is mainly supported by synchronous languages, such as Esterel [START_REF] Berry | The esterel synchronous programming language: Design, semantics, implementation[END_REF], Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF], and Signal [START_REF] Benveniste | Synchronous programming with events and relations: the SIGNAL language and its semantics[END_REF]. The simplicity of this abstraction is the reason for the success of the synchronous approach, which has been widely used for over two decades for the design and analysis of safety critical systems in various application domains (e.g., avionics, railway transportation, nuclear plants, etc.). For instance, Lustre, industrialized under the name SCADE [START_REF] Berry | SCADE: Synchronous design and validation of embedded control software[END_REF], serves for the control of nuclear power plants, flight control software and in railway systems. SCADE models can be validated with the synchronous MBT tool GATeL [START_REF] Marre | Test Sequences Generation from LUSTRE Descriptions: GATeL[END_REF].

Critical systems are more and more often distributed, involving several components running independently without a global clock and interacting with each other. For such systems, the strong synchronous assumptions about time and order of events is not realistic anymore, because of the concurrency between independent components of these systems and message-passing communication. The asynchronous approaches [START_REF] Goltz | CSP-Programs with Individual Tokens[END_REF][START_REF] Goltz | On Representing CCS Programs by Finite Petri Nets[END_REF][START_REF] Guillemot | Derivation of useful execution trees from lotos specifications by using an interpreter[END_REF] are more appropriate for describing these systems, the concurrency between components being reduced to a nondeterministic choice between the possible sequences of the component actions, and these approaches are able to capture the nondeterminism induced by unknown message transmission delays. This model of concurrency is mainly supported by process algebras, such as CCS [START_REF] Milner | Communication and Concurrency[END_REF], CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], ACP [START_REF] Bergstra | Algebra of communicating processes with abstractions[END_REF], and LNT [START_REF] Garavel | From LOTOS to LNT[END_REF]. Particularly suited for nondeterministic concurrent systems, conformance testing aims at extracting from a formal model of a system a set of test cases to assess whether an actual implementation of the system under test conforms to the model. In this setting, the most prominent conformance relation is input-output conformance (ioco) [START_REF] René | Towards formal test purposes[END_REF][START_REF] Tretmans | Model Based Testing with Labelled Transition Systems[END_REF].

Nowadays, modern asynchronous systems, such as autonomous cars or the Internet of Things, are not only increasingly large and distributed, but also consisting of multi-ple synchronous components that execute independently and interact with each other. These systems are adequately described as GALS (Globally Asynchronous, Locally Synchronous) [START_REF] Daniel | Globally-Asynchronous Locally-Synchronous Systems[END_REF], i.e., composed of concurrent synchronous reactive systems interacting with each other asynchronously, by means of message passing with non-zero communication delays. For instance, in an autonomous car, the perception devices (radar, GPS, cameras, etc.) and the engine controls (decision-maker) are separate components, located in various places of the car, operating independently and connected through communication links. Each of these components might be considered and implemented as a synchronous reactive system, but the complete autonomous car is rather a GALS system.

The GALS approach allows the smooth integration and reuse of existing and time-proven synchronous components when designing new systems that no longer fit into the framework of synchronous programming. Rigorous design approaches, based on formal methods and assisted by efficient validation and verification tools exist for the separate modeling and analysis of synchronous or asynchronous parts of a GALS system, but their combination can further improve the effective support in the design of a complete GALS system. In this thesis we consider three aspects of MBT for GALS systems: synchronous, asynchronous, and their combination.

Contributions

In this thesis we bring two main contributions.

First, we propose a new on-the-fly MBT tool called TESTOR, which explores the model and generates automatically a set of controllable test cases or a complete test graph to be executed on a physical implementation of the system. The generated test cases are automata that attempt to drive a system under test towards these desired states. TESTOR extends the algorithms of the conformance test generation tool TGV [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF] to extract test cases completely on the fly (i.e., during test case execution against the system under test), making TESTOR suitable for online testing. Concretely, given a formal specification of a system and a test purpose, TESTOR automatically generates test cases, which assess using black box testing techniques the conformance to the specification of a system under test. In this context, a test purpose describes the goal states to be reached by the test and enables one to indicate parts of the specification that should be ignored during the testing process. Compared to the conformance test generation tool TGV, TESTOR has a more modular architecture, based on generic graph transformation components, is capable of extracting a controllable test case completely on the fly, and enables a more flexible expression of test purposes, taking advantage of the multiway rendezvous of LNT.

Then, we propose a testing methodology for GALS systems that integrates (1) synchronous and asynchronous concurrent models; (2) functional unit testing and behavioral conformance testing; and (3) various formal methods and their tool equipments. an overview of our GALS testing approach, combining the existing synchronous testing tool Lurette presented in Chapter 2 and used in Chapter 3 and our new on-the-fly conformance test case generation tool TESTOR described in Chapter 4. The idea is to exploit the information gathered by the analysis of a globally asynchronous system to automate and finely tune the testing of its individual synchronous components. We illustrate our approach on a simple, but relevant example, namely an autonomous car, which has to reach a destination, following roads on a map, in the presence of moving obstacles. The car is modeled as a GALS system, comprising synchronous components for perception, decision, and action. As far as we know, this is the first approach of model-based testing for GALS systems.

Structure of this thesis

This dissertation focuses on the MBT of GALS systems, taking into account synchronous and asynchronous aspects. Chapter 2 briefly presents the scientific background necessary for the subsequent chapters and also places our work with respect to the state of the art.

Chapter 3 explores formal techniques for the functional testing of synchronous components, using the testing tool Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF] for synchronous programs. As a case-study, we reconsider the Message Authenticator Algorithm (MAA), a pioneering cryptographic function designed and standardized by ISO in the mid-80s. Formally modeling and validating the MAA as a synchronous dataflow enabled us to discover various mistakes in prior (informal and formal) specifications of the MAA, the test vectors and code of the ISO standards, and in some of the compilers and verification tools used by us.

Chapter 4 describes the formalization and the functional testing of a communication protocol and presents our new on-the-fly conformance test case generation tool, named TESTOR [START_REF] Marsso | TESTOR: A modular tool for on-the-fly conformance test case generation[END_REF], developed on top of the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. As a case-study, we reconsider the formalization of the draft Transport Layer Security (TLS) handshake version 1.3 [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF], a protocol responsible for the authentication and exchange of keys necessary to establish or resume a secure communication. Our TLS model has been vali-dated using TESTOR.

In Chapter 5, we leverage the conformance test generation for asynchronous systems to automatically derive realistic scenarios (input constraints and oracles), which are necessary ingredients for the unit testing of individual synchronous components, and are difficult and error-prone to design manually. We illustrate our approach on a simple, but relevant example of an autonomous car modeled as a GALS system.

Finally, Chapter 6 concludes by summarizing our main contributions and discussing directions for future work.

Chapter 2 Formal Modelling and Validation of GALS Systems

This chapter presents first some preliminary notions that we use in the rest of this thesis. It also defines the perimeter of this thesis by listing aspects considered to be out of scope, together with the reasons justifying this choice.

The rest if this chapter is structured in three parts, corresponding to the different techniques required for the analysis of GALS systems: (1) techniques for synchronous components; (2) techniques for the asynchronous communication; and (3) techniques for complete GALS systems. For each part we present tools, languages, and an overview of the ones we used. A reader familiar with our languages and tools can safely skip the overviews.

Preliminaries

In order to describe formally the behavior of discrete and concurrent systems, one may use Labelled Transition Systems (LTS). In this section we define informally and formally LTS, and we describe three approaches to validate them, namely equivalence checking, model checking, and testing.

Labelled Transition Systems (LTS)

An LTS is a state-transition graph, in which the states do not provide information except for the indication of the initial state. The information is represented in the labels (or actions) related to transitions. Formally, an LTS (Q, A, T, q 0 ) consists of a finite set of states Q, a set of actions A, a transition relation T ⊆ Q × A × Q, and an initial state q 0 ∈ Q. A transition (q 1 , a, q 2 ) ∈ T (also noted q 1 a → q 2 ) indicates that the system can move from coffee coin tea τ τ q0 q2 q1 q3

Figure 2.1: The LTS corresponding to a simple coffee/tea vending machine state q 1 to state q 2 by performing action a. Internal transitions, i.e., transitions whose label is not visible, are labeled by the action τ . An LTS is said nondeterministic if there is more than one initial state or if it exists a state q ∈ Q and an action a ∈ A, where more than one state can be reached from q by performing the same action a. An example LTS is shown in Figure 2.1, modelling the simple behavior of a coffee vending machine. The set of states of this LTS is Q = {q 0 , q 1 , q 2 , q 3 }. The set of actions is A = {coin, coffee, tea,τ }. The initial state is q 0 . An LTS can be represented explicitly, such as the textual AUTomaton (AUT) format [FGK + 96] and the Binary Coded Graph (BCG) format [START_REF] Garavel | Binary coded graphs: Definition of the bcg format[END_REF]; or implicitly, by providing the post function iterating over the outgoing transitions of a given state, for instance using the Open/Caesar API [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF].

The LTS model of a system represents exhaustively its behavior, which can be described intuitively as follows. The LTS starts with its initial state. From this initial state, the LTS evolves according to its transition relation. Very often, more than one transition will be possible from a given state. In that case, a transition is selected non-deterministically. Coming back to Figure 2.1, from the initial state (q 0 ), only one transition is possible. So, the LTS of the vending machine will always perform a coin action first and reach q 1 . In q 1 , there are two internal steps (τ ). The LTS system will non-deterministically choose one of them and then either perform a coffee or a tea action.

Individual execution sequences in an LTS are called traces. A trace of size n ∈ N is a sequence of actions a 1 , a 2 , . . . , a n ∈ A such that q 0 a 1 -→ q 1 ∈ T, q 1 a 2 -→ q 2 ∈ T, . . . , q n-1 an -→ q n ∈ T . A trace starts always with the initial state (q 0 ). A trace is potentially infinite, due to the presence of cycles in the LTS. The traces of the LTS in Figure 2.1 consist of (infinite) repetitions of one or both of the following cycles:

i) q 0 coin --→ q 1 τ - -→ q 2 tea --→ q 0 ii) q 0 coin --→ q 1 τ - -→ q 3 coffee ---→ q 0
In this thesis, we also use a particular kind of LTS with the distinction between input and output actions (LTS (A i ∪ A o )), called Input-Output Labelled Transition Systems (IOLTS) [START_REF] Tretmans | Testing Concurrent Systems: A Formal Approach[END_REF]. An IOLTS is an LTS (Q, A, T, q 0 ) where the set of actions is partitioned in A = A I ∪ A O ∪ {τ }, where A I , A O are the subsets of input and output actions, and τ is the internal (unobservable) action. Input (resp. output) actions are noted ?a (resp. ). An example of IOLTS is illustrated in black in Figure 2.2, modelling the behavior of a vending coffee machine. The machine receives coins, represented as input (?coin) and delivers beverages, represented as outputs (!tea and !coffee) in the LTS. In order to avoid any bias in the observation of the input actions of an IOLTS, the IOLTS can be input enabled. This particular kind of IOLTS, with the property that any input action is always enabled in any state, is called IOTS [START_REF] Tretmans | Testing Concurrent Systems: A Formal Approach[END_REF]. An example of IOTS is illustrated in Figure 2.2 with the additional input transitions in green.

Equivalence checking

Equivalence checking is a verification method consisting in comparing two LTSs modulo an equivalence relation. There exist several equivalence relations in the literature, such as strong equivalence, branching equivalence [START_REF] Van Glabbeek | Branching-Time and Abstraction in Bisimulation Semantics[END_REF], trace equivalence [START_REF] Fernandez | On the Fly" Verification of Behavioural Equivalences and Preorders[END_REF], weak trace equivalence [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF], etc. We focus on two of them, namely the branching equivalence and the weak trace equivalence.

Two LTS M = (Q, A, T, q 0 ) and M = (Q , A , T , q 0 ) are equivalent according to an equivalence relation ∼ (written M ∼ M ), if and only if their initial states are equivalent modulo ∼ (written q 0 ∼ q 0 ).

Branching equivalence Two states p and q are branching equivalent (called p ∼ bra q), if and only if, it exists a relation R bra such that pR bra q and:

1. for each transition p a --→ p ∈ T

• either a = τ and p R bra q

• or it exists a sequence q τ * --→ q a --→ q ∈ T * such as pR bra q and p R bra q 2. for each transition q a --→ q ∈ T

• either a = τ and pR bra q

• or it exists a sequence p τ * --→ p a --→ p ∈ T * such as p R bra q and p R bra q

Weak trace equivalence Two states p and q are weak trace equivalent (called p ∼ wtr q), if and only if:

1. for all n ≥ 0 and all sequences p τ * .a 1 ...τ * .an -------→ p ∈ T * , there exists a sequence q τ * .a 1 ...τ * .an -------→ q ∈ T * 2. for all n ≥ 0 and all sequences q τ * .a 1 ...τ * .an -------→ q ∈ T * , there exists a sequence p τ * .a 1 ...τ * .an

-------→ p ∈ T *
The CADP (Construction and Analysis of Distributed Processes) verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] provides the tools BISIMULATOR [START_REF] Bergamini | Bisimulator: A modular tool for on-the-fly equivalence checking[END_REF][START_REF] Mateescu | Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems[END_REF] and BCG CMP [START_REF] Vasy | Bcg cmp manual page[END_REF] to compare LTSs, the tool REDUCTOR [START_REF] Vasy | Reductor manual page[END_REF] to reduce LTSs according to the strong or weak trace equivalence, and the tool BCG MIN [BHH + 06] to minimize LTSs according to strong or branching equivalence.

Model checking

Model checking [START_REF] Clarke | Model checking[END_REF] is a verification method establishing that a model of a system (respectively, component) satisfies a property. A property defines how the system should be designed and which features it should provide. Informally, model checking produces a Boolean answer to the question: Does a given system satisfy a property ? Most model checking approaches add a diagnostic that answers to the question: Where is this property not satisfied by this system ? Concretely, model checking defines a satisfaction relation between a system (respectively, component) and a property as a mathematical binary relation that is true if and only if the property holds for the system, i.e., if the system correctly implements the property. The system is described by a finite state model (e.g., an LTS) and a property is expressed in temporal logic.

Examples of properties are simple assertions, stating that a predicate on system variables holds whenever the execution reaches a particular control location (e.g., the transition coffee is reachable whenever a coin with the value 20 was inserted), or termination properties (e.g., "the vending machine system terminates on a coffee or tea transition"). Principally, properties are classified as liveness, fairness and safety. A liveness property expresses that something good eventually happens, e.g., all transition sequences starting after an action coin eventually lead to an action tea or coffee. A fairness property expresses that, under certain conditions, something should always happen, e.g., after an action coin, all fair execution sequences (which avoid the infinite repetition of cycles) will lead to an action tea or coffee. A safety property expresses that something bad never happens, e.g., if the action coin happens, then while there is no action tea or coffee, no other action coin may happen.

Numerous model checkers exist for synchronous and asynchronous systems, verifying in the supported modeling formalism and property languages (stochastic, probabilistic, timed, etc.) including (in alphabetical order): CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], CPAchecker [START_REF] Beyer | Cpachecker: A tool for configurable software verification[END_REF], Cubi-cle [CGK + 12], DREAM [START_REF] Proenca | Dreams: A Framework for Distributed Synchronous Coordination[END_REF], FDR [START_REF] Gibson-Robinson | FDR3 -A Modern Refinement Checker for CSP[END_REF], Java Pathfinder [VHBP00], KIND 2 [START_REF] Champion | The kind 2 model checker[END_REF], LESAR [SSC + 04], mCRL2 [CGK + 13], NuSMV [START_REF] Kadono | Using the nusmv model checker for test generation from statecharts[END_REF], Prism [START_REF] Hinton | Prism: A tool for automatic verification of probabilistic systems[END_REF], SAL 2 [dMOR + 04], SLAM [START_REF] Ball | The SLAM toolkit[END_REF], SPIN [START_REF] Holzmann | State compression in spin: Recursive indexing and compression training runs[END_REF], TLA+ [START_REF] Lamport | The temporal logic of actions[END_REF], UPPAAL [BLL + 95], XEVE [START_REF] Bouali | Xeve, an ESTEREL verification environment[END_REF], and Zing [AQR + 04].

Testing and coverage criteria

Exhaustive testing is infeasible in practice, because the systems are complex and their corresponding LTSs are large, the space of possible test cases being generally too big to cover exhaustively in a reasonable time. Thus, strategies are required to decide when to stop testing. Coverage criteria serve to decide when to stop testing, by measuring the amount of the system already tested. More particularly, a coverage criterion is a measure used to describe the degree to which the internal structure of a system has been exercised when a particular a set of test cases, called a test suite, runs. Coverage criteria could also guide automatic test generation, otherwise the test generation is simply random. One can distinguish two complementary coverage methodologies. Functional coverage tries to measure how scrupulously a system under test is tested against its informal specification, e.g., system requirements. Functional coverage is helpful to reveal functionality defects. Structural coverage tries to quantify how much the internal structure of a system under test is exercised during its test process. Structural coverage is helpful for detecting unused fragments of the system, as well as highlighting the fragments that have not been properly exercised.

In this section, we focus on a particular structural coverage for model based testing, called model coverage [START_REF] Utting | A taxonomy of model-based testing approaches[END_REF]. Model coverage quantifies how much of the internal structure of the model (e.g., a LTS) is explored and unexplored during the test process. Five coverage criteria defined with respect to an LTS for the model coverage of a concurrent system are proposed in [START_REF] Taylor | Structural testing of concurrent programs[END_REF]:

1. all labels criterion, which covers all labels of the LTS at least once, a same label may occur on several transitions in the LTS;

2. all states criterion, which covers all states of the LTS at least once;

3. all transitions criterion, which covers at least once all transitions in the LTS;

4. all proper paths criterion, which covers all finite trace in the LTS without any identical states;

5. and all paths criterion, which covers all paths of the LTS at least once, which is impossible to achieve in finite time if the LTS contains cycles.

A specific model coverage, called dataflow coverage criteria [START_REF] Frankl | An applicable family of data flow testing criteria[END_REF][START_REF] Lakehal | Critères de couverture structurelle pour les programmes Lustre[END_REF], can be applied to any modelling notation that contains variables. For instance, the academic tool Lustructu [START_REF] Lakehal | Critères de couverture structurelle pour les programmes Lustre[END_REF][START_REF] Lakehal | Lustructu: A tool for the automatic coverage assessment of lustre programs[END_REF] includes these criteria for the synchronous dataflow language Lustre.

One can also directly specify custom criteria in the model test coverage module of the SCADE environment [START_REF] Berry | SCADE: Synchronous design and validation of embedded control software[END_REF].

For large systems, it is not realistic to describe explicitly the LTS of the system. Such large LTSs are described using higher level formalism, and in the next sections we present synchronous, asynchronous, and GALS specific higher level formalisms.

Synchronous Models and their Validation

The synchronous paradigm [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] for developing reactive systems is based on the synchronous hypothesis: the time is discrete, and the inputs of the system are only changed at a clock tick. Thus, defining the outputs of the system by equation on the inputs and the current state is sound if the outputs are computed faster than the sampling rate. Synchronous models enable to describe, simulate and verify reactive systems and to compile the code or the hardware ensuring the same behavior described in the model, if the synchronous hypothesis is verified. Synchronous programs have a cyclic behavior: at each cycle, all inputs are read, processed and all outputs are transmitted simultaneously and theoretically instantly. In the state of the art, one can principally distinguish two synchronous paradigms of programming:

• The synchronous dataflow languages as Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF]. The dataflow model is based on a block diagram description. A block diagram can be described by a system of equations. A system is made up of a network of operators acting in parallel and at a pre-established pace.

• The control oriented languages as Esterel [START_REF] Berry | The esterel synchronous programming language: Design, semantics, implementation[END_REF][START_REF] Potop-Butucaru | Compiling Esterel[END_REF]. This programming paradigm is particularly suited to the description of systems whose behavior changes frequently and depending on the data.

In this thesis we will use the synchronous data flow language Lustre taking advantage of its connection to robust testing tools, actively supported and maintained by developers. Moreover, Lustre is at the basis of industrial environments, such as SCADE [START_REF] Berry | SCADE: Synchronous design and validation of embedded control software[END_REF].

Overview of the Lustre language

In this section we give an overview of the Lustre language, readers familiar with Lustre can safely skip this section. Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF] is a synchronous language based on the dataflow model. At each cycle, the value of the previous inputs can be memorized. The outputs of a program at a given instant may depend on these memorized inputs, but not on future inputs.

The relations between inputs and outputs are expressed using constants, operators, auxiliary variables, and functions. Lustre provides some predefined types, i.e., Boolean (bool), integer numbers (int), real numbers (real), and strings (string). For example, the following Lustre constant average_temperature is defined as the integer 20, and could be used to specify the desired average temperature in a room for a heater.

( * temperature in Celsius * ) const average_temperature:int = 20;

The user can also define record, array and enumeration types. For example, the following Lustre enumeration seasons corresponds to the four seasons:

type seasons = enum {Winter, Spring, Summer, Autumn};

In addition to built-in operators for the predefined types, and all classical arithmetic and logic operators, Lustre enables to define functions. For example, the following Lustre function season_to_temperature associates a temperature to be set by the heater for each season. Lustre offers also the possibility to define new, complex operators, called nodes. Each description written in Lustre is built up of a network of nodes. A node describes the relation between its input and output parameters using a system of equations. A node has a set of unordered equations that define each of the output parameters according to the actual or previous input parameters. Being a data flow language, Lustre handles infinite sequences of values, called streams.

In addition, Lustre has two specific flow manipulation operators for the nodes:

• the memory operator pre ("previous") refers to the value of an input or output variable at the previous cycle;

• the initialization operator -> ("followed by") initializes a stream.

The code below represents a Lustre node corresponding to a simple synchronous heater. The heater increases gradually the temperature (new_room_temperature), taking into account the previous temperature (pre new_room_temperature) and the expected temperature of a room (the variable expected_temperature). The input actual_room_temperature, denoting the actual temperature of the environment (the room), is only used to initialize the value of the room temperature. The input

Synchronous system validation

In this section, we present tools enabling the validation of reactive systems, more particularly model checking and testing tools.

Synchronous models can be verified by using model checking. One can distinguish two kinds of synchronous model checkers. Symbolic model checkers use logical representations of sets of states, such as Binary Decision Diagrams (BDD) to describe regions of the state space that satisfy the properties being evaluated such as: LESAR [SSC + 04], NuSMV [START_REF] Kadono | Using the nusmv model checker for test generation from statecharts[END_REF], SLAM [START_REF] Ball | The SLAM toolkit[END_REF] and XEVE [START_REF] Bouali | Xeve, an ESTEREL verification environment[END_REF]. Model checkers based on satisfiability modulo theories (SMT) solvers reason about infinite state models containing real numbers and unbounded arrays, such as: KIND 2 [CMST16], Cubicle [CGK + 12], and SAL 2 [dMOR + 04]. In this thesis, we did not use synchronous verification to validate synchronous components, but we used synchronous test generation tools.

Model based testing of synchronous models includes automating test data generation. Automating the test data generation consists in generating inputs for testing a synchronous system. Often the inputs are generated from a model and a description of constraints on the inputs of this model. The generation could also be guided by a scenario, in order to generate relevant tests. The test generation can use a white box approach, such as Gatel [START_REF] Marre | Test Sequences Generation from LUSTRE Descriptions: GATeL[END_REF], or black box approach, such as Lutess v1 [START_REF] Du Bousquet | Lutess: A Specification-Driven Testing Environment for Synchronous Software[END_REF], Lutess v2 [START_REF] Seljimi | Automatic generation of test data generators for synchronous programs: Lutess V2[END_REF], Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF], and Testium [MDP14, MDP + 16]. In this thesis, we focus on automating the test data generation for testing the synchronous components of a GALS system. In this thesis, we use the black box testing tool Lurette for validating synchronous components, taking advantage of its connection with the Lustre language.

Overview of the Lurette testing tool

In this section we give an overview of the testing tool Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF], readers familiar with it can safely skip this section. Using formal specifications of the input constraints and an oracle, Lurette automates both, the generation of appropriate inputs for the SUT (system under test) and the decision about the test result. (i) a specification of the environment constraints in Lutin [START_REF] Raymond | Lutin: a language for specifying and executing reactive scenarios[END_REF] to dynamically constrain the inputs;

(ii) an oracle in Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF] implementing the test decision and the coveragecomputation of the generated and executed input sequences, and the coverage criteria to evaluate these input sequences generated.

Lurette interacts with the SUT, logs the generated sequence of inputs and their corresponding outputs in a file, and displays the test decisions. The admissible test inputs are generally provided by a formal specification of the system environment. The correct corresponding/respective outputs to an input vector are generally provided as formal properties of the system.

Lutin input constraints

The test sequence is generated uniformly and randomly by Lurette. Lurette builds and submits to the SUT an input vector respecting the input constraints description. Then the tool calculates a new input vector for SUT, based on the current state of the input constraints and the last output of the SUT.

Lutin is a language to program stochastic reactive systems. It has been designed to model input constraints and perform automated testing of reactive systems with Lurette. Lutin supports the numerical and Boolean types of Lustre, as well as all Lustre statements, such as variable assignment, conditional (if-then-else), previous (pre) and initialization operators (->). In addition, Lutin has three specific operators: sequence (fby, for "followed by"), Kleene star (loop), and probabilistic choice (|). Consider for example the following Lutin node corresponding to the simple scenario defined by the automaton1 in Figure 2.4, where the input values actual_room_temperature and season of the node heater (see Section 2.2.1) can possibly take 18 and Winter respectively, or 26 and Spring, etc. Note that the first actual_room_temperature input is only taken into account in the first activation of the heater, then for the next iterations only the season input values are taken into account. Because Lutin does not provide structured datatypes, we have to add four constants for the four seasons. Each input can only be a Boolean, or a numerical type (integer, real), mostly because of the data types provided by the Lutin language. Note that if the input values are not explicitly constrained in the Lutin specification, random numbers will be generated.

Lustre oracle

In order to determine whether the outputs generated by the SUT are correct or not, one should define an oracle. An oracle should contain all possible pairs of inputs with the corresponding expected outputs, and signal an error for each unexpected output. In addition to checking correctness, Lurette supports additional Boolean outputs (called coverage variables) to measure coverage. While testing the SUT, Lurette records the coverage variables that were at least once true, and computes the ratio of covered versus uncovered variables. The list of coverage variables with their status is stored in a file, and is updated by any subsequent run of Lurette for the same SUT, input constraints, and oracle.

For instance, the temperature of the heater (new_room_temperature) can only increase, and only if the previous room temperature (pre new_room_temperature) is lower than the expected temperature (expected_temperature), defined for each season. Because the heater takes into account only the first actual room temperature (actual_room_temperature), the possible values of the heater (new_room_temperature) depend on the value of the first actual room temperature and on the next room temperature (new_room_temperature). Consider for example all possible combinations of the input value (season) and the output value (new_room_temperature) of the node heater: if we start with an actual temperature ini-tialized with 20 in the automaton2 illustrated in Figure 2.5, then according to the season, all possible temperatures of the heater can be explored. The oracle should take into account all these possible values, and also for all other possible initializations. The following Lustre code corresponds to an excerpt of the oracle from the automaton illustrated in Figure 2.5. As the Lutin node input_constraints, the oracle takes the inputs and outputs of the heater (season, temperature) as input and gives as outputs the verdict res, i.e., whether the observed outputs are those expected from the inputs. For instance, if the first actual_room_temperature is 20, the temperature can only increase until 22, according to the seasons and the previous temperature of the heater. The following oracle also computes a coverage variable cover_seasons, measuring the coverage of all seasons at least once by the generated input vectors. For a more detailed presentation of Lurette see [START_REF] Jahier | Case studies with Lurette V2[END_REF]. In the next section, we describe asynchronous model and validation for the asynchronous communication between synchronous components.

Asynchronous Models and their Validation

Process calculi [START_REF] Aceto | Structural operational semantics[END_REF] provide a formal means for the high-level description of interactions, communications, and synchronizations between a set of independent components of a concurrent system. They also provide rules to describe, manipulate, and analyze processes. The interactions between independent processes are represented by message-passing on communication gates (not modification of shared variables). Interleaving semantics is used for the compositions of processes, i.e., if two processes P 1 and P 2 execute respectively an action a 1 and a 2 in parallel, then the global behavior, represented by an LTS, will have two possible paths: a 1 then a 2 and a 2 then a 1 . In the asynchronous semantics two actions never occur at the same time.

The ideas behind process algebra have been implemented in several languages including: CCS [START_REF] Milner | Communication and Concurrency[END_REF], CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], ACP [START_REF] Bergstra | Algebra of communicating processes with abstractions[END_REF], LOTOS [START_REF] Bolognesi | Introduction to the ISO Specification Language LOTOS[END_REF], mCRL2 [GMR + 06], and LNT [CCG + 19]; and tools including: CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], Concurrency Workbench [START_REF] Cleaveland | The Concurrency Workbench[END_REF][START_REF] Cleaveland | The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems[END_REF], FDR [START_REF] Gibson-Robinson | FDR3 -A Modern Refinement Checker for CSP[END_REF], and mCRL2 [CGK + 13].

In this thesis, we use LNT as specification language for obtaining LTSs models, mostly because LNT is concise, expressive, easily readable, and user-friendly. Also LNT is the recommended specification language of the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], which provides several useful validation tools.

Overview of the LNT language

LNT is an improved version of formal specification language LOTOS [START_REF] Bolognesi | Introduction to the ISO Specification Language LOTOS[END_REF], providing more user-friendly notations than LOTOS, which combines traits from process calculi, functional languages, and imperative languages. In order to let the reader understand the LNT excerpts presented in Chapters 4 and 5, we present here a short introduction to the LNT language. The reader familiar with LNT can safely skip this section.

LNT allows the definition of data types, functions, and processes.

LNT provides some predefined types, i.e., Boolean (bool), natural numbers (nat), integer numbers (int), real numbers (real), characters (char) and strings (string). The user can also declare abstract data types, through the use of the type keyword. For instance, we define the enumeration type drink, corresponding to the different types of drinks of a vending machine: The predefined functions get and set enable to access and respectively modify one field of the record type price. For instance, the following LNT instructions of the ristretto price illustrate two different ways to access and modify a field of this type: ristretto := price (coffee, 20); --get the cost of the ristretto get_cost (ristretto); ristretto.cost; --modify the cost of the ristretto set_cost (ristretto, 25); ristretto.{cost => 2} Note that comments in LNT can be single line comments, in the form --comment, or several lines, in the form ( * comment * ).

LNT provides syntactic sugar to define types corresponding to the list, sorted list, set, or array of another type. We can for instance have the following LNT list type coin, corresponding to all possible coin values (from 5 cents to 2 euros), and the type coins corresponding to a list of coins: The case operator allows pattern matching to be performed on values of any type. As part of the pattern matching, the keyword any matches any value. The following function returns the change if the cash passed as an argument is bigger than the price of the drink, all coins of the cash are matched in order to compute the sum: Note that LNT pattern matching should be exhaustive; the existence of a formal semantics is guaranteed by static semantic constraints [START_REF] Garavel | Revisiting Sequential Composition in Process Calculi[END_REF] ensuring that all possible cases are taken into account in the pattern matching.

A process executes actions. An action is either internal or a rendezvous synchronization on a gate. The internal action in LNT is designated by i. External actions, i.e., realized on a gate, are the observable events of the execution of a process. The formal semantics of LNT defines how, from the specification of a process, one can build the LTS that represents the possible behaviors of this process. An action on a gate is defined by the identifier of the gate, possibly followed by a list of offers in parentheses. A gate is used to handle input/output communications and synchronizations. Offers allow to exchange data on a gate, and they can be an emission of an expression prefixed by an optional !, or the reception of a value prefixed by ?. Here is for example a behavior that performs an internal action, followed by an action on the gate cup where the first offer denotes the sending of a coin, and the second one the receiving a drink. Gates can be untyped (any) or typed by a channel. The channel defines the gate profiles, i.e., the possible offer combinations accepted by the gate. A channel is defined using the channel keyword and must state one or more profiles, which are lists of parameters that declare the number and types of authorized offers. Note that two gates are compatible only if they have the same type, or they are both untyped (any). The channel none is predefined and allows any profile offers. For instance, the following LNT channels define one offer with the drink type and one offer with two possible types, respectively.

--one offer with the drink type is allowed channel single is (drink) end channel --several profiles allowed channel change is (coins), (token) end channel

Processes in LNT are defined with the process keyword. A process receives as argument a list of gates on which it can perform actions. Every gate corresponds to a channel. In order to make explicit the gates available for communication and synchronization between processes, each processes has a list of gates parameters (between square brackets). Similar to a function, a process can also receive a list of values as arguments (between parentheses). Statements presented for functions also apply to processes. A process terminates by executing implicitly the special action exit.

A process can make nondeterministic choices between multiple actions using the select operator. This operator allows to introduce several possible behaviors, which are delimited by []. For instance, the following LNT process vending_machine and its corresponding LTS make a nondeterministic choice between the action on the gate cup (coffee) and the one on the gate cup (tea). Once it has realized an action of a branch of this non-deterministic choice, it is forced to perform the rest of this branch. Note that this corresponds to a state in the LTS with multiple outgoing transitions, where each transition corresponds to one of the choices in a select construct.

Another construction can also perform nondeterminism in an expression. The keyword any assigns any value of a type, possibly with a restriction introduced by the clause where. For example, the following LNT process (and its corresponding LTS) can cyclically perform an action on the gate cup passing a random type of drink different from water: The parallel composition operator can be used to handle communication between differ-ent processes. Concretely, the parallel composing operator par is used to declare multiple processes that run independently, in parallel, while specifying on which gates the processes must synchronize their actions. Two or more processes synchronize and exchange information during a rendezvous. A rendezvous involving an arbitrary number superior to two processes is called multiway rendezvous. One can distinguish three kinds of treatments on actions during a parallel composition. The actions on the gates for which no synchronization is imposed are performed independently by each process. The termination action (exit) is always synchronized between all processes in a parallel composition. Only actions which are offered by every process in the parallel composition can be synchronized. The following example shows the parallel composition of the tea_m and coffee_m processes, which must synchronize their actions on gates coins, sugar, milk and honey:

- The first action on gate coins is common to both processes. Then the actions on gates coffee and tea do not have to be synchronized, so they can be realized in any order. Actions on gates sugar, milk, and honey must be synchronized. When the process coffee_m is ready for an action on the gate sugar or the gate milk, and the process tea_m is ready for action on gate sugar or gate honey, so the only action that is possible for both processes is the one on the sugar gate. Finally, the two processes synchronize their exit action.

Last, but not least, the disruption operator is also provided by LNT. The disrupt behavior starts a behavior, however at any moment, this behavior can be interrupted by another one. For instance, the following LNT disrupt behavior starts with the correct behavior of the vending_machine (coins, etc.), which executes normally. However, at any moment, the correct behavior can be interrupted, in which case the execution of the unexpected behavior (an electrical failure) starts and the correct behavior is disrupted. Note, if the correct behavior successfully terminates before any action has taken place in the unexpected behavior, the disrupt behavior terminates, meaning that the possibility to be interrupted by an electrical failure disappears.

For a more detailed presentation of LNT see [CCG + 19, GLS17].

Verification of asynchronous systems

In this section, we present model checking tools enabling the verification of asynchronous systems, more particularly the property specification languages of the model checker used in this thesis. Numerous model checkers exist for asynchronous systems, including: CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], CPAchecker [START_REF] Beyer | Cpachecker: A tool for configurable software verification[END_REF], DREAM [START_REF] Proenca | Dreams: A Framework for Distributed Synchronous Coordination[END_REF], FDR [START_REF] Gibson-Robinson | FDR3 -A Modern Refinement Checker for CSP[END_REF], Java Pathfinder [START_REF] Visser | Model checking programs[END_REF], mCRL2 [CGK + 13], Prism [START_REF] Hinton | Prism: A tool for automatic verification of probabilistic systems[END_REF], SPIN [START_REF] Holzmann | State compression in spin: Recursive indexing and compression training runs[END_REF], TLA+ [START_REF] Lamport | The temporal logic of actions[END_REF], and UPPAAL [BLL + 95].

In this thesis we will use the EVALUATOR 4.0 [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] model checker of CADP. EVAL-UATOR 4.0 can verify temporal logic properties on the fly on an LTS, and exhibits full diagnostics (portions of the LTS) illustrating the truth value of temporal logic formulas. The temporal logic formulas are written in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF]. We also used the executable temporal Logic tool called XTL [START_REF] Mateescu | XTL: A Meta-Language and Tool for Temporal Logic Model-Checking[END_REF] of the CADP toolbox. We included the MCL formulas and the XTL calls in an SVL (Script Verification Language) [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] script, in order to automate the model verification and test generation method presented in Chapter 5. This script avoids the need to explicitly name certain CADP tools, as SVL is responsible for invoking the appropriate tools to conduct the required verifications. The SVL tool executes verification scenarios expressed in the scripting language SVL. CADP tools are traditionally called from the command line, and each tool has several options. The SVL language makes it easy to describe verification scenarios which involve several CADP tools. In addition, it is possible to insert any UNIX shell command within an SVL scenario, which facilitates the automation of formal verifications.

Overview of the MCL language

In this section we give an overview of the MCL language, readers familiar with MCL can safely skip this section. MCL (Model Checking Language) [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] is an action-based, branching-time temporal logic suitable for expressing properties of concurrent systems, including properties parameterized by data values. MCL is interpreted on Labelled Transition Systems (LTSs).

MCL language extends the temporal property specification formalism µ-calculus [START_REF] Kozen | Results on the propositional mu-calculus[END_REF], with regular expressions over transition sequences similar to those of PDL [START_REF] Michael | Propositional dynamic logic of regular programs[END_REF], datahandling constructs inspired from functional programming languages (quantified variables and fixed point parameters), and a generalization of the infinite looping operator of PDL-∆ [START_REF] Streett | Propositional dynamic logic of looping and converse is elementarily decidable[END_REF] specifying fairness. MCL allows a concise and readable formulation of temporal properties, notably when these properties are parameterized by data values.

We give below the MCL formulation of the four temporal properties defined in Section 2.1.3 and one additional MCL properties, in order to illustrate the MCL predicates used in this thesis.

a) The following MCL formula encodes a liveness property expressing the existence of a sequence leading to an action, e.g., one can potentially get a TEA after inserting a COIN in the vending machine: For a more detailed presentation of MCL see [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF].

<

Overview of the XTL language

In this section we give an overview of the XTL language, readers familiar with XTL can safely skip this section.

The XTL (eXecutable Temporal Logic) tool [START_REF] Mateescu | XTL: A Meta-Language and Tool for Temporal Logic Model-Checking[END_REF] is a tool that allows the parsing of BCG (an explicit representation of LTS) [START_REF] Garavel | Binary coded graphs: Definition of the bcg format[END_REF], and can perform operations at a lower level than classical temporal logic. Since XTL is a programming language, it can also be used to define non-standard temporal operators and, more generally, to perform any computation on an LTS model. In this thesis, we used it to traverse the LTS and print various information (e.g., list of labels going out of certain states).

XTL provides the standard predefined types with their usual operators, such as boolean, integer, character, string, etc. XTL provides also the types corresponding to the elements of a LTS model, such as the states and sets thereof (state and stateset), the transitions and sets thereof (edge and edgeset), the labels and sets thereof (label and labelset).

XTL expressions are built from classical functional programming operators, such as function calls, or pattern-matching. For example, the following XTL code computes the set of labels corresponding to the reception of a cup containing a drink different than coffee. The variable D is initialized by pattern-matching with the corresponding value contained in the label, and is used in the where clause, which allows additional filtering using a Boolean condition:

{ A:label where A -> [ CUP ?D:String where D <> "COFFEE" ] }

In addition, XTL provides four specific operators for accessing and exploring the LTS and its elements:

• the init operator returns the initial state of the LTS;

• the succ and pred operators access successors and predecessors of a state respectively;

• the in and out operators define incoming and outgoing transitions of a state respectively;

• the source and target operators access the origin and the destination states of a transition respectively.

An XTL expression can also contain quantifiers (exists) and conditional branching (if) or loop (for) control structures. For binary operators, such as +, *, <=, both prefix and infix notations are available. For instance, the definition of a corner state, i.e., the state corresponding to the target of an input transition (COIN) and the source of an output transition (CUP), can be implemented by the following XTL function: XTL being a functional language, its loop control structures operate by performing iterative computations over accumulation variables. For example, the following XTL loop for prints all corner states of an LTS: The evaluation of the for proceeds as follows. First, the accumulation variables, more precisely the state s and an action, are initialized with the initial state (init) and the empty action (nop) respectively. Then, for all corner states, an iteration is performed, that consist in assigning the state name to the accumulator (s) and printing the information through the second accumulator (fby). For certain for loops, such as the previous one, XTL also provides an abbreviated form: <| fby on s:state where corner state (s) |> ( printf ("the state ") fby print (s) fby printf (" is a corner state\n") )

def
As in MCL, one can also define macros in XTL, for instance the following example of XTL macro definition implements the drink transition, characterizing all edges labeled by a drink (coffee or tea) action:

macro drink transition (e) = (((e) -> [TEA]) or ((e) -> [COFFEE])) end macro
For a more detailed presentation of XTL see [START_REF] Mateescu | Vérification des propriétés temporelles des programmes parallèles[END_REF][START_REF] Mateescu | XTL: A Meta-Language and Tool for Temporal Logic Model-Checking[END_REF].

Asynchronous model-based testing (the ioco theory)

After verifying the formal model of a system (e.g., using model checking), one can check the conformance of the system under test (SUT) against this formal model. This can be carried out by Model-Based Testing (MBT), which generates tests from the model. The purpose of such test suites is either to check if the SUT is correct, or if the model does not correspond to the SUT.

Conformance testing aims at extracting from a formal model (M) of a system a set of test cases to assess whether an actual implementation of the SUT conforms to the model, using black-box testing techniques (i.e., without knowledge of the actual code of the SUT). This technique is particularly suited for nondeterministic concurrent systems, where the behavior of the SUT can be observed and controlled by a tester only via dedicated interfaces, called points of control and observation. Often, the formal model is an IOLTS3 (Input/Output Labelled Transition System), where transitions between states of the system are labeled with an action classified as input, output, or internal (i.e., unobservable, usually denoted by τ ). In this setting, the most prominent conformance relation is inputoutput conformance (ioco) [START_REF] René | Towards formal test purposes[END_REF][START_REF] Tretmans | Model Based Testing with Labelled Transition Systems[END_REF]. In this section, we present the ioco relation and a few tools that use variants of the ioco conformance relation. Other model-based tools for combinatorial and statistical testing, or white box testing are described in [START_REF] Utting | A taxonomy of model-based testing approaches[END_REF].

According to this relation, the SUT conforms to the model if and only if the SUT passes all tests generated from the model. In our context, we are interested in MBT using LTSs and the input/output conformance (ioco) relation proposed by the conformance testing theory. The SUT behaves as an input-enabled LTS (i.e., IOTS), from all states every input is possible. Intuitively, a SUT (with initial state s) ioco-conforms to a model (with initial state m), if and only if:

• when s produces an output !x after a trace σ, m can also produce the output !x after the trace σ;

• and when s cannot produce any output after a trace σ, m cannot produce either any output after this trace σ, which denotes the quiescence δ.

Formally, ioco relates an SUT ∈ IOT S and a model M ∈ IOLT S:

ioco ⊆ IOT S(A i , A o ) × LT S(A i ∪ A o )
The ioco relation is defined in terms of observing outputs as follows:

SU T ioco M = def ∀σ ∈ Straces(m): out(s after σ) ⊆ out(m after σ)
where: 8]), the model M specifies that after input coins ?20 output cup !coffee must occur, which is expressed as: out(M after coins ?20) = {cup !coffee}. The system under test S 2 satisfies this requirement, but S 1 does not: out (S 1 after coins ?20) = {cup !coffee, δ} ⊆ {cup !coffee}. Effectively S 1 is not ioco M, because the system under test should not produce more outputs than allowed by the model. Note that S 2 ioco M, even if out (S 2 after coins ?10) = {cup !tea} because coins ?10 / ∈ Straces(M).

• p δ - -→ p = ∀!x ∈ A o ∪ {τ }.p !x - -→ • Straces(m) = {σ ∈ (A ∪ {δ}) * |m σ = ⇒} • p after σ = {p |p σ = ⇒ p } • out(P ) = {!x ∈ A o |p !x - -→, p ∈ P } ∪ {δ|p δ - -→ p, p ∈ P },
q 0 q 0 q 1 q 2 q 3 q 3 q 2 q 1 q 0 q 1 δ q 4 q 3 q 2 (M) (S 2 ) (S 1 )
Although model-based conformance testing has been intensively studied, there are only a few tools that use variants of the ioco conformance relation and that are still actively developed [START_REF] Belinfante | and Christian Schallhart. 14 Tools for Test Case Generation[END_REF]. In this section we will compare the main ones: AGEDIS In this thesis, in order to face the state-space explosion of the complex GALS model we needed an on-the-fly model-based testing tool with test selection, the test selection description could contain data, so we decided to extend the TGV approach.

The TGV approach

In this section we give an overview of the TGV approach, readers familiar with the TGV approach can safely skip this section.

We assume that the behavior of the SUT can also be represented as an IOLTS, even if it is unknown (the so-called testing hypothesis [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF]). In the sequel, we consider the same running example as [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF], whose IOLTS model M is shown on Figure 2.7.

Input actions of the SUT are controllable by the environment, whereas output actions are only observable. Testing allows one to observe the execution traces of the SUT, and also to detect quiescence, i.e., the presence of deadlocks (states without successors), outputlocks (states without outgoing output actions), or livelocks (cycles of internal actions). The quiescence present in an IOLTS L (either the model M or the SUT) is modeled by a suspension automaton ∆(L), an IOLTS obtained from L by adding self-loops labeled by a special output action δ on the quiescent states. The SUT conforms to the model M modulo the ioco relation [START_REF] Tretmans | Conformance Testing with Labelled Transition Systems: Implementation Relations and Test Generation[END_REF] if after executing each trace of ∆(M), the suspension automaton ∆(SUT) exhibits only those outputs and quiescences that are allowed by the model. Since two sequences having the same observable actions (including quiescence) cannot be distinguished, the suspension automaton ∆(M) must be determinized before generating tests.

The test generation technique of TGV is based upon test purposes, which allow one to guide the selection of test cases. A test purpose guides the exploration of the specification model to have more focused test cases. Formally, a test purpose for a model M = (Q M , A M , T M , q M 0 ) is a deterministic and complete (i.e., in each state all actions are accepted) IOLTS TP = (Q TP , A TP , T TP , q TP 0 ), with the same actions as the model A TP = A M . TP is equipped with two sets of trap states Accept TP and Refuse TP , which are used to select desired behaviors and to cut the exploration of M, respectively. In the TP shown on Figure 2.8, the desired behavior consists of an action !y followed by !z and is specified by the accepting state q 3 ; notice that the occurrence of an action !z before a !y is forbidden by the refusal state q 2 . In a TP, a special transition of the form q * → q is an abbreviation for the complement set of all other outgoing transitions of q. These *-transitions facilitate the definition of a test purpose (which has to be a complete IOLTS) by avoiding the need to explicitly enumerate all possible actions for all states. Test purposes are used to mark the accepting and refusal states in the IOLTS of the model M. In TGV, this annotation is computed by a synchronous product [JJ05, Definition 8] SP = M × TP. Notice that SP preserves all behaviors of the model M because TP is complete and the synchronous product takes into account the special *-transitions. When computing SP, TGV implicitly adds a self-looping *-transition to each state of the TP with an incomplete set of outgoing transitions. To keep only the visible behaviors and quiescence, SP is suspended and determinized, leading to SP vis = det(∆(SP)). Figure 2.9 shows an excerpt of SP vis limited to the first accepting and refusal states reachable from q SP vis 0 .

A test case is an IOLTS TC = (Q TC , A TC , T TC , q TC 0 ) equipped with three sets of trap states Pass ∪ Fail ∪ Inconc ⊆ Q TC denoting verdicts. The actions of TC are partitioned into A TC I and A TC O subsets 4 . A test case TC must be controllable, meaning that in every state, no choice is allowed between two inputs or an input and an output (i.e., the tester must either inject a single input to the SUT, or accept all the outputs of the SUT). Intuitively, a TC denotes a set of traces containing visible actions and quiescence that should be executable by the SUT to assess its conformance with the model M and a test purpose TP. From every state of the TC, a verdict must be reachable: Pass indicates that TP has been fulfilled, Fail indicates that SUT does not conform to M, and Inconc indicates that correct behavior has been observed but TP cannot be fulfilled. An example of TC (dark gray states) is shown on Figure 2.9. Pass verdicts correspond to accepting states (e.g., q 11 ). Inconclusive verdicts correspond either to refusal states (e.g., q 4 or q 6 ) or to states from which no accepting state is reachable (e.g., state q 10 ). Fail verdicts, not displayed on the figure, are reached from every state when the SUT exhibits an output action (or a quiescence) not specified in the TC (e.g., an action !z or a quiescence in state q 1 ).

In general, there are several test cases that can be generated from a given model and test purpose. The union of these test cases forms the Complete Test Graph (CTG), which is ∪ {δ} (TC captures outputs and quiescences of SUT). To avoid confusion, we consider here that inputs and outputs of TC are the same as those of M and SUT.

an IOLTS having the same characteristics as a TC except for controllability. Figure 2.9 shows the CTG (light and dark gray states) corresponding to M and TP, which is not controllable (e.g., in state q 5 the two input actions ?a and ?b are possible). Formally, a CTG is the subgraph of SP vis induced by the states L2A (lead to accept) from which an accepting state is reachable, decorated with pass and inconclusive verdicts. A controllable TC exists iff the CTG is not empty, i.e., q SP vis 0 ∈ L2A [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF].

The execution of a TC against the SUT corresponds to a parallel composition TC || SUT with synchronization on common observable actions, verdicts being determined by the trap states reached by a maximal trace of TC || SUT, i.e., a trace leading to a verdict state. Quiescent livelock states (infinite sequences of internal actions in the SUT) are detected using timers, and lead to inconclusive verdicts. A TC may have cycles, in which case global timers are required to prevent infinite test executions. For a more detailed presentation of TGV see [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF].

In this thesis, we will present a new tool for on-the-fly conformance test case generation tool based on the TGV approach, but enabling online testing by generating controllable test cases completely on the fly and a more versatile description of test purposes than the TGV ones using the LNT language.

GALS Models and Validation

A GALS (Globally Asynchronous and Locally Synchronous) system consists of several independent synchronous components that evolve concurrently, each at its own pace, and communicate all together asynchronously. A GALS system is a particular asynchronous system, but with additional difficulty when faithfully modelling it as a composition of synchronous components, with all the synchronous constraints (one clock, no interleaving during a component execution, synchronous loop). To model it formally and manage the complexity of the underlying state space (and hence of the analysis), one has to consider the following aspects: C1. atomicity of synchronous components, i.e., the execution of the synchronous component can not be interrupted or reduced before its end;

C2. interleaving of the execution of synchronous components, i.e., the order of synchronous component executions is not fixed;

C3. nondeterminism induced by the absence of a shared clock and by the unreliable communication media (messages can be delayed, lost, duplicated, or reordered);

C4. data constraints on the inputs and/or outputs of components, which, combined with nondeterminism allow to calibrate the description of the system; C5. activation constraints on the components, which allow to control the degree of asyn- Due to the different semantics and abstraction level, a direct modeling with only synchronous or asynchronous languages could be complex. Instead, using a single GALSspecific language enables to reduce that complexity. Although GALS models have been intensively studied, as far as we know GALS Representation Language (GRL) [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF] is the only existing DSL with formal semantics specially designed for GALS systems.

Thus, in this thesis, we use GRL to describe the global behavior of GALS systems. GRL is equipped with the GRL2LNT [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF] translator to LNT [START_REF] Garavel | From LOTOS to LNT[END_REF], which provides a connection to the CADP verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF].

An overview of the GRL language

We present here an overview of the GRL language, the reader familiar with GRL can safely skip this section. GRL [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF] is a formal language designed to model the behavior of GALS systems. GRL enables the behavioral modelling of synchronous components (determinism, atomicity), asynchronous communication (nondeterminism, asynchronous concurrency), and constraints involving both component activations and the data carried by component inputs. Concretely, GRL integrates the synchronous reactive model underlying dataflow languages and the asynchronous interleaving semantics of concurrency underlying process algebras.

GRL provides constructed data types, constants, statements built upon standard algorithmic control structures, and functions. GRL supports all the basic types of LNT (see Section 2.3.1), such as bool, int, real numbers, and character string, as well as user-defined LNT types (bounded or unbounded), such as records, unions, lists, sets, and arrays. For instance, the following LNT type defines the enumerated data type window_status. The with clause specifies the predefined functions for this type (in our case, the comparison operations).

type window_status is open, close, already_sent with "!=", "==" end type

The constants are defined by the keyword const and are necessarily initialized. Here is an example of numerical constant max_open_time, corresponding to the maximum duration (in minutes) for which the window could be open without a reaction of the smart heater:

const max_open_time: nat := 10;
The GRL model reflects the modular specification, connecting the synchronous components by a communication network. Figure 2.11 shows the architecture of a formal GRL model for the smart room temperature management seen in Figure 2.10. Each of the two synchronous components (smart_window_contact and smart_heater) is represented in GRL as a block, depicted as a (light blue) rectangle with solid border in Figure 2.11. These blocks exchange data via asynchronous communication media (state), which is represented in GRL as a medium, depicted as a (pink) ellipse with dashed border in Figure 2.11. The interaction between blocks has also to respect environmental constraints, represented in GRL as an environment (room_temperature), depicted as a (light pink) ellipse with thick dashed border in Figure 2.11. The overall model of the GALS is represented in GRL as a system, which describes the composition and interactions of blocks, media, and environments.

Block

A GRL block defines the deterministic code executed at each activation (i.e., clock pulse) by the synchronous component. GRL blocks behave as deterministic and atomic synchronous components that interleave with other blocks. For defining blocks, GRL provides a set of basic synchronous language constructs. GRL block statements are inspired by those of LNT, such as variable assignment, sequential composition, conditional (if-then-else), loops (for, while), and extended with block invocations, and communication primitives. Because the initial idea behind GRL blocks was to generate them from a synchronous language, one has to manually implement these three classical synchronous languages operators:

1) The synchronous parallel operator is not provided by GRL, the composition between GRL blocks is sequential and require to define a correct order between blocks.

2) The delay operator is not explicitly present, but GRL makes explicit the internal state through the usage of static variables. One should manage the access and update the block's internal states or the delay operators could be encoded in GRL libraries.

3) The explicit loop, for and while loops are also missing in GRL. One can encode bounded operators in GRL libraries.

Therefore, GRL is less user-friendly for describing synchronous components5 than using a full-fledged synchronous language, such as Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF]. For instance, the smart window contact of the smart room temperature management could be modeled by a GRL block smart_window_contact (defined below). This block has three static variables, which define its internal states:

• opening_time to keep track of the (abstract) time when the window is open from the previous activation (this time is considered to be initially null);

• previous_info to keep track of the perception information (open window or closed one) computed and sent during the previous activation;

• is_open to keep track of the perception information open or not even if the window is open for less than max_open_time minutes.

At each activation, the smart_window_contact block receives the current time (in parameter time). It then computes the current window status send_info indicating if the window is open (opened for more than max_open_time minutes), or closed. If there is a change between previous_info and info (the window was not open for more than max_open_time minutes, or did not close after being open), both the variable previous_info and the output send_info are updated; otherwise the output is set to the particular value already_sent indicating that the status of the window did not change. At the end of the activa-tion, the computed window status info is sent to the connected medium (send parameter send_info), and it sends the status to the environment managing the activation of the block smart_heater through the out status channel. The function perception_window_open detects if the window is open or not.

Medium

Synchronous blocks interact with each other via asynchronous communication media. GRL media do not impose any communication protocol, but provide enough expressiveness to model general communication mechanisms. Explicitly representing these media makes it possible to finely model a large panel of behaviors (i.e., message buffering, message loss, nondeterminism, etc.). A medium is connected to each block by at most two channels, called receive and send channels. Note that a receive channel corresponds to the reception of some value in a variable prefixed by "?". Channels are tuples of variables, by which the synchronizations between components (rendezvous) take place. Each channel has an associated Boolean condition (tested with a when clause), stating whether a message is available or should be sent. GRL media statements are those of the blocks and extended with nondeterministic statements. For instance, the following GRL medium state enables the block smart_window_contact to send the current perception window status (via the receive channel send_info) to the block smart_heater (via the send channel receive_info); the transmission takes place only when the window status information has not already been sent.

Environment

GRL environments model the external environment of blocks; by providing their inputs and receiving their outputs. Concretely, an environment is a loop, where at each iteration at most one block is activated. Blocks and environments are connected through input and output channels, with a primitive communication data signal, i.e., a data signal is executed by the environment, if an interaction on a channel occurs (receiving in or sending out). Note that an environment may be nondeterministic, e.g., it may contain nondeterministic choice, modelled in GRL using the select statement, as in LNT. For instance, the following GRL environment room_temperature ensures that: (1) the (abstract) time, which corresponds to the number of activations (ticks), is shared with the block smart_window_contact (by sending this information to smart_window_contact as input time); (2) the evolution of the (abstract) temperature is changed gradually and shared with the block smart_heater (by sending it as input temperature). Note that in order to execute its body several times, an environment should contain a loop, whereas the synchronous loop is built-in in block definitions, therefore, the body of a block contains only the code executed at each activation.

Block activations are particular implicit inputs of blocks, enabling an environment to precisely control the activations of synchronous blocks. GRL enables to model various activations, by using the keyword enable. In the following environment example, the activation signal enable implements the permission for the block smart_heater to execute only if the window is closed or open for less than ten minutes (window_status)):

--Environment constraining the block activations environment smart_heater_activation (block smart_heater in status: window_status) is loop when status -> if status == false then enable smart_heater end if end loop end environment System GRL systems define GALS as sets of blocks, environments, and media. The system behavior can be refined to model detailed communication strategy and constraints. Also to reduce the complexity, one can model in a system the behavior of blocks separately, or a primary system behavior with simple communication media and test case scenarios. The following GRL system describes the complete model of the smart room temperature management, built by composing the blocks smart_window_contact and smart_heater, the medium state, and the environment room_temperature, introduced by the keywords block list, medium list, and environment list, respectively. The component aliasing smart_heater (heater) is required for the environment smart_heater_activation to control its activation. GRL defines the semantics of a GALS system as an LTS (Labeled Transition System), whose states represent the memories of all blocks, media, and environments of the system [Jeb16, Chapter 4]. The initial state is the initial memory, in which each static variable has its (mandatory) initial value. Each transition going out of a state corresponds to the atomic execution of a block, which consists in reading the values of input and receive channels, executing the code of that block activation, and producing the values for the outputs and send channels of the block. The transition is labeled with all these values, and its target state corresponds to the updated memories of the participating components, i.e., the block and its connected media and environments. Thus, the atomic executions of synchronous blocks are interleaved in the LTS, which reflects the GALS nature of the system.

For technical reasons, we rely in this thesis on the semantics of GRL as induced by the current translation-based implementation of GRL. In this semantics [Jeb16, Chapter 5], the execution of a synchronous block activation is split into an input transition followed by an output transition. These two transitions are executed atomically, i.e., without interleaving with any other transitions corresponding to an activation of another block. GRL is equipped with the GRL2LNT [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF] translator to LNT [START_REF] Garavel | From LOTOS to LNT[END_REF], which provides a connection to the CADP tools. For a more detailed presentation of GRL see [START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF][START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF].

Verification of GALS systems

Milner's proposal [START_REF] Milner | Calculi for Synchrony and Asynchrony[END_REF] to encode asynchronism in a synchronous process calculus has been used to specify GALS systems using synchronous programming approaches [HB02, GTL03, MGT + 04, HM06]. These approaches do not retain a finer modeling of the overall GALS system and consider only the synchronous verification. The global aspects of a GALS system and the asynchronous validation are missing.

Following a bottom-up approach [START_REF] Günther | On the formal verification of systems of synchronous software components[END_REF], manually defining contracts for the synchronous components (to be verified locally, for instance using SCADE [START_REF] Berry | SCADE: Synchronous design and validation of embedded control software[END_REF]), the overall GALS system can be verified by translating the network of component contracts and verification properties into Promela (for verification with SPIN [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF]) or timed automata (for timing analysis with UPPAAL [BDL + 01]).

A graphical tool set [RSD + 04], based on the specification of the synchronous components as communicating reactive state machines, translates the system and its properties specified as observers into Promela for verification with SPIN. This tool focuses on the verification of the overall GALS system.

Encapsulating synchronous components makes the overall GALS system amenable for analysis with asynchronous verification tools. This approach has been followed for a combination of the synchronous language SAM, the asynchronous language LNT, and the CADP toolbox [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF], and a combination of the synchronous language SIGNAL, the asynchronous language Promela, and the model checker SPIN [DMK + 06].

Focusing on communication media for GALS hardware circuits, the asynchronous connections between synchronous blocks can be encoded into variants of Petri nets dedicated to the analysis of hardware circuits [START_REF] Frank | A Structured Visual Approach to GALS Modeling and Verification of Communication Circuits[END_REF]. On the contrary, our approach targets the testing of synchronous components of more generic GALS systems, relying on less precise models of the communication signals.

As far as we know, we propose the first approach of Model Based Testing for GALS systems. In this thesis, we retain a fine modeling of the synchronous components in the overall GALS system and consider the validation of both, the overall GALS system and its synchronous components. The overall flow of our approach is illustrated in Figure 2.12. For modelling and validating the synchronous components, we will use the synchronous data flow language Lustre (see Section 2.2.1) and the synchronous Lurette testing tool (see Section 2.2.3). For the global GALS behavior model, we chose the formal GRL language (see Section 2.4.1).

We

Chapter 3 Validation Techniques for Synchronous Components

In this chapter we illustrate formal techniques for the functional testing of a synchronous component, using a case study of a synchronous dataflow algorithm: The Message Authenticator Algorithm (MAA), a pioneering cryptographic function designed in the mid-80s at the National Physical Laboratory (NPL, United Kingdom). Part of this work has been published in [START_REF] Garavel | A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm[END_REF] and in [START_REF] Garavel | Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm[END_REF].

The chapter is organized as follows. Section 3.1 presents the MAA, both from a technical and an historical perspective. Section 3.2 presents the modeling of the MAA using the synchronous dataflow language Lustre. Section 3.3 precises how the Lustre model has been validated. Section 3.4 gives an overview of our supplementary work on three other formal models describing the full MAA. Finally, we give summarizing remarks on our work and synchronous testing.

The Message Authenticator Algorithm (MAA)

In data security, a Message Authentication Code (MAC) is a short sequence of bits that is computed from a given message; a MAC ensures both the authenticity and integrity of the message, i.e., that the message sender is the stated one and that the message contents have not been altered. A MAC is more than a mere checksum, as it must be secure enough to defeat attacks; its design usually involves cryptographic keys shared between the message sender and receiver.

T S W M n W X Y M 1 W W Y X Initialization Discard V future use V X 0 J K Prelude contains BYT/PAT, MUL1, MUL2 Z PRELUDE XOR MAIN_LOOP CODA Keys Message M 1 M n Y 0 V 0 W S T Storage for (Contains MUL1 MUL2A
) The MAA was intended to be implemented in software and to run on 32-bit computers. Hence, its design intensively relies on 32-bit words (called blocks) and 32-bit machine operations. Figure 3.1 (inspired by [DC88, Figure 21]), gives an overview of the data flow of the MAA. The MAA takes as inputs a key and a message. The key has 64 bits and is split into two blocks J and K. The message is seen as a sequence of blocks. If the number of bytes of the message is not a multiple of four, extra null bytes are added at the end of the message to complete the last block. The size of the message should be less than 1,000,000 blocks; otherwise, the MAA result is said to be undefined; we believe that this restriction, which is not inherent to the algorithm itself, was added in the second ISO standard [START_REF] Iso | Approved Algorithms for Message Authentication -Part 2: Message Authenticator Algorithm[END_REF] to provide MAA implementations with an upper bound (four megabytes) on the size of memory buffers used to store messages.

1 st MAIN_LOOP iteration n th MAIN_LOOP iteration X := X 0 Y := Y 0 V := V 0 n + 1 th MAIN_LOOP iteration n + 2 th MAIN_LOOP iteration
The MAA produces as output a block, which is the MAC value computed from the key and the message. The fact that this result has only 32 bits proved to be a major weakness enabling cryptographic attacks; MAC values computed by modern algorithms now have a much larger number of bits. Apart from the aforementioned restriction on the size of messages, the MAA behaves as a totally-defined function; its result is deterministic in the sense that, given a key and a message, there is only a single MAC result, which neither depends on implementation choices nor on hidden inputs, such as nonces or randomlygenerated numbers.

The MAA calculations rely upon conventional 32-bit logical and arithmetic operations, among which: AND (conjunction), OR (disjunction), XOR (exclusive disjunction), CYC (circular rotation by one bit to the left), ADD (addition), CAR (carry bit generated by 32-bit addition), MUL (multiplication, sometimes decomposed into HIGH_MUL and LOW_MUL, which denote the most-and least-significant blocks in the 64-bit product of a 32-bit multiplication). On this basis, more involved operations are defined, among which MUL1 (result of a 32-bit multiplication modulo 2 32 -1), MUL2 (result of a 32-bit multiplication modulo 2 32 -2),

MUL2A (faster version of MUL2), FIX1 and FIX2 (two unary functions1 respectively defined as x → AND(OR(x,A),C) and x → AND(OR(x,B),D), where A, B, C, and D are the four hexadecimal block constants A = 02040801, B = 00804021, C = BFEF7FDF, and D = 7DFEFBFF). The MAA operates in three successive phases:

• The PRELUDE takes the two blocks J and K of the key and converts them into six blocks X 0 , Y 0 , V 0 , W , S, and T . This phase is executed once. After the prelude, J and K are no longer used.

• The MAIN_LOOP successively iterates on each block M n of the message (M 1 , ..., M n ). This phase maintains three variables X, Y , and V (initialized to X 0 , Y 0 , and V 0 , respectively), which are modified at each iteration. The main loop also uses the value of W , but neither S nor T .

• The CODA adds the blocks S and T at the end of the message and performs two more iterations on these blocks. After the last iteration, the MAA result is XOR(X, Y ), called Z.

In 1987, the second ISO standard [ISO87, Section 5] introduced an additional feature (called mode of operation), which concerns messages longer than 256 blocks and which, seemingly, was not present in the early MAA versions designed at NPL. containing less than 256 blocks. The above MAA algorithm (prelude, main loop, and coda) is applied to the first segment, resulting in a value noted Z 1 . This block Z 1 is then inserted before the first block of the second segment, leading to a 257-block message to which the MAA algorithm is applied, resulting in a value noted Z 2 . This is done repeatedly for all the n segments, the MAA result Z i computed for the i-th segment being inserted before the first block of the (i + 1)-th segment. Finally, the MAC for the entire message is the MAA result Z n computed for the last segment.

MAA MAA MAA MAA final MAC result Z 1 Z n Z i+1 segment i+1 segment 1 segment 2 segment 2 last last segment i+1
From the point of view of formal methods, the MAA is interesting because of its pioneering nature, because its definition is freely available and stable, and because it is involved enough while remaining of manageable complexity. Over the past decades, various formal specifications of the MAA have been developed, either non-executable ones using VDM in 1990 [PO90, PO91], using Z in 1991 [START_REF] Lai | A Formal Interpretation of the MAA Standard in Z[END_REF], and LOTOS in 1990/1991 [START_REF] Harold | LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS[END_REF][START_REF] Harold | Comments on the LOTOS Standard[END_REF] or executable ones using LOTOS, written by Hubert Garavel and Philippe Turlier in 1992 (LOTOS-92), and using LNT written by Wendelin Serwe in 2016 (LNT-16). For such formalism, the usual examples often deal with syntax trees, which are explored using standard traversals (breadth-first, depth-first, etc.); contrary to such commonplace examples, cryptographic functions (and the MAA, in particular) exhibit more diverse behavior, as they rather seek to perform irregular computations than linear ones.

Modelling the MAA in Lustre

We considered the MAA models LOTOS-92 and LNT-16 and extended them to model the full MAA algorithm in the synchronous formal language Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF] (more details about Lustre are available in Chapter 2 Section 2.2.1). We decided to take advantage of Lustre connection to robust testing tools, actively supported and maintained by developers. A large part of our Lustre model contains general definitions, half of which are largely independent of the MAA. The whole Lustre model of the MAA is presented in the Appendix A. The architecture of this model follows the dataflow shown on Figure 3.1.

We chose to represent blocks as words of four bytes, rather than thirty-two bits. So doing, the logical operations on blocks (AND, OR, XOR, and CYC) are easy to define using bitwise and bytewise manipulations. The bits, bytes and blocks are represented with the three following Lustre data structures: Then, we defined a set of functions to implement the corresponding logical operations on bits, bytes, and blocks. The arithmetical operations (ADD, CAR, and MUL) have been implemented using 8-bit, 16-bit, and 32-bit adders and multipliers, more or less inspired from the theory of digital circuits. Thus, the structure Pair shown below, represents results of the multiplication of two blocks.

type Pair = struct {w1: Block; w2: Block};

A message is a list of blocks, each block of the message is an input of the main MAC node in Lustre, shown in Figure 3.3. Long messages (i.e., containing more than one block) are hard coded in functions, as for instance, the twenty-words message in the Appendix A.16.

The MAC node takes as input the message to encode, and a key, which corresponds to two words (called K and J). A local variable init defines the beginning of a message, and another variable n stores the number of blocks, in order to ensure the implementation of the "mode of operation" of the MAA, i.e., segmentation of messages larger than 1024 bytes (as explained in Section 3.1). The MAC gives as outputs the result of the intermediate computations (prelude, mainloop) in the auxiliary blocks (X, Y, V, W, S, T), and the result of its main computation, which is represented with a variable (Z) containing the MAC for the given input (one key and a message). At each call of the Lustre node MAC, one new block of the message is processed as follows:

• for the 1 st block of the message, the auxiliary variables (X, Y, and V) are computed with an iteration of the mainLoop function with the initial values (X0, Y0, V0) computed by the function prelude shown in Figure 3.3;

• for the 257 th block of the message, the auxiliary variables are computed with an iteration of the mainLoop2 function, which consists of two iterations of the mainLoop, one on the result of the previous coda (Z), and one on this block message;

• and, for the other blocks of the message, the auxiliary variables are computed by taking into account the previous auxiliary variables (pre X, pre Y, and pre V) computed by the previous block.

Keys could also be represented using the type Pair, but we prefer introducing the following dedicated structure Key to clearly distinguish between keys and, e.g., results of the multiplication of two blocks:

type Key = struct {K: Block; J: Block};

We defined the "multiplicative" functions used for MAA computations, most of which were present in [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF] or have been later introduced in [START_REF] Menezes | Handbook of Applied Cryptography[END_REF]. The three principal low-level operations are MUL1, MUL2, and MUL2A, with its auxiliary functions. We also defined the higher-level functions that implement the MAA algorithm on one segment (maximum 1024-byte), namely the prelude, the inner loop, the coda, as well as the principal function MAC (that computes the 4-byte signature of a message).

It turned out that Lustre enables an elegant modeling of the involved data structures, such as enumeration (e.g., the enumeration Bit) and structures (e.g., the type Byte defined as Octet). We briefly discuss below some of our choices for modeling the MAA in Lustre.

Usage of local variables. Local variables are essential to store computed results that need to be used several times, thus avoiding identical calculations to be repeated. Lustre allows to freely define and assign local variables; the compiler guaranties that each variable is duly assigned before used. However, Lustre forbids successive assignments to the same variable. For instance, the MUL2 function can be expressed in Lustre as follows:

Testing the MAA Model

To validate our Lustre model, we defined four sets of test vectors derived from the specification in [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF]:

(T1) implements the 36 checks listed in Tables 1, 2, and 3 of [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF]. These test vectors specify, for a few given keys and messages, the expected values of intermediate calculations (e.g., MUL1, MUL2, MUL2A, etc.).

(T2) is based upon Table 4 of [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF], checking if the main loop of MAA (as described on page 10 of [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF]) is correctly implemented on six groups of checks (three single-block messages and one three-block message); T2 corresponds to 56 tests. In all these series of test vectors [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF], which corresponds to 201 tests, we found mistakes, which we documented and for which we gave corrections in [GM18, Annex A].

(T3) is based upon

We automate the test execution process, by using the testing tool Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF] taking advantage of its connection with the Lustre language. (ii) an oracle implementing the test decision, in our case the 12 possible pairs (one key K J, and a message of two blocks), and the expected resulting MAC; and some parameters controlling the execution and the coverage of the generated input sequences, e.g., the number of steps (n) in the execution sequence. The Lurette tool is also connected to a system under test, in our case the Lustre implementation of the MAA. More details about Lurette are available in Section 2.2.3 (Chapter 2).

As seen below, we consider hard-coded messages, and for using Lurette, the inputs of the system under test must only use the datatypes provided by Lutin (Boolean, reals, and integers). Thus, we rewrote the Lustre MAC node as below: it has two inputs, a natural number corresponding to the id of one key-message pair and a Boolean expressing the beginning of a new message segment. In the rewritten Lustre node (Figure 3.6), the function get_mess_key (line 6) takes as input an id, and returns the corresponding key and a message (the possible messages blocks and pairs are hard-coded in this function).

The Lutin code in Figure 3.7 constrains the input of the MAA to one out of four messages, containing each one two words.

Note that if the input values are not explicitly constrained in the Lutin environment, random numbers will be generated. The environment contains the 12 possible pairs of keys and messages. Although larger and more complex environments could be written, this task is tedious and error-prone, in particular due to the representation of messages and keys by natural numbers.

node MAC (id: int; init: bool) returns (X, Y, V, W, S, T, Z: Block; n: int); var X0, Y0, V0: Block; KJ: Key; Mn: Block; let Mn, KJ = get_mess_key (id); n = if init then 1 else if pre n = 256 then 0 else pre n + 1; --initialisations X0, Y0, V0, W, S, T = prelude (KJ.J, KJ.K); --mainloops X, Y, V = if init then mainLoop (X0, Y0, V0, W, Mn) else if n = 0 then --mode of operation mainLoop2 (X0, Y0, V0, W, pre Z, Mn) else mainLoop (pre X, pre Y, pre V, W, Mn); --coda Z = coda (X, Y, V, W, S, T); tel; In our example, correct tests consist of the right output (a correct MAC value), given an input vector (the id of the pair of one key and a message). A small example of oracle for the previous Lutin code is given by the Lustre code of Figure 3.9, containing the test decisions and the expected output: the auxiliary block values of X, Y and MAC value for each block of message given in the First, we undertook the translation of LOTOS-92 into a term rewrite system (REC-17). This system was encoded in the simple language REC proposed in [Gar89, Sect. 3] and [DRB + 09, Sect. 3.1], which was slightly enhanced to distinguish between free constructors and non-constructors. Contrary to higher-level languages such as LOTOS or LNT, REC is a purely theoretical language that does not allow to import external fragments of code written in a programming language. Thus, all types (starting by the most basic ones, such as Bit and Bool) and their associated operations were exhaustively defined "from scratch" in the REC language. 3. an error was found in the main C program provided by [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF], which computed an incorrect MAC value, as the list of blocks storing the message was built in reverse order;

4. three others errors were found in the Lustre v6 toolbox: (i) lv6 compiler generating invalid C code if a variable identifier uses quotes ('); (ii) another issue with constant structures and the compiler lv6; and (iii) Lurette tool ignoring -2c-exec option; all these errors have been communicated to the Lustre v6 developers and have been quickly fixed by Erwan Jahier;

5. another error was found in the external implementation in C of the function HIGH_MUL, which computes the highest 32 bits of the 64-bit product of two blocks and is imported by the LOTOS and LNT models -this illustrates the risks arising when formal and non-formal codes are mixed.

It is however fair to warn the reader that testing our Lustre MAA model was a tedious task: in order to automate the tests validation with a Lutin environment and an oracle, we had to define more than 400 constants. An automation of this testing process is therefore highly beneficial, as it will be illustrated in Chapter 5.

Chapter 4

Validation of Communication Protocols between Components

In this chapter we illustrate the formalization and the functional testing of communication protocols between synchronous components, taking as a case study the TLS (Transport Layer Security) handshake version 1.3 [DR06, IET18], a protocol responsible for the authentication and the exchange of keys necessary to establish or resume a secure communication.

The TLS [START_REF] Bozic | A formal TLS handshake model in LNT[END_REF] model has been validated using a new on-the-fly conformance test case generation tool named TESTOR [START_REF] Marsso | TESTOR: A modular tool for on-the-fly conformance test case generation[END_REF].

This chapter is organized as follows. Section 4.1 gives an overview of the TLS 1.3 handshake, from a technical perspective. Section 4.2 presents the LNT model of the TLS 1.3 handshake. Section 4.3 presents our new on-the-fly conformance test case generation tool TESTOR and describes various experiments to validate it. Section 4.4 describes our validation approach for the TLS handshake, using TESTOR to generate test cases.

Transport Layer Security Handshake Protocol

Security services are frequently used in fields like online banking, e-government and online shops. With increased availability of such services, the number of security risks rises both for users and providers alike. In order to ensure a secure communication between peers in terms of authenticity, privacy, and data integrity, cryptographic protocols are applied to regulate the data transfer. These protocols provide a standardized set of rules and methods for the interaction between peers. Transport Layer Security (TLS) [START_REF] Dierks | The transport layer security (TLS) protocol version 1.1[END_REF] is a widely used security protocol, designed as a successor of Secure Sockets Layer (SSL) [START_REF] Weaver | Secure sockets layer[END_REF]. Both protocols encompass a set of rules for the communication between client and server and rely on public-key cryptography to ensure integrity of exchanged data.

In this chapter, we focus on the TLS handshake protocol, which enables a TLS client and server to establish a secure, authenticated communication link. The TLS handshake consists of four steps: (i) consent on the version of the protocol to use and choose cryptographic algorithms; (ii) exchange and validate certificates to authenticate each other; (iii) generate a shared secret key; and (iv) abort the handshake with an alert if something goes wrong. We present below the main TLS 1.3 handshake messages exchanged, as well as the exchange process between the server and the client(s).

Handshake TLS 1.3 interactions

The TLS messages make up the interaction between a client and a server and exchange values between them. The most important feature is the negotiation of cryptographic parameters that ensures privacy and integrity of exchanged information. During the protocol, client and server agree on used protocol version, exchange random values and select cryptographic algorithms for encryption and decryption of transferred data. Both peers exchange keys and certificates and after the handshake is finished, they can start to encrypt and exchange application data.

A summary of the interactions and the message exchanges from the client side and the server side is respectively depicted in the state machines [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF] shown on Note that these state machines do not represent the client's and server's Alert message interactions. The server and the client have to abort the handshake with an Alert message if one of the TLS 1.3 requirements textually described in the draft TLS 1.3 handshake [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF] is not respected. As an example, we describe here three requirements taken from the draft TLS 1.3 handshake [IET18]:

• The handshake messages should be sent in one of the orders represented in a path of the state machines given in Figure 4.1 and Figure 4.2. If a message is sent in the wrong order, the handshake connection will be aborted with an "unexpected message" alert.

• The TLS 1.3 handshake refuses renegotiation without a hello retry request message, thus the client hello message can only be exchanged in the beginning of the protocol or after receiving a hello retry request message. If renegotiation takes place without a hello retry request message, the handshake is aborted with an "unexpected message" alert.

• When the client receives a hello retry request message, the client should check that cryptographic information contained in the hello retry request is different from the information in the initial client hello message. If not, the handshake is aborted with an "illegal parameter" alert.

The difficulty in modelling the TLS was the extraction of definitions from the informal definition of the TLS 1.3 handshake requirements in [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF]. Since this informal specification is not self-contained, it refers to many documents, e.g., the alert management.

In the sequel, we will not consider the internal processing of the TLS handshake but we will focus instead on the TLS messages, leaving the information exchange to be handled by the execution framework and the SUT. In the next section, we detail the handshake messages exchanged.

Main TLS 1.3 handshake messages

The handshake itself consists of different message types, so-called TLS messages, and corresponding parameters that are part of these messages. Every such parameter comprehends specific values, where some of them are assigned dynamically during the handshake procedure. The main messages exchanged during the TLS handshake steps are: i. The client and the server agree upon the version of the protocol and cryptographic algorithms to use by exchanging the client hello, hello retry request, server hello, and encrypted extensions messages.

• The client hello is always the first message, and a client should resend a client hello message only if the server responded to it by a hello retry request message. It contains the client's cryptographic information: the supported version of protocol, the pre-shared keys, the list of symmetric cipher options, and the extended functionalities.

• The server hello is the response (message) from the server to the client hello message if the server was able to select an acceptable set of handshake parameters based on the client hello. It contains the cryptographic information selected: the protocol version, the list of symmetric cipher, and the server extensions.

• The hello retry request is the response (message) from the server to the client hello message if the server was not able to select an acceptable set of parameters. It contains the same cryptographic information as the server hello message.

• The encrypted extensions message is sent by the server immediately after the server hello message. This is the first message that is encrypted using keys derived from the server handshake traffic secret. It contains extensions that can be protected.

ii. An authentication with a certificate between the server and the client can be requested by exchanging the certificate request, certificate, and certificate verify messages.

• The certificate request message must be sent by the server directly after the encrypted extensions message if the server requests a certificate. It contains an identification of the certificate request and a set of extensions describing the parameters of the certificate.

• The certificate message is sent by the server and by the client. It contains their respective certificate to be used for authentication, and any other supporting certificates.

• The certificate verify message is directly sent by the server and by the client after the respective certificate message. It contains a signature using the private key corresponding to the public key in the certificate message.

iii. The server and the client generate and share a secret key by exchanging the finished message. The finished message is sent by the server, then by the client. It contains a message authentication code (MAC).

iv. At any step of the handshake, the client or the server can abort the handshake, and close the connection if a failure happened. To do so, they should exchange an alert message. The alert message contains the description of the alert.

A number of TLS handshake messages contain encoded extensions. There are 21 types of extensions defined in [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF] (e.g., "supported versions", "cookie", "negotiated groups", etc.). For instance, the "supported versions" extension is a list of supported versions in preference order, and it is used by the client to indicate which versions of TLS it supports and by the server to indicate which version it is using. The client sends its extension requests in the client hello message and the server sends its responses in the server hello extension, encrypted extensions, hello retry request extensions and certificate messages.

Formal Model of the TLS Handshake in LNT

Taking the draft specification of the TLS [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF] protocol version 1.3 as starting point, we formalize the handshake protocol of TLS in the LNT language [GLS17, CCG + 19]. In this section, we give a brief description of our model, which encompasses the handshake messages, and illustrate then the handshake interactions. We discuss the challenges to specify the TLS handshake in LNT with concrete examples. The full LNT model is given in [BMMW18]1 .

Handshake interactions

Our modeling of the communication between client and server is based on the state machines (Figures 4.1 and 4.2) and the handshake TLS 1.3 requirements discussed in Section 4.1.1.

The server and the client are modeled by two processes [START_REF] Bozic | A formal TLS handshake model in LNT[END_REF] communicating by rendezvous on gates, i.e., the communication is blocked by both sending and receiving messages: the one waiting for a rendezvous is suspended and terminates immediately after the rendezvous takes place. Concretely, the server and the client processes correspond to their respective state machines (Figure 4.1 and Figure 4.2) extended with the management of the Alert message. Each kind (server or client) of handshake message is implemented as a process, and two additional processes by kind of handshake message sent by the client and the server. In total there are 15 processes.

The alert management is in charge of handling handshake errors. If a handshake requirement is not respected, the handshake should be aborted with an alert message. We defined the following AlertType, an enumeration of all possible alert messages. Each process takes as parameter an alert type, which is initialized by an "undefined" alert in the main process. If a handshake requirement is not respected in a process, the corresponding alert type should be assigned to the out alert parameter, and the handshake aborted with the corresponding alert message.

type AlertType is missing_extension, unexpected_message, unsupported_certificate, ... undefined end type

During the modeling process of the handshake interactions, we took advantage of the powerful disruption operation of the LNT language. Consider for instance the following requirement: the TLS 1.3 handshake refuses renegotiation without a hello retry request message. The client hello message can only arrive at the beginning of the handshake, or right after a hello retry request message. In all other cases, if a client hello message arrives, the handshake should be aborted with an alert. To implement this requirement we used the LNT operator disrupt, which allows at any time a possible disruption of a block of code by another block. In the following LNT code, we have for instance the possible disruption of a content behavior by a client hello message (ClientHello), followed by an alert.

disrupt

... content by --TLS 1.3 refuses renegotiation without a Hello Retry Request ClientHello [clientHello_c] (false, !?CH_p, HRR_P, ?alert); alert := unexpected_message; --abort the handshake with an "unexpected message" alert alert_c (alert) end disrupt

Handshake messages

The handshake messages and their encryption information are defined as types. Our model contains 43 types, with simple types as enumerations, lists, or more sophisticated ones, such as "union like" types. Below is an example of structure-like type containing one constructor with several fields. The main challenge was the definition of "union-like" types, regrouping several types, the difficulty being to build this abstract tree of types from the informal TLS handshake description. The advantage is that, once this was done, it became easy to bring new extensions to our model. For instance, one of the encryption parameters of the client hello message is of type Extensions, which is a list of elements of type Extension, i.e., a tuple containing an extension type and an extension data.

type Extensions is list of Extension with "cons", "remove" end type type Extension is Extension (extension_type: ExtensionType, extension_data: ExtensionData) end type LNT provides some predefined functions, which simplify the modeling task by avoiding the definition of classical useful functions. For instance, the LNT definition of the client hello message described in Section 4.1.2, uses three predefined functions to support notation x.f and compare values of the ClientHello type (cons and remove). Extension type is defined by an enumeration of 21 extension types. Extension data is a type regrouping several constructors, each of them having its own parameters and corresponding to an extension type. Most of the extensions are optional, thus we implemented 9 of the 21 respective extension data constructors in our model. Consider for instance the definition of one of the mandatory extensions in TLS 1.3, the supported version extension. We want to model a supported-version extension for the protocol "TLS 1.2" in LNT. To do so, we need an extension with the supported version type, and with an extension data using the constructor SupportedVersions, which takes as a parameter a supportedVersions, i.e., a list of protocol versions.

Extension( supported_version, SupportedVersion ({TLS12}) )

type SupportedVersions is list of ProtocolVersion end type type ProtocolVersion is TLS12, ... end type Our complete LNT model of the TLS handshake 1.3 (see in [BMMW18, Appendix 16]) has 918 lines and contains 15 processes, 8 functions, 42 types, and 10 channel definitions.

TESTOR: On-the-Fly Conformance Test Case Generation

In this section, we present TESTOR2 , a tool for on-the-fly conformance test case generation guided by test purposes. Following the approach of TGV [JJ05], a test purpose characterizes some state(s) of the model as accepting. TESTOR extends the algorithms of TGV to extract controllable test cases completely on the fly (i.e., during test case execution against the SUT), making TESTOR suitable for online testing. The tool is built following a modular architecture on top of the OPEN/CAESAR [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF] generic environment for on-the-fly graph manipulation provided by CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. (i) τ -compression produces the suspension automaton ∆(SP) by squeezing the strongly connected components of τ -transitions and replacing them with δ-loops representing quiescence;

Architecture

(ii) τ -confluence eliminates redundant interleavings by giving priority to confluent τtransitions, i.e., whose neighbor transitions (going out from the same source state) do not bring new observational behavior;

(iii) τ -closure computes the transitive reflexive closure on τ -transitions;

(iv) the resulting τ -free IOLTS is determinized by applying the classical subset construction.

The reduction by τ -compression is necessary for τ -confluence (which operates on IOLTSs without τ -cycles) and is also useful as a preprocessing step for τ -closure (whose algorithm is simpler in the absence of τ -cycles). Although τ -confluence is optional, it may reduce drastically the size of the IOLTS prior to τ -closure, therefore acting as an accelerator for the whole test selection procedure when SP contains large diamonds of τ -transitions produced by the interleavings of independent actions [START_REF] Mateescu | On-the-fly State Space Reductions for Weak Equivalences[END_REF]. The first three reductions [START_REF] Mateescu | On-the-fly State Space Reductions for Weak Equivalences[END_REF] are applied only if TESTOR detects the presence of τ -transitions in SP.

The determinization produces as output the post function of the IOLTS SP vis , whose states correspond to sets of states of the τ -free IOLTS produced by τ -closure. SP vis is processed by the explorer component, which builds the CTG or the TC by computing the corresponding subgraph whose states are contained in L2A (lead to accept). The reachability of accepting states is determined on the fly by evaluating the PDL [START_REF] Michael | Propositional dynamic logic of regular programs[END_REF] formula ϕ l2a = true * accept on the states visited by the explorer, where the atomic proposition accept denotes the accepting states. This check is done by translating the verification problem into a Boolean equation system (BES) and solving it on the fly using a BES solver component [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF].

On-the-fly test selection algorithm

We describe below the algorithm used by the explorer component to extract the CTG or a (controllable) TC from the SP vis IOLTS on the fly.

Basically, the CTG is the subgraph of SP vis containing all states in L2A, extended with some states denoting verdicts. The accepting states (which are by definition part of L2A) correspond to pass verdicts. For every state q ∈ L2A, the output transitions q !a → q with q ∈ L2A lead to inconclusive verdicts, and the output transitions other than those contained in SP vis lead to fail verdicts. To compute the CTG, the explorer component performs a forward traversal of SP vis and keeps the states q ∈ L2A, which satisfy the formula ϕ l2a . The check q |= ϕ l2a is done by solving the variable X q of the minimal fixed point BES {X q = (q |= accept) ∨ q b →q X q } denoting the interpretation of ϕ l2a on SP vis . The resolution is carried out on the fly using the algorithm for disjunctive BESs proposed in [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF]. If the CTG is not empty (i.e., q SP vis 0 |= ϕ l2a ), then it contains at least one controllable TC [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF].

The extraction of a TC uses a similar forward traversal as for generating the CTG, extended to ensure controllability, i.e., every state q of TC either has only one outgoing input transition q ?a → q with q ∈ L2A, or has all output transitions q !a → q of SP vis with q ∈ L2A. The essential ingredient for selecting the input transitions on the fly is the diagnostic generation for BESs [START_REF] Mateescu | Efficient diagnostic generation for boolean equation systems[END_REF], which provides, in addition to the Boolean value of a variable, also the minimal fragment (w.r.t. inclusion) of the BES illustrating the value of that variable. For a variable X q evaluated to true in the disjunctive BES underlying

ϕ l2a , the diagnostic (witness) is a sequence X q b 1 → X q 1 b 2 → • • • b k → X q k where q k |= accept.

This induces a sequence of transitions q

b 1 → q 1 b 2 → • • • b k → q k in
SP vis leading to an accepting state. Since all states q, q 1 , ..., q k also belong to L2A, this diagnostic sequence is naturally part of the TC under construction.

More precisely, the TC extraction algorithm works as follows. If q SP vis 0 |= ϕ l2a , the diagnostic sequence for q SP vis 0 is inserted in the TC (otherwise the algorithm stops because the CTG is empty). For the TC illustrated on Figure 4.4, this first diagnostic sequence is q 0 ?a → q 1 !y → q 5 ?b → q 9 !z → q 11 . Then, the main loop consists in choosing an unexplored transition of the TC and processing it.

• If it is an input transition q ?a → q , nothing is done, since the target state q ∈ L2A by construction. Furthermore, the presence of this transition in the TC makes its source state q controllable. This is the case, e.g., for the transition q 0 ?a → q 1 in the TC shown on Figure 4.4.

• If it is an output transition q !a → q , each of its neighboring output transitions q !a → q is examined in turn. If the target state q ∈ L2A, the transition is inserted in TC and q is marked with an inconclusive verdict. This is the case, e.g., for the transition q 1 !x → q 4 in the TC on Figure 4.4. If q ∈ L2A, the transition in inserted in the TC, together with the diagnostic sequence produced for q . This is the case, e.g., for the transition q 9 !y → q 5 in the TC on Figure 4.4.

The insertion of a diagnostic sequence in the TC stops when it meets a state q that already belongs to the TC, since by construction the TC already contains a sequence starting at q and leading to an accepting state. This is the case, e.g., for the diagnostic sequence starting at state q 5 in the TC on Figure 4.4. In this way, the TC is built progressively by inserting the diagnostic sequences produced for each of the encountered states in L2A.

During the forward traversal of SP vis , the explorer component continuously interacts with the BES solver, which in turn triggers other forward explorations of SP vis to evaluate ϕ l2a . The repeated invocations of the solver have a cumulated linear complexity in the size of the BES (and hence, the size of SP vis ), because the BES solver keeps its context in memory and does not recompute already solved Boolean variables [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF].

Examples of different ways to express a test purpose

A natural TP for the TLS handshake is to search for a sequence corresponding to the exchange of handshake messages between the client and the server, for instance, the client sends a client hello message. If the server is not satisfied with this request, it responds with a hello retry request, and the client responds with a new client hello message. Finally, if the server is satisfied, it responds with a server hello message. Using the LNT language [GLS17, CCG + 19], one would be tempted to write this TP as the process PURPOSE_A below, simply containing the desired sequence of the four handshake messages (on gates CLIENT_HELLO, HELLO_RETRY_REQUEST, CLIENT_HELLO, and SERVER_HELLO):

process PURPOSE_A [CLIENT_HELLO: CH, HELLO_RETRY_REQUEST: HRR, SERVER_HELLO: SH, T_ACCEPT: none] is CLIENT_HELLO (CTLS12, 28byteRand, T_NULL, {}, T_NULL, {}); HELLO_RETRY_REQUEST (TLS12, TLS_AES_128_GCM_SHA256, {Extension (signature_algorithms, SignatureSchemeList (sas))}); CLIENT_HELLO (CTLS12, 28byteRand, T_NULL, {TLS_AES_128_GCM_SHA256}, T_NULL, {Extension (signature_algorithms, SignatureSchemeList (sas))}); SERVER_HELLO (TLS12, 28byteRand, TLS_AES_128_GCM_SHA256, {Extension (signature_algorithms, SignatureSchemeList (sas))}); loop T_ACCEPT end loop end process Following the conventions of TGV, we mark accepting (respectively, refusal) states by a self-loop labeled with T_ACCEPT (respectively, T_REFUSE).

However, PURPOSE_A is not complete: e.g., initially only one action out of the possible set {CLIENT_HELLO(), HELLO_RETRY_REQUEST (...), SERVER_HELLO (...), ...} is specified.

Thus, when computing the synchronous product with the model, PURPOSE_A is implicitly completed by self-loops labeled with "*" (as explained in Section 2.3.3), yielding a significantly more complex TC than expected. For instance, the implicit *-transition in the initial state allows the tester to perform the sequence "CLIENT_HELLO (...); HELLO_RETRY_REQUEST (...); CLIENT_HELLO (...); HELLO_RETRY_REQUEST (...); CLIENT_HELLO (...); SERVER_HELLO (...)" rather than the expected simple sequence "CLIENT_HELLO (...); HELLO_RETRY_REQUEST (...); CLIENT_HELLO (...); SERVER_HELLO (...)". To force the generation of a TC corresponding to the simple sequence, it is necessary to explicitly complete the TP with transitions to refusal states, as shown by the LNT process PURPOSE_B, where gate OTHERWISE stands for the special label "*": The modular architecture of TESTOR also makes the description of test purposes more convenient, replacing the specific synchronous product of TGV by the LNT parallel compositions and taking advantage of the multiway rendezvous, a powerful primitive to express communication and synchronization among a set of distributed processes. This approach based on the multiway-rendezvous supports data handling, something which is necessary for defining test purposes to validate. Instead of using the dedicated synchronous product, it is also possible to take advantage of the multiway rendezvous [START_REF] Hoare | Communicating Sequential Processes[END_REF][START_REF] Garavel | The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark[END_REF] to compositionally annotate the model, relying on the LNT operational semantics [CCG + 19, Appendix B] to cut undesired branches. For instance, the same effect as the synchronous product with PURPOSE_B can be obtained by skipping the left-most component "synchronous product" of Figure 4.3, i.e., feeding the τ -reduction steps with the IOLTS described by the following LNT parallel composition: This approach based on the multiway rendezvous even supports data handling. For instance, to receive the hello request message (variable H), and to use the information directly in the client hello message (H.cipher_suite and H.extensions), one has just to replace in the above parallel composition the call to PURPOSE_A by a call to the process

Experimental comparison of TESTOR and TGV

TESTOR follows TGV's implementation of the ioco-based testing theory [START_REF] Tretmans | A Formal Approach to Conformance Testing[END_REF][START_REF] Tretmans | Model Based Testing with Labelled Transition Systems[END_REF], using the same IOLTS processing steps, adding only the τ -confluence reduction. For each step, TESTOR uses components developed, tested, and used in other tools for more than a decade. We focus on performance aspects and we compare TESTOR to TGV. For this purpose, we conducted several experiments with models and test purposes, both automatically generated and drawn from academic examples and realistic case studies. In this section we present a summary of the evaluation process and experimentation (more details are available in [START_REF] Marsso | TESTOR: A modular tool for on-the-fly conformance test case generation[END_REF]).

For assessing the correctness of TESTOR, we checked that each TC is included in the CTG, and we compared the TCs and CTGs generated by TESTOR to those generated by TGV. For each pair of model and TP, we measured the runtime and peak memory usage of computing a TC or CTG (using TESTOR and TGV), excluding the fixed cost of compiling the LNT code (model and TP) and generating the executable. The experiments presented in this chapter were carried out using the petitprince cluster located in Luxembourg 3 , each machine of which is equipped with 2 Intel Xeon E5-2630L CPUs, 32GB RAM, and running 64-bit Debian GNU/Linux 8 and CADP 2017-i. Each measurement corresponds to the average of ten executions.

Test Purposes taken from case studies

Table 4.1 summarizes the results for some selected examples. The first two have been kindly provided by Alexander Graf-Brill, and correspond to initial versions of TPs for his EnergyBus model [START_REF] Graf-Brill | A Model-based Certification Framework for the EnergyBus Standard[END_REF]; both aim at exhibiting a particular boot sequence, the second one using REFUSE transitions. The next four examples have been used by STMicroelectronics to verify a cache-coherence protocol [START_REF] Kriouile | Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip[END_REF]. The last three correspond to the three test purposes for an asynchronous implementation of the DES (Data Encryption Standard) [START_REF] Serwe | Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard[END_REF] and check the correctness of a simplified4 version of the asynchronous implementation of the DES (Data Encryption Standard). These examples cover a large spectrum of characteristics: from no τ -transitions (ACE) to huge confluent τ -components (DES), from few visible transitions (DES) to many outgoing visible transitions (Energy-Bus), and a test selection more or less guided via refusal states.

We observe that TESTOR requires less memory than TGV for all examples, but most significantly for the DES. However, although TESTOR is several orders of magnitude slower than TGV for the DES when using the synchronous product (DES TPs without and with REFUSE), TESTOR requires only two seconds to generate a TC or CTG when using an LNT parallel composition with the DES TP with data handling. This is because the LNT parallel composition, handled by the LNT compiler, enables more aggressive optimizations. Thus, using LNT parallel composition to annotate the model's accepting and refusal states is not only more convenient (thanks to the multiway rendezvous) and data aware, but also much more efficient -it is even possible to generate a TC for the original DES model (167 million states, 1.5 billion transitions) in less than 40 minutes.

For the ACE examples, TESTOR is both faster and requires less memory than TGV. This is partly due to an optimization of TESTOR, which deactivates the various reductions of τ -transitions. For a fair comparison, we also run experiments forcing the execution of these reductions. For the extraction of a TC, this increases the execution time by a factor of two and the memory requirements by a factor of three. For the computation of a CTG, this increases the memory requirements by a factor of one and a half, without modifying the execution time significantly.

Automatically generated test purposes

To evaluate the performance, we used a collection of 9791 LTSs with up to 50 million transitions, taken from the non-regression test-base of CADP. For each LTS M of the collection, we automatically generated two TPs: one to test the reachability of an action and another to test the presence of an execution sequence. For the former TP, we sorted the actions of the LTS alphabetically, and checked the reachability of the first action, considering the second half of the action set as inputs. For the latter TP, we used the EXECUTOR tool5 to extract a sequence of up to 1000 visible actions, which we transformed into a TP, considering all actions whose ranking is an odd number as inputs. Technically, this transformation consists in adding to each state of the sequence a self-loop labeled with τ and a *-transition to a refusal state. From the generated pairs (M, TP) we eliminated those for which the automatic generation of a TP failed (for instance, due to special actions that would require particular treatment) and those for which the computation of a TC or CTG took too much time or required too much memory by either TESTOR or TGV. This led to a collection of 13,142 pairs (M, TP) for which both tools could extract a TC. For 12,654 of them, both tools also could compute the CTG.

As for the case studies, we observe that TESTOR and TGV choose different tradeoffs between computation time and memory requirements. On average, TESTOR requires 0.3 times less memory and runs 1.3 (respectively 0.5) times faster to compute a TC (respectively the CTG). When considering only the 1005 pairs with more than 500,000 transitions in the LTS, the average numbers show a larger difference. On average for these larger examples, to compute a CTG, TESTOR requires 1.4 times less memory, but runs 3.5 times longer; to compute a TC, TESTOR requires 2.7 times less memory and runs 0.7 times faster.

Also, while both tools required the exclusion of examples due to excessive runtime, we excluded several examples due to insufficient memory for TGV, but not for TESTOR. Given that TCs are usually much smaller than CTGs, the on-the-fly extraction of a TC by TESTOR is generally faster and consumes less memory than the generation of the CTG. We also observed that the CTGs produced by TESTOR are sometimes smaller than (although strongly bisimilar to) those produced by TGV. While trying to understand these results in more detail, we found examples where each tool is one or two magnitudes faster or memory-efficient than the other.

Indeed, the benefits of the different reductions applied in the tools depend heavily on the characteristics of the example, most notably the sizes of the various subgraphs explored (τ -components, L2A). For instance, when the model M does not contain any τ -transition, there is no point in applying the reductions (τ -compression, τ -confluence, and τ -closure).

Comparison of TESTOR and other MBTs

In the following, we compare TESTOR to the most closely related tools.

TorX [START_REF] Tretmans | TorX: Automated Model-Based Testing[END_REF] and JTorX [START_REF] Belinfante | JTorX: A Tool for On-line Model-driven Test Derivation and Execution[END_REF] are online test generation tools, equipped with a set of adapters to connect the tester to the SUT. The latest versions support test purposes (TPs), but they are used differently than in TESTOR. Indeed, JTorX yields a two-dimensional verdict [START_REF] Belinfante | JTorX: Exploring Model-Based Testing[END_REF]: one dimension is the ioco correctness verdict (pass or fail), and the other dimension is an indication whether the test objective has been reached. This contrasts with TESTOR, which generates test cases (TCs) ensuring by construction that the execution stays inside the lead to accept states (L2A), and stopping the test execution as soon as possible with a verdict: fail if non-conformance has been detected, pass if an accepting state has been reached, or inconclusive if leaving L2A is unavoidable.

Uppaal is a toolbox for the analysis of timed systems, modeled as timed automata extended with data. Three test generation tools exist for Uppaal timed automata. Uppaal-Tron [START_REF] Kim | Testing Real-time Embedded Software Using UPPAAL-TRON: An Industrial Case Study[END_REF] is an online test generation tool, taking as input a specification and an environment model, used to constrain the test generation. Uppaal-Tron is also equipped with a set of adapters to derive and execute the generated tests on the SUT. Contrary to TESTOR, the TCs generated from Uppaal-Tron can be irrelevant, because the generation is not guided by TPs. Uppaal-Cover [START_REF] Hessel | Model-Based Testing of a WAP Gateway: An Industrial Case-Study[END_REF] generates offline a comprehensive test suite from a deterministic Uppaal model and coverage criteria specified by observer automata. Uppaal-Cover attempts to build a small test suite satisfying the coverage criteria, by selecting those TCs satisfying the largest parts of the coverage criteria. In contrast to TESTOR and Uppaal-Tron, Uppaal-Cover generates offline tests. Offline generation does not face the state-space explosion, but also limits the expressiveness of the specification language (e.g., nondeterministic models are not allowed). Uppaal-Yggdrasil [KLN + 15] generates offline test suites for deterministic Uppaal models, using a three-step strategy to achieve good coverage: (i) a set of reachability formulas, (ii) random execution, and (iii) structural coverage of the transitions in the model. The guidance of the test generation by a temporal logic formula is similar to the use of a TP. However, the TPs supported by TESTOR (and TGV) can express more complex properties than reachability, and enable one to control the explored part of the model (using refusal states).

On-the-fly test generation tools also exist for the synchronous dataflow language Lustre [HCRP91], e.g., Lutess [START_REF] Du Bousquet | Lutess: A Specification-Driven Testing Environment for Synchronous Software[END_REF], Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF], and Gatel [START_REF] Marre | Test Sequences Generation from LUSTRE Descriptions: GATeL[END_REF]. Contrary to TESTOR, these tools do not check the ioco relation, but randomly select TCs, satisfying constraints of an environment description and an oracle.

In IOLTS, actions are monolithic, which does not fit for realistic models that involve data handling. STG (Symbolic Test Generator) [START_REF] Clarke | STG: A symbolic test generation tool[END_REF] breaks the monolithic structure of actions, enabling access to the data values, and generates tests on the fly, handling data values symbolically. This enables more user-friendly TPs and more abstract TCs, because not all possible values have to be enumerated. However, the complexity of symbolic com-q 1 q 2 q 5 q 6 q 7 q 8 q 9 q 10 q 11

q 1 q 3 q 4 q 5 q 6 q 7 q 8 INCONC q 0 CH(.

Testing the TLS Handshake Model with TESTOR

We validated our LNT model using TESTOR, taking advantage of its ability to specify data in the test purposes. We defined three test purposes corresponding to three requirements from the draft TLS 1.3 handshake [IET18]:

I. The protocol messages must be sent in the right order, using classical TLS 1.3 order (without hello retry request message).

II. The handshake must be aborted with an "unexpected message" alert, if there is a client renegotiation.

III. The protocol messages are sent in the right order with an incorrect key shared (with hello retry request message).

q 2 q 3 q 4 q 5 q 7 q 9 q 6 q 1 q 8 q 10 q 12 q 11 q 0 During this validation process we found an error in our model, with test purpose III. We couldn't reach the accepting state of this test purpose, because of our initial implementation of this requirement: "The server hello message should have the same cryptographic information as the hello retry request message." In fact, we were assigning to the hello retry request encryption data the value of the server hello encryption data, whereas the hello retry request message arrives before the server hello message. We changed our model to correct this issue.

INCONC

We illustrated the formalization and the functional testing of a communication protocol, through a case study of the TLS handshake 1.3. We presented TESTOR, a new tool for on-the-fly conformance test case generation for asynchronous concurrent systems. Like the existing tool TGV, TESTOR was developed on top of the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] and brings several enhancements: online testing by generating (controllable) test cases completely on the fly; a more versatile description of test purposes using the LNT language; and a modular architecture involving generic graph manipulation components from the OPEN/CAESAR environment [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF]. The modularity of TESTOR simplifies maintenance and fine-tuning of graph manipulation components, e.g., by adding or removing on-the-fly reductions, or by replacing the synchronous product. Besides the ability to perform online testing, the on-the-fly test selection algorithm sometimes makes possible the extraction of test cases even when the generation of the complete test graph (CTG) is infeasible. The experiments we carried out on ten-thousands of benchmark examples and three industrial case studies show that TESTOR consumes less memory than TGV, which in turn is sometimes faster, for generating CTGs.

A combination of this conformance test case generation tool and the synchronous testing techniques presented in Chapter 3 is therefore beneficial for testing GALS systems, as it will be illustrated in Chapter 5.

Chapter 5

Validation of GALS Systems

In this chapter we illustrate formal techniques for GALS systems, using a simple, but relevant example, namely an autonomous car, which has to reach a destination, following roads on a geographical map, in the presence of moving obstacles. The car is modeled as a GALS system, comprising synchronous components for perception, decision, and action. Part of this work has been published in [START_REF] Marsso | Asynchronous testing of synchronous components in GALS systems[END_REF].

This chapter is organized as follows. Section 5.1 presents the car example. Section 5.2 introduces the formal GRL model of an autonomous car. Section 5.3 describes the application of model checking for asynchronous systems to the overall GALS system. Section 5.4 experiments manually the functional testing of synchronous components. Section 5.5 presents the integration of asynchronous conformance testing with automated synchronous testing to improve the latter. Finally, we give concluding remarks on our work and synchronous testing.

GALS Example: An Autonomous Car

To illustrate our approach, we consider the behavioral model of a (simplified) autonomous car interacting with its environment. The environment consists of a geographical map shared by the car and a given set of moving obstacles (pedestrians, cyclists, other cars, etc.). For instance, the autonomous car and a pedestrian could share the streets of Manchester as it is shown in Figure 5.2. To limit the complexity, each obstacle executes a fixed number of random or statically chosen movements.

The autonomous car shown in Figure 5.1, itself consists of four synchronous components:

(i) a GPS keeps the car position updated, (ii) a radar detects the presence of the obstacles close to the car and builds a perception grid summarizing information about perceived obstacles, (iv) an action controller commands the engine and direction to follow the itinerary computed by the decision controller, using the perception grid built by the radar to avoid collisions.

These four components communicate in various ways:

• the GPS sends the current position to the decision controller upon request,

• the radar periodically sends the perception grid to the action controller, and

• the action controller requests a new itinerary from the decision controller.

This example is simple, but relevant, because it is representative of a GALS system, with synchronous components (e.g., radar, action controller) interacting with each other, the whole GALS system (e.g., autonomous car) being constrained by a realistic environment (e.g., geographical map and obstacles).

GRL Model of the GALS System

GRL (GALS Representation Language) [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF] is a formal language designed to model GALS systems (more details about GRL are available in Chapter 2 Section 2.4.1). We decided to take advantage of the GRL2LNT [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF] translator to LNT [START_REF] Garavel | From LOTOS to LNT[END_REF], which provides a connection to the CADP verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. The whole GRL model of the car is presented in the Appendix B. each of which is represented in GRL as a medium, depicted as a (pink) ellipse with dashed border in Figure 5.3. The interaction between blocks also respects environmental constraints (MAP_MANAGEMENT), each one being represented in GRL as an environment, depicted as a (light pink) ellipse with thick dashed border in Figure 5.3. The overall model of the GALS is represented in GRL as a system, which describes the composition and interactions of blocks, media, and environments. In the sequel, we present excerpts of a block, a medium, an environment, and the system of our GRL model (1189 lines).1

The geographical map is represented as a directed graph as illustrated in Figure 5.4, in which edges correspond to streets and nodes correspond to crossroads; for simplicity, we assume that the car or an obstacle occupies a street completely (a longer street can be represented by several edges in the graph). A set of functions is defined to explore this graph, to compute itineraries, etc. For instance, the following LNT constant initial_map returns the graph corresponding to the map shown in Figure 5.4. A GRL block defines the deterministic code executed at each activation (i.e., clock instant) by the synchronous component. For instance, the radar of our autonomous car is modeled by the GRL block RADAR, which has a static variable previous_grid to keep track of the perception grid computed during the previous activation. This grid is considered to be initially empty (i.e., it has the value Grid (NIL)). At each activation, the radar receives the current positions of the car and all the obstacles as input from the environment (in parameter POSITIONS).2 It then computes the current perception grid indicating, for each possible direction the car might take, whether at least radar_visibility steps are free of any obstacle. If there is a change between previous_grid and grid, both the variable previous_grid and the output CURRENT are updated; otherwise the output is set to the particular value already_sent indicating that the grid did not change. At the end of the activation, the computed grid is sent to the connected medium (send parameter CURRENT). Synchronous blocks interact with each other via asynchronous communication media. Explicitly representing these media makes it possible to finely model a large panel of behaviors (i.e., message buffering, message loss, nondeterminism, etc.). A medium is connected to each block by at most two channels, called receive and send channels. Note that a receive channel corresponds to the reception of some value in a variable prefixed by "?". Each channel has an associated Boolean condition (tested with a when clause), stating whether a message is available. For instance, the following GRL medium CURRENT_GRID enables the block RADAR to send the current perception grid (via the receive channel SEND_CURRENT_GRID) to the block ACTION (via the send channel RECEIVE_CURRENT_GRID); the transmission takes place only when the perception grid has not already been sent. Environments provide blocks with inputs and receive their outputs. Block activations are particular inputs, enabling an environment to precisely control the activations of synchronous blocks. For instance, the following fragment of the GRL environment MAP_MANAGEMENT ensures that: (1) the geographical map information, such as the position of the car (map.c) and obstacles (grid), is shared with the block RADAR (by sending this information to RADAR as input POSITIONS); (2) the geographical map information is updated when the car or the obstacles move (by receiving these moves from blocks ACTION and RADAR as outputs CAR_MOVE and OBSTACLE_MOVE, respectively); and (3) the blocks are only activated as long as the car did neither arrive at destination, nor crashed. Note that an environment may be nondeterministic, e.g., it may contain nondeterministic choice, modelled in GRL using the select statement. The following GRL system describes the composition of the complete model of the autonomous car, i.e., the blocks RADAR and ACTION, the medium CURRENT_GRID, and the environment When considering a complete GALS system from the outside, all parts based on the synchronous programming paradigm are hidden. Thus, the overall GALS system is amenable to classic analysis techniques developed for asynchronous systems.

Model Checking of the GALS Behavior

Using GRL2LNT [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF] and CADP, for a geographical map (with 22 streets and 8 crossroads) and two obstacles, each with a first random movement and a second statically chosen movement, we generated (in about 12 minutes on a standard laptop) the LTS corresponding to our GRL autonomous car model (952, 759 states and 1, 518, 227 transitions after strong bisimulation minimization). We first validated our GRL model by checking several safety and liveness properties3 characterizing the correct behavior of the autonomous car. We expressed the properties in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF], which is the datahandling, action-based, branching-time temporal logic of the on-the-fly model checker of CADP (more details about MCL are available in Section 2.3.2). We describe here the properties in natural language and in MCL.

• The position of the car is correctly updated after any movement of the car. This safety property specifies that on all transition sequences, an update of the car position (action "UPDATE_POSITION ?current_street", where current_street is the street on which the car is) followed by a car movement (action "CAR_MOVE ?control", where control is a movement command) cannot be followed by an update of the car position inconsistent with current_street, control, and the map. This can be expressed in MCL using the necessity modality below, which forbids the transition sequences containing inconsistent position updates: The values of the current position, the movement, and the new position of the car present on the actions UPDATE_POSITION and CAR_MOVE are captured in the variables current_street, control, and new_street of the corresponding action predicates (surrounded by curly braces) and reused in the where clause of the last action predicate. The predicate Consistent_Move defines all valid combinations for current_street, control, and new_street allowed by the map.

[
• A same message from one of the autonomous car components must be considered only once. For instance, the radar should not send twice the same perception grid, i.e., two successive occurrences of action SEND_CURRENT_GRID must carry different values of the grid, reflecting the changes in perception due to obstacle or car movements. This can be expressed by four properties in MCL, one for a SEND_CURRENT_GRID with no perceivable obstacles, with one perceivable obstacle, with two perceivable obstacles, and with no updated information (might be repeated). For simplicity, we only give and comment the MCL code of the two perceivable obstacles to illustrate the flavor. 1 This can be expressed in MCL using the necessity modality below, which forbids the transition sequences containing twice the same values for the radar outputs. • Inevitably (by avoiding the non-progressing iterations of synchronous blocks), the system should reach a state where either the car arrived (ARRIVED), or a collision occurred between the car and an obstacle (COLLISION), or all obstacles have finished their list of movements (END_OBSTACLE). This can be expressed in MCL using the inevitability modality below, which forbids the infinite transition sequences avoiding the non-progressing iterations of synchronous blocks (NO_UPDATE) and not leading to one of the three terminal actions (TERMINATE).

not <(not TERMINATE)*> <(not TERMINATE) and (not NO_UPDATE)>@ ;

The predicate TERMINATE defines all valid actions allowed by the map (ARRIVED, COLLISION, and END_OBSTACLE) and the predicate NO_UPDATE defines all repeated actions of a block.

We believe that the two last properties are to all GALS systems, because a GALS system contains non-progressing iterations of its synchronous components. Therefore, it is necessary to identify these non-progressing iterations and to verify that the system reaches the terminal states by avoiding these iterations.

Manual Testing of a Synchronous Component

We use the Lurette testing tool 4 [JRB06] to test an implementation of a radar in the C language 5 , which might be a part of an implementation of our GALS autonomous car example described in Section 5.2. Usually, a radar builds an occupancy grid with respect to its position (this grid reflects the visibility of the radar); in an autonomous car, the position of the radar is the position of the car. To simplify, in our example the radar takes as input the position of the car and the obstacles (provided by the GRL environment on channel POSITIONS) and outputs the perception grid (sent to the medium CURRENT_GRID).

In the C radar implementation, the street names of the geographical map presented in Section 5.2 are represented by natural numbers, because the input language of Lutin (the Lurette component for defining test scenarios) supports only Boolean and numerical types. Figure 5.5 gives an overview of this encoding of the geographical map.

As in Section 5.2, we consider a fixed instance, here with two obstacles (called leo and lilly). Testing the synchronous radar component consists in providing a sequence of inputs and observing the generated sequence of outputs. Each of the radar's inputs (position of the car and the obstacles) can take one out of the 21 streets of the map, yielding 21 3 possible inputs. Fortunately, not all sequences of these inputs are realistic, because the car is not flying and has to respect the constraints of the map and by being fixed on the car, the possible inputs taken by the radar are also constrained by the possible movements 4 More details about the Lurette tool are available in Section 2.2.3 5 The radar implementation in C was generated from a Lustre program The input constraints for the radar should enforce that the positions of the car and the obstacles evolve in a realistic manner, i.e., respecting the map. The following Lutin code corresponds to a simple scenario defined by the automaton in Figure 5.6, where the car starts on street 9 and possibly moves to street 12, and lilly (respectively, leo) appears on street 5 (respectively, street 14) and moves back and forth to street 12 (respectively, street 11). The scenario automaton enables to constrain the test inputs generation to those possible in the physical environment (geographical map, and possible movements of the car and obstacles). Each state of the automaton contains a tuple with the three radar inputs values (car, leo, and lilly), the value "2000" indicating that the obstacles are absent. This scenario can be described by an automaton with five states and seven transitions; the corresponding constraints on the inputs of the radar can be encoded in Lutin as a node input_constraints with four outputs (the three inputs of the radar plus the state s of the automaton). Although simple, the scenario covers the appearance and movement of obstacles, and the case where the perception grid should remain unchanged. Although larger and more complex scenarios can be written manually, this task is tedious and error-prone, in particular due to the representation of street names by natural numbers (the input language of Lutin supports only Boolean and numerical types), and may easily introduce redundant definitions or equivalent states.

A small example of an oracle for the previous scenario is given by the following Lustre node oracle, describing the expected output (perception grid) for each given input vector (the positions of the car and obstacles). As the Lutin node, the oracle takes, besides the inputs and outputs of the radar, as input also the state s to keep track of the evolution (according to the same small automaton shown in Figure 5.6). The oracle outputs the verdict res, i.e., whether the observed outputs are those expected for the state and the inputs. For instance, in state 3, lilly (in street 12) and leo (in street 11) should both be detected by the car (in street 9), whereas they should not be detected in the initial state. The oracle also computes two coverage variables pass and blocked: the former measures the coverage of state 2 (representing the situation where the car arrives at destination and all obstacles appeared), and the latter measures the coverage of the situation where the car is blocked by the obstacles. mainly due to the dependency on the map and the necessity to enumerate all possible movements. For instance, to detect the already_sent, one should manually follow the scenario's evolution. Because one can easily forget some cases, an automated generation of these input constraints and the oracle is more convenient, as we illustrate in the next section.

Test Projection and Exploration

Each synchronous component of a GALS system is constrained by the other synchronous components, communication media, and environments present in the system. In this section we propose an approach that explicitly exploits these constraints to improve the unit testing of a synchronous component taken separately.

The idea is to automatically derive inputs for synchronous testing tools by projecting the complete test graph generated for the entire GALS system on the inputs and outputs of the synchronous component. In this way, the inputs provided to the synchronous component are realistic and relevant, because they are chosen according to possible execution scenarios of the overall GALS system. Furthermore, the synchronous tests generated in this way contain all possible inputs leading to the goals of test purposes (e.g., a possible input leading to collision in the case of T 1, see Figure 5.8).

Figure 5.7 gives an overview of the approach. In a first step, a complete test graph for the overall GALS system is projected on the synchronous component C to be tested, resulting in a test graph for C. In a second step, this test graph is translated and renamed to be compatible with the synchronous testing tool Lurette. In the last step, the test graph is explored (using XTL [MG98] scripts), generating the input constraints and the oracle for testing C separately. In the remainder of this section, we present the approach in more detail, illustrating how it improves the testing of the radar of our autonomous car example.

Test graph projection

Projecting a complete test graph CTG on a synchronous component C consists in hiding all transitions labeled with an action that is neither an input nor an output of C, and reducing The reduction removes all internal transitions (created by the hiding), so that all actions of CTG C are either an input or an output of C. A precondition for a successful projection is that all inputs and outputs of C, as well as the verdict transitions, are present and visible in CTG.

COLLISION q 0 q 1 ACCEPT * q 2 Figure 5
For the GRL model of the autonomous car (see Section 5.2), the only controllable inputs are the movements of obstacles; the observable outputs make it possible to study the behavior of the car. An example test purpose (T 1) is to specify the situation where a collision occurs between a car and an obstacle. The test purpose is expressed as an LTS (in the AUT format) and shown in Figure 5.8, where a transition representing the collision (action COLLISION) should lead to a goal state, i.e., having an outgoing transition labelled by an ACCEPT action.

We also defined four other test purposes (T 2, T 3, T 4, and T 5) constraining the car and obstacles interaction on the map. For these test purposes, TESTOR generates the complete test graphs in less than a minute (see Table 5.1).

More particularly, the radar takes as input the positions of the car and of the obstacles. The positions of the obstacles are also a controllable input of the overall GALS system. But the position of the car is computed by the scenario depending on the output of another synchronous component, namely the action controller. The output of the radar is the perception grid, which is, inside the GALS system, sent to the action controller. Hiding, in the complete test graph CTG, all transitions but those corresponding to these inputs and outputs, and reducing the result with respect to weak trace equivalence yields the LTS CTG RADAR . Columns 2 & 3 of Table 5.2 give the number of states and transitions of CTG RADAR for the five test purposes considered.

Translating and renaming

Because some of the data types used in the GALS model might not be exactly the same as those supported by the synchronous testing tools, a preliminary step is the conversion of the values present on the transition labels of CTG C , for instance by applying appropriate renaming rules. Null values have been added, in order to transform non scalar data on transitions into variable names and value tuples of constant length.

We defined a generic format for the exploration tools to work properly. Each input transition is renamed into

"INPUT !s 1 !v 1 ... !s m !v m "
, where s i is the name of the input variable and v i its value; each output transition is similarly renamed into "OUTPUT !s 1 !v 1 ... !s n !v n ". For instance, the projected complete test graph CTG RADAR contains non-scalar data structures, in particular, the perception grid computed by the radar is represented as a list and streets are identified by their names (i.e., character strings). To be usable with the synchronous test generator Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF], these lists need to be transformed into tuples of constant length, and the street names need to be translated into the corresponding (numeric) constants.

Test graph exploration

By construction, the projected CTG C is an LTS describing the interaction with the SUT, and as such contains both, the sequence of inputs for the SUT and the verdict concerning the test outcome (i.e., the test oracle). Because the test inputs and oracle should be provided to Lurette using two different languages (Lutin for the input constraints and Lustre for the oracle), two explorations of (the renamed) CTG C are required.

The generation of input constraints

The input constraints are generated by encoding CTG C as a possibly nondeterministic node in Lutin with the XTL 6 [MG98] script extract constraints (87 lines). The whole XTL script extract constraints is presented in the Appendix C.1. This node has the same inputs as C and an additional input variable s corresponding to the current state of CTG C , initialized to the initial state. The main loop of the node contains a nondeterministic choice, with a branch for each transition in CTG C . A branch corresponding to a transition T is executed if s is equal to the source state of T , and as result of execution it sets s to the target state of T . A branch for an output transition specifies that the inputs are kept unchanged, which corresponds to the behavior expected for the special output transition δ on quiescent states. A branch for an input transition updates the corresponding inputs. A branch for a verdict transition, instead of looping on the same verdict state of the CTG C (pass and inconclusive), sets the variable s to the initial state of the CTG, thus enabling to not generate the same inputs as a self-loop would do and to cover faster the whole CTG when a verdict is reached. Thus, the Lutin node describes exactly the set of input sequences contained in CTG C .

An excerpt of the second step of the script extract constraints is given by the following XTL code, illustrating the CTG encoding into the nondeterministic node in Lutin. In the first step of the script, the names of the inputs (stored in the variables iv1, iv2, iv3)

and their initial values are extracted. Then we explore all transitions of the CTG (<|fby on e:edge |>(...)), and first extract and print the source state (s) of the transition, then match, extract and print the new input values (p2, p4, p6) through the print info function for the input transition (INPUTS ?...), or match and print unchanged input values using the memory Lustre operator (pre)7 for output transitions. Finally, we print the target states (target (e)) for all other transitions except the verdict transitions (INCONCLUSIVE and PASS), where the target state is replaced by the state -1, which corresponds to an intermediary state where the values are reset to the initial ones and leading to the initial state.

<| fby on e:edge |> ( printf (" | pre s = ") fby print (source (e)) fby if (e -> [ INPUTS ?p1:raw ?p2:natural ?p3:raw ?p4:natural ?p5:raw ?p6: natural ]) then ( * car movement; obstacles do not move * ) print info (p1, p3, p5, p2, p4, p6) else ( * output or verdict transition: keep inputs unchanged * ) printf (" and ") fby print (iv1) fby printf (" = pre ") fby print (iv1) fby printf (" and ") fby print (iv2) fby printf (" = pre ") fby print (iv2) fby printf (" and ") fby print (iv3) fby printf (" = pre ") fby print (iv3) end if fby ( * change s to the target state * ) printf (" and s = ") fby if e -> [INCONCLUSIVE] or e -> [PASS] then printf ("-1") else print (target (e)) end if fby printf ("\n") ) fby

An input of the radar is a new position of the car and the obstacles (lilly and leo). Because the exploration takes into account all transitions of CTG RADAR , the generated Lutin node incorporates all evolution of the car and the obstacles that are relevant for the considered test purpose. The generated Lutin nodes are quite long (see Table 5.2) and complex, because they contain nondeterministic choices, induced by the random movements of the obstacles. Note that the generated Lutin node corresponds to a specific automatically generated automaton scenario (cf. Section 5.4). Writing similar Lutin nodes by hand would probably have been difficult and error-prone.

The generation of oracles

Because a synchronous block C is executed atomically, i.e., not interleaved with other synchronous components, a sequence of input transitions for C is immediately followed by the expected sequence of output transitions. Because the target state s of the last transition in such a sequence of inputs is also the source state of the first transition in the sequence of outputs, we call such a state s a corner state. For the radar, the sequence of input transitions corresponding to new positions of the car or the obstacles is followed by an output transition corresponding to the expected perception grid. The oracle is generated with the XTL script extract oracle (263 lines), by encoding CTG C as a deterministic node in Lustre, which, to each corner state and its set of inputs/outputs, associates a Boolean verdict, indicating whether the outputs are the expected ones. The whole XTL script extract oracle is presented in the Appendix C.2. An excerpt of the script extract oracle is given by the following XTL code describing the rules of extraction for corner states. In this code for each corner state s, we iterate over pairs of an input and an output transition, assign the input values (i1, i2, i3), to the accumulator (a i1, a i2, a i3) and print them with the source state (s) and the output values (o1, o2) through the print corner function. The oracle node is also defined for the verdict states of CTG C . For a pass (respectively, fail ) verdict it always returns true (respectively, false). For an inconclusive verdict it returns true iff the outputs are unchanged; this matches the generation of the input constraints. In order to observe the coverage of the generated tests, for each verdict state (pass and inconclusive) and each other state of the CTG C , a coverage variable is introduced in the Lustre node generated for the oracle. These coverage variables are true if at least one of the executions passed by the corresponding state of CTG C (see Section 5.4). node oracle (s, car, lilly, leo, perception_leo, perception_lilly: int) returns (res, pass, inconclusive, s0, ... s86: bool); let res = true -> ( if s = 6 then (car = 11 and lilly = 13 and leo = 6 and perception_lilly = 13 and perception_leo = 2000) ... ); pass = false -> if s = 83 then true else pre pass; inconclusive = false -> if s = 7 then true else pre inconclusive; s0 = false -> if s = 0 then true else pre s0; ... s86 = false -> if s = 86 then true else pre s86; ... The generated oracles are quite long (see Table 5.2) and complex, because they contain all oracle verdicts and coverage criteria. For each of the five test purposes, we executed the generated scenarios on the radar SUT using Lurette (the last columns of Table 5.2 indicate the overall time and memory consumed by the overall testing process). This enabled us to discover (and fix) a mistake in the SUT related to the incorrect management of the special value already sent. We presented an automatic approach (see Figure 5.9) integrating both asynchronous and synchronous testing tools to derive complex, but relevant unit test cases for the synchronous components of a GALS system. From a formal model of the system in GRL [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF] and a test purpose, the conformance testing tool TESTOR [START_REF] Marsso | TESTOR: A modular tool for on-the-fly conformance test case generation[END_REF] automatically generates a complete test graph [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF] capturing the asynchronous behavior of the system relevant to the test purpose. Such a complete test graph is then projected on a synchronous component C and explored using XTL [START_REF] Mateescu | XTL: A Meta-Language and Tool for Temporal Logic Model-Checking[END_REF] scripts to provide a synchronous test scenario (input constraints in Lutin [START_REF] Raymond | Lutin: a language for specifying and executing reactive scenarios[END_REF] and an oracle in Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF]) required to test C with the Lurette tool [START_REF] Jahier | Case studies with Lurette V2[END_REF]. We automated all these steps using an SVL [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] script. The approach substantially relieves the burden of handcrafting these test scenarios, because, by construction, the derived scenarios constrain the inputs provided to C to relevant values, covering a test purpose, which might arise during the execution of the GALS system. We illustrated the approach on an autonomous car example. This work also enabled us to observe two common properties of GALS systems, more precisely that it is necessary to identify the non-progressing iterations of GALS's synchronous components and verify that the system reaches the terminal states by avoiding these iterations.

Chapter 6 Conclusion

GALS (Globally Asynchronous, Locally Synchronous) [START_REF] Daniel | Globally-Asynchronous Locally-Synchronous Systems[END_REF] systems consist of multiple synchronous components that execute independently and interact with each other. They are intrinsically complex, often critical, and nowadays become increasingly large and distributed. The simultaneous presence of synchronous and asynchronous aspects makes their development and debugging difficult. Hence, to ensure their functional correctness and reliability, it is required to use a rigorous testing process based on formal methods, such as model-based testing [BJK + 05], a validation technique taking advantage of a model of a system (both, requirements and behavior) to automate the generation of relevant test cases. In this dissertation, we have explored different ways to carry out the model-based testing of GALS systems. In particular, we have presented testing techniques for synchronous components, for communication protocols between components, and how to combine these two techniques for testing complete GALS systems.

Synchronous formal techniques for the functional testing of components

In the first part of this dissertation, we explored formal techniques for the functional testing of synchronous components. As a case-study, we reconsidered the Message Authenticator Algorithm (MAA), a pioneering cryptographic function designed in the mid-80s, and we formalized it as a synchronous dataflow algorithm in the synchronous language Lustre [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF]. A large part of our Lustre model contains general definitions, half of which are largely independent of the MAA. To validate our Lustre model, we defined sets of test vectors derived from the specification in [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF]. We automated the test execution process, by using the test generation tool Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF] of the Lustre V6 toolbox 1 [HCRP91, RRJ08]. The modeling and validation of the MAA enabled us to discover various mistakes in prior (informal and formal) specifications of the MAA, the test vectors and code of the ISO 1990 [ISO90, Annex E], and the ISO 1992 [ISO92, Annex A] standards, in the main program (implementation of the MAA in C) provided by [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF], and in some of the compilers and verification tools that we used. Testing our Lustre MAA model was a tedious task: in order to automate the tests validation with a Lutin environment and an oracle, we had to define more than 400 constants. An automation of this testing process is therefore highly beneficial.

Asynchronous conformance testing techniques for a communication protocol

Then, we explored the formalization and the functional testing of a communication protocol between two (synchronous) components. For this purpose, we introduced TESTOR [START_REF] Marsso | TESTOR: A modular tool for on-the-fly conformance test case generation[END_REF], a new tool for on-the-fly conformance test case generation for asynchronous concurrent systems. TESTOR explores the model and generates automatically a set of test cases or a CTG (Complete Test Graph) to be executed on a physical implementation of the system. Like the existing tool TGV [START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF], TESTOR was developed on top of the CADP2 toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] and brings several enhancements: online testing by generating (controllable) test cases completely on the fly; a more versatile description of test purposes using the LNT language; and a modular architecture involving generic graph manipulation components from the OPEN/CAESAR environment [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF]. The modularity of TESTOR simplifies maintenance and fine-tuning of graph manipulation components, e.g., by adding or removing on-the-fly reductions, or by replacing the synchronous product between the model and the test purpose. Besides the ability to perform online testing, the on-the-fly test selection algorithm sometimes makes possible the extraction of test cases even when the generation of the CTG is infeasible. The experiments we carried out on tenthousands of benchmark examples and three industrial case studies show that TESTOR consumes less memory than TGV for generating CTGs. As a case-study, we reconsider the formalization of the Transport Layer Security (TLS) 1.3 handshake, a protocol responsible for the authentication and exchange of keys necessary to establish or resume a secure communication. Taking the draft specification of the TLS [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF] protocol Version 1.3 as starting point, we formalized the TLS handshake protocol in the LNT language [GLS17, CCG + 19]. Our LNT model of TLS 1.3 handshake has been validated against a concrete implementation of TLS by an approach using TESTOR [START_REF] Bozic | A formal TLS handshake model in LNT[END_REF]. The validation process enabled us to find an ambiguity in the specification of the draft TLS 1.3 handshake [START_REF] Van De Pol | The transport layer security (tls) protocol version 1.4[END_REF].

Combined synchronous and asynchronous testing techniques for GALS systems

Finally, we proposed a combination of conformance test generation and synchronous testing techniques that cumulates their benefits for testing a complete GALS system. We presented an automatic approach combining both techniques, to minimize the handwriting test effort while maximizing the coverage. Our methodology integrates: (1) synchronous and asynchronous concurrent models, (2) functional unit testing and behavioral conformance testing, and (3) various formal methods and their supporting tools. First, the GALS system is modelled in GRL (GALS Representation Language) [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF][START_REF] Jebali | Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems[END_REF], a formal language designed for describing GALS systems. The asynchronous aspects of the GRL model can be validated using CADP, e.g., by checking temporal logic formulas expressing desired (global) correctness properties. Next, from the formal model of the system in GRL and a test purpose, the TESTOR tool can be used to automatically generate CTGs, capturing the asynchronous behavior of the system relevant to the test purpose, which can be used to assess whether an actual implementation of the GALS system conforms to the GRL model. Then, the CTG is projected on a synchronous component C and subsequently translated automatically, using XTL [START_REF] Mateescu | XTL: A Meta-Language and Tool for Temporal Logic Model-Checking[END_REF] scripts, into a scenario (i.e., input constraints in Lutin [START_REF] Raymond | Lutin: a language for specifying and executing reactive scenarios[END_REF] and an oracle in Lustre), required to automate the testing of C using the synchronous test generation tool Lurette. Because these scenarios are automatically generated from the GRL model of the GALS system, they correspond by construction to relevant (and often complex) executions of the synchronous component. The whole methodology has been automated using SVL [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] scripts. The approach substantially relieves the burden of handcrafting these test scenarios, because, by construction, the derived scenarios constrain the inputs provided to C to relevant values, covering a high-level test purpose, which might arise during the execution of the GALS system. We illustrated the approach on an autonomous car example.

Perspectives

As future work, we plan to consider the behavioral coverage of GALS systems, which can be achieved by identifying a set of test purposes (ideally as small as possible) whose corresponding CTGs cover the whole state space of a GALS system. The set of test purposes could be built by deriving them from the action-based, branching-time temporal properties of the model (following the results of [FFJ + 12] in the state-based, linear-time setting) or by synthesizing them according to behavioral coverage criteria. Furthermore, we also plan to consider the transition coverage of a CTG, which can be achieved by identifying a set of test cases (ideally as small as possible) covering all states and transitions of a CTG. The difficulty is to find a simple solution, which extracts automatically controllable test cases (TCs) from an acyclic CTG, and which can cover the CTG using as few TCs as possible. This could be done by invoking the TESTOR algorithm repeatedly on the CTG itself, and by ensuring that the generated TCs have covered all CTG transitions, by taking into account also the transitions looping in the cycles possibly requiring unfolding of some cycles. The extraction strategy has to be studied and finely-tuned experimentally.

Finally, to execute a generated TC against a system under test (SUT), it is necessary to refine the TC to take into account the asynchronous communication between the SUT and the tester. Actually, the SUT accepts every input at any time, whereas the TC is deterministic, i.e., there is no choice between an input and an output. An approach for connecting a TC (randomly selected) and an asynchronous SUT was defined in [START_REF] Weiglhofer | Asynchronous Input-Output Conformance Testing[END_REF]. A similar approach using test purposes (TPs) to guide the test generation was proposed in [START_REF] Bhateja | A TGV-like Approach for Asynchronous Testing[END_REF] and subsequently extended to timed automata [START_REF] Bhateja | Asynchronous testing of real-time systems[END_REF]. Recently, this kind of connection was automated by the MOTEST tool [START_REF] Graf | Model-Based Testing for Asynchronous Systems[END_REF]. It would be interesting to investigate how these solutions could be integrated into our methodology to automate the execution of TCs on asynchronous SUTs, and to experiment it on a real GALS system.

- ---------------------------------------- ----------------------------------------- ------------------------------------------A.2 Definitions for Type Byte

We define bytes (octets) using a structure Octet that contains the eight bits of a byte, together with functions implementing bitwise logical operations, left-shift and right-shift operations on bytes, as well as all byte constants needed to formally describe the MAA and its test vectors. ---------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- -----------------------------------------

A.3 Definitions for Type OctetSum

We define type OctetSum that stores the result of the addition of two octets. Values of this type are 9-bit words, made up using the structure OctetSum that gathers one bit for the carry and an octet for the sum. The two principal functions for this type are addOctetSum (which adds two octets and an input carry bit, and returns both an output carry bit and an 8-bit sum), and addOctet (which is derived from the former one by dropping the input and output carry bits); the other functions are auxiliary functions implementing an 8-bit adder.

type OctetSum = struct {x: Bit; o: Octet}; ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ------------------------------------------A.4 Definitions for Type Half

We define 16-bit words ("named half words") using a structure Half that contains two bytes corresponding to a half word, together with two usual constants, and a function implementing operation mulOctet that takes two octets and computes their 16-bit product; the other functions are auxiliary functions implementing an 8-bit multiplier.

type Half = struct {o1: Octet; o2: Octet}; ----------------------------------------- ---------------------------------------- ----------------------------------------- ------------------------------------------A.5 Definitions for Type HalfSum

We define type HalfSum that stores the result of the addition of two half words. Values of this type are 17-bit words, made up using the constructor buildHalfSum that gathers one bit for the carry and a half word for the sum. The five principal non-constructors for this type are eqHalfSum (which tests equality), addHalfSum (which adds two half words and returns both a carry bit and a 16-bit sum), addHalf (which is derived from the former one by dropping the carry bit), addHalfOctet and addHalfOctets (which are similar to the former one but take byte arguments that are converted to half words before summation); the other non-constructors are auxiliary functions implementing a 16-bit adder built using two 8-bit adders.

type HalfSum = struct {x: Bit; h: Half}; ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ------------------------------------------A.6 Definitions for Type Block

We define 32-bit words (named "blocks" according to the MAA terminology) using a constructor buildBlock that takes four bytes and returns a block. The seven principal non-constructors for this type are eqBlock (which tests equality), andBlock, orBlock, and xorBlock (which implement bitwise logical operations on blocks), HalfU and HalfL (which decompose a block into two half words), and mulHalf (which takes two half words and computes their 32-bit product); the other non-constructors are auxiliary functions implementing a 16-bit multiplier built using four 8-bit multipliers, as well as all block constants needed to formally describe the MAA and its test vectors.

type Block = struct {o1: Octet; o2: Octet; o3: Octet; o4: Octet}; ----------------------------------------- ----------------------------------------function andBlock (w1, w2: Block) returns (w: Block); let w = Block {o1 = andOctet (w1.o1, w2.o1); o2 = andOctet (w1.o2, w2.o2); o3 = andOctet (w1.o3, w2.o3); o4 = andOctet (w1.o4, w2.o4)}; tel; -----------------------------------------function orBlock (w1, w2: Block) returns (w: Block); let w = Block {o1 = orOctet (w1.o1, w2.o1); o2 = orOctet (w1.o2, w2.o2); o3 = orOctet (w1.o3, w2.o3); o4 = orOctet (w1.o4, w2.o4)}; tel; ----------------------------------------- -----------------------------------------function HalfU (w: Block) returns (o1o2: Half); let o1o2 = Half {o1 = w.o1; o2 = w.o2}; tel; -----------------------------------------function HalfL (w: Block) returns (o3o4: Half); let o3o4 = Half {o1 = w.o3; o2 = w.o4}; tel; -----------------------------------------function mulHalf (h1, h2: Half) returns (w: Block); var h3, h4, h5, h6, h7, h8, h9: Half; let h3 = mulOctet (h1.o1, h2.o1); h4 = mulOctet (h1.o1, h2.o2); h5 = mulOctet (h1.o2, h2.o1); h6 = mulOctet (h1.o2, h2.o2); h7 = addHalfOctet (h4.o2, addHalfOctets (h5.o2, h6.o1)); h8 = addHalfOctet (h7.o1, addHalfOctet (h3.o2, addHalfOctets (h4.o1, h5.o1))); h9 = addHalfOctets (h8.o1, h3.o1); w = Block {o1 = h9.o2; o2 = h8.o2; o3 = h7.o2; o4 = h6.o2}; tel; ------------------------------------------

A.7 Definitions for Type BlockSum

We define type BlockSum that stores the result of the addition of two blocks. Values of this type are 33-bit words, made up using the constructor buildBlockSum that gathers one bit for the carry and a block for the sum. The five principal non-constructors for this type are eqBlockSum (which tests equality), addBlockSum (which adds two blocks and returns both a carry bit and a 32-bit sum), addBlock (which is derived from the former one by dropping the carry bit), addBlockHalf and addBlockHalves (which are similar to the former one but take half-word arguments that are converted to blocks before summation); the other non-constructors are auxiliary functions implementing a 32-bit adder built using four 8-bit adders. ------------------------------------------A.9 Definitions for Type Key

We define a type Key that is intended to represent the 64-bit keys (J, K) used by the MAA. This type has a constructor buildKey that takes two blocks and returns a key. In [START_REF] Menezes | Handbook of Applied Cryptography[END_REF], keys are represented using the type Pair, but we prefer introducing a dedicated type to clearly distinguish between keys and, e.g., results of the multiplication of two blocks.

type Key = struct {K: Block; J: Block};

A.10 Definitions (1) of MAA-specific Cryptographic Functions

We define a first set of functions to be used for MAA computations, most of which were present in [START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF] or have been later introduced in [START_REF] Menezes | Handbook of Applied Cryptography[END_REF]. ----------------------------------------- ----------------------------------------- ------------------------------------------function BYT (w1, w2: Block) returns (w, wp: Block); var opat: Octet;

B.5 Definitions of LNT library

We define here the LNT types together with functions related to this case study, and the LNT functions defining the scenario used in this case study.

B.5.1 Definitions of LNT Graph Functions and Types

We define here the types related to graph definitions together with the classical graph functions.

type Corner is 0, 1, 2, 3, 4, 5, 6, 7, 8 end type -----------------------------------------type Edge is Edge (q1: Corner, l: Street, q2: Corner) end type -----------------------------------------type Edges is --hash-table used as cache !card 100000 list of Edge with "head", "tail", "reverse", "length" end type ------------------------------------------type Vertices is list of Corner with "head", "tail" end type -----------------------------------------type Graph is --Digraph (directed graph)

Graph (V: Vertices, E: Edges) end type --------------------------------------------Functions end var end function ----------------------------------------- ------------------------------------------

B.5.2 Definitions of LNT Datatypes

The definition of the main types related to this case study together with heir functions.

-----------------------------------------type Localization is !printedby "PRINT_LOCALIZATION" --global localization (GPS) --localisation (graph with anotate state for the current position) Localization (c: Edge, G: Graph) end type -----------------------------------------type Grid is --local localization Grid (E: Edges) end type ------------------------------------------type Direction is turn_n (N: Nat) --5th if crossroads end type -----------------------------------------type Itinerary is list of Direction with "head", "tail", "reverse" end type -----------------------------------------type Control is --direction turned_n (N: Nat), brakes end type -----------------------------------------type Operation is --obstacle operations turned_n (N: Nat), --5th if crossroads, leave, random end type -----------------------------------------type Obstacle_behaviour is list of Operation with "head", "tail" end type ------------------------------------------type Obstacle is Obstacle (name: Street, position: Edge, behaviour: Obstacle_behaviour) end type -----------------------------------------type The_Obstacles is list of Obstacle with "head", "tail", "length" end type -----------------------------------------type LOG_END_CAR is COLLISION, ARRIVED, END_OBSTACLE end type -----------------------------------------type Obstacle_Wait is obst_wait (o: Obstacle, waiting: bool) end type ------------------------------------------type Obstacle_Info is obst_inf (o: Obstacle, car: Edge, obstacles: Grid) end type -----------------------------------------type Car_Obstacle_Pos is pos (car: Edge, obstacles: Grid) end type -----------------------------------------type Block_Init is ----------------------------------------- ----------------------------------------- ------------------------------------------

B.5.3 Definitions of the Scenario

We present here all functions corresponding to the scenario information of our model, which is modifiable such as the geographical map, the obstacles behaviors, the initial and destination streets.

print (iv1) fby printf (" = ") fby print (p1) fby printf (" and ") fby print (iv2) fby printf (" = ") fby print (p2) fby printf (" and ") fby print (iv3) fby printf (" = ") fby print (p3) fby printf (" and ") fby print (ov1) fby printf (" = ") fby print (o1) fby printf (" and ") fby print (ov2) fby printf (" = ") fby print (o2) fby printf (")\n or") end def -----------------------------------------macro verdict edge <| + on e: edge among out (s) where verdict edge (e) |> 1 end def -----------------------------------------def print inconclusive (n: natural, iv1, iv2, iv3: raw): action = if n > 1 then printf (" or\n") else nop end if fby printf (" ") fby print (iv1) fby printf (" = pre ") fby print (iv1) fby printf (" and ") fby print (iv2) fby printf (" = pre ") fby print (iv2) fby printf (" and ") fby print (iv3) fby printf (" = pre ") fby print (iv3) end def def print pass (n: natural): action = if n > 1 then printf (" or\n") else nop end if fby printf (" true") end def ------------------------------------------( * extraction of the names of the three inputs * ) let (iv1, iv2, iv3: raw) =

for in e: edge where in e -> [INPUTS ?iv1:raw ?iv2:raw ?iv3:raw ] apply (replace, replace, replace) else printf ("s") end if fby print (s) fby printf (" and ") ) fby printf ("true;\n") fby printf ("tel\n") end let end let end let end let

FigureFigure 1 . 1 :

 11 Figure 1.1: Overview of the testing methodology for GALS systems

Figure 2

 2 Figure 2.2: The IOLTS (and the IOTS in green) corresponding to the LTS in Figure 2.1

Figure 2 . 3 :

 23 Figure 2.3: Overview of the Lurette testing tool

Figure 2

 2 Figure 2.3 (inspired by [JHR13, Figure 3]) gives an overview of Lurette. The tool takes two inputs:

Figure 2 . 4 :

 24 Figure 2.4: Simple scenario automaton with the inputs values of the heater (actual_room_temperature and season)

  node input_constraints () returns (actual_room_temperature, season: int) = let Winter:int = 1, Spring:int = 2, Summer:int = 3, Autumn:int = 4 in loop { | actual_room_temperature = 18 and season = Winter | actual_room_temperature = 26 and season = Spring | actual_room_temperature = 34 and season = Summer | actual_room_temperature = 20 and season = Autumn } At each iteration, Lurette generates inputs by executing one transition of the Lutin node.

Figure 2

 2 Figure 2.5: Part of the oracle automaton with output new_room_temperature and input season, corresponding to an initial value of 20 for actual_room_temperature

const

  Winter = 1; const Spring = 2; const Summer = 3; const Autumn = 4; node oracle (season, temperature: int) returns (res, cover_seasons: bool); var s1, s2, s3, s4: bool; let res = true -> ( * if the first actual room temperature is 20 * ) ((season = Winter and temperature = 21) or (season = Winter and temperature = 22) or (season = Spring and temperature = 20) or (season = Spring and temperature = 21) or (season = Spring and temperature = 22) or (season = Summer and temperature = 20) or (season = Summer and temperature = 21) or (season = Summer and temperature = 22) or (season = Autumn and temperature = 20) or (season = Autumn and temperature = 21) or (season = Autumn and temperature = 22) ( * the cases for the other first actual room temperature values * ) or ...); ( * each intermediate variables s1 -s4 are covering one season * ) s1 = false -> if season = Winter then true else pre s1; s2 = false -> if season = Spring then true else pre s1; s3 = false -> if season = Summer then true else pre s1; s4 = false -> if season = Autumn then true else pre s1; ( * check the coverage of each season at least once * ) cover_seasons = false -> if s1 and s2 and s3 and s4 then true else pre cover_seasons; tel

Figure 2

 2 Figure 2.6: Examples of the implementation relation ioco.

  [START_REF] Hartman | The AGEDIS tools for model based testing[END_REF], JTorX[START_REF] Belinfante | JTorX: A Tool for On-line Model-driven Test Derivation and Execution[END_REF][START_REF] Belinfante | JTorX: Exploring Model-Based Testing[END_REF], STG[START_REF] Clarke | STG: A symbolic test generation tool[END_REF], TGV[START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF], TorX[START_REF] Tretmans | TorX: Automated Model-Based Testing[END_REF], TorXakis [MPS + 09, Tre17], Uppaal-Cover[START_REF] Hessel | Model-Based Testing of a WAP Gateway: An Industrial Case-Study[END_REF], Uppaal-Tron[START_REF] Kim | Testing Real-time Embedded Software Using UPPAAL-TRON: An Industrial Case Study[END_REF], and Uppaal-Yggdrasil [KLN + 15].

Figure 2

 2 Figure 2.7: Model M of the running example [JJ05]

Figure 2

 2 Figure2.9: The visible behavior SP vis , complete test graph CTG (gray), and a test case TC (dark gray) of the running example[START_REF] Jard | Tgv: Theory, principles and algorithms -a tool for the automatic synthesis of conformance test cases for nondeterministic reactive systems[END_REF]

4

  In TGV [JJ05], the actions of test cases are symmetric w.r.t. those of the model M and the SUT, i.e., A TC O ⊆ A M I (TC emits only inputs of M) and A TC I ⊆ A SUT O

Figure 2 .

 2 Figure 2.10: Simple smart room temperature management

Figure 2

 2 Figure 2.11: Architecture of the GRL model of the room temperature management

  block smart_window_contact (in time: nat, out status: window_status) [send send_info: window_status] is static var opening_time: nat := 0, var previous_info: window_status := already_sent; var is_open: bool := false; var info: window_status --detects if the window is open info := perception_window_open (); if previous_info == info then --the same status as the previous activation info := already_sent elsif (info == open) and (previous_info == close) and (is_open == false) then --the window has been opened since the last activation opening_time := time; info := previous_info; is_open := true elsif (info == open) and (time -opening_time > max_open_time) then --the window has been open for more than max open time opening_time := 0; previous_info := open; info := open; is_open := false else --the window has been closed since the last activation --(less than max open time minutes ago) previous_info := close; info := close; is_open := false end if; send_info := info; status := info end block

--

  Environment constraining the data carried by blocks environment room_temperature (out time: nat, out temperature: nat) is static var ticks: int := 0, pre_temperature: nat := 20 loop ticks := ticks + 1; select --The evolution of the temperature is abstract and changes gradually when temperature -> case pre_temperature is 18 -> select temperature := 18 [] temperature := 19 end select | 19 -> select temperature := 18 [] temperature := 19 [] temperature := 20 end select | 20 -> select temperature := 19 [] temperature := 20 [] temperature := 21 end select | 21 -> select temperature := 20 [] temperature := 21 end select | any -> temperature := 20 end case; pre_temperature := temperature [] when time -> time := ticks end select end loop end environment

Figure 3

 3 Figure 3.1: MAA data flow

Figure 3 . 2 :

 32 Figure 3.2: Mode of operation of the MAA

Figure 3

 3 Figure 3.3: The node MAC

Figure 3

 3 Figure 3.4: The function prelude

Figure 3

 3 Figure 3.5: Overview of the Lurette testing tool

Figure 3

 3 Figure 3.6: The MAC node rewritten

Figure

  Figure 3.7: Environment

  Figure 3.9: Oracle

  Figure 4.1 and Figure 4.2. The state machines are transition-based (i.e., the state names are for sake of readability only), and conditional actions are represented in brackets ([ ]).

  Figure 4.1: TLS handshake client

Figure 4

 4 Figure 4.2: TLS handshake server

Figure 4 . 3 :

 43 Figure 4.3: Architecture of TESTOR

Figure 4

 4 Figure 4.4: The visible behavior SP vis , complete test graph CTG (gray), and a test case TC (dark gray) of the running example [JJ05].

  par CLIENT_HELLO, HELLO_RETRY_REQUEST, SERVER_HELLO in SERVER [CLIENT_HELLO, HELLO_RETRY_REQUEST, SERVER_HELLO] || PURPOSE_A [CLIENT_HELLO, HELLO_RETRY_REQUEST, SERVER_HELLO, T_ACCEPT] end parNote that SERVER denotes a process implementing the Server behavior.

Figure 4

 4 Figure 4.5: TC I: TLS handshake with classical TLS 1.3 order

Figure 4

 4 Figure 4.6: TC II: TLS handshake aborted with an unexpected Alert

Figure 5 . 1 :

 51 Figure 5.1: Simple autonomous cars

  Figure 5.2: Geographical map example with the autonomous car and a pedestrian

Figure 5

 5 Figure 5.4: GRL geographical map representation

  block RADAR (in POSITIONS: Car_Obstacle_Pos) [send CURRENT: Grid] is static var previous_grid: Grid := Grid (NIL) var grid: Grid grid := perception (POSITIONS, radar_visibility); if grid != previous_grid then previous_grid := grid; CURRENT := grid else CURRENT := Grid (already_sent) end if end block

[

  true* . ( { RADAR_OUTPUT ?obstacle1:String ?street1:String ?obstacle2:String ?street2:String } . (not { RADAR_OUTPUT ... })* . { RADAR_OUTPUT !obstacle1 !street1 !obstacle2 !street2 } ) ] false

Figure 5

 5 Figure 5.5: Geographical map, with natural numbers identifying the streets fragments.

Figure 5 . 6 :

 56 Figure 5.6: Simple scenario automaton

  node input_constraints () returns (car, leo, lilly, s: int) = let not_visible: int = 2000 in ( * initial state: car on street 9 and no visible obstacles * ) car = 9 and lilly = not_visible and leo = not_visible and s = 0 fby loop { | ( * s = 0 -> car on street 9, lilly on street 5, leo on street 14, s = 1 * ) (pre s = 0) and car = 9 and lilly = 5 and leo = 14 and s = 1 | ( * s = 0 -> car on street 12, lilly on street 5, leo on street 14, s = 2 * ) (pre s = 0) and car = 12 and lilly = 5 and leo = 14 and s = 2 | ( * s = 1 -> car on street 9, leo on street 11, lilly on street 12, s = 3 * ) (pre s = 1) and car = 9 and lilly = 12 and leo = 11 and s = 3 | ( * s = 1 -> car on street 12, leo on street 11, lilly on street 5, s = 4 * ) (pre s = 1) and car = 12 and lilly = 5 and leo = 11 and s = 4 | ( * s = 2 -> car on street 12, leo on street 11, lilly on street 5, s = 4 * ) (pre s = 2) and car = 12 and lilly = 5 and leo = 11 and s = 4 | ( * s = 3 -> car on street 12, leo on street 14, lilly on street 5, s = 1 * ) (pre s = 3) and car = 9 and lilly = 5 and leo = 14 and s = 1 | ( * s = 4 -> car on street 12, leo on street 14, lilly on street 5, s = 2 * ) (pre s = 4) and car = 12 and lilly = 5 and leo = 14 and s = 2 }

Figure 5 . 7 :

 57 Figure 5.7: Overview of the derivation of synchronous test scenarios by projection and exploration of an asynchronous complete test graph CTG

Figure 5

 5 Figure 5.9: Overview of the testing methodology for GALS systems

  function orBit (x1, x2: Bit) returns (x: Bit); let x = if x2 = X0 then x1 else X1; tel;

  function xorBit (x1, x2: Bit) returns (x: Bit); let x = if x2 = X0 then x1 else notBit (x1); tel;

type

  Octet = struct {x1: Bit; x2: Bit; x3: Bit; x4: Bit; x5: Bit; x6: Bit; x7: Bit; x8: Bit}; -----------------------------------------const x00 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x01 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x02 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x03 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x04 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x05 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x06 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x07 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x08 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x09 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x0A = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x0B = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x0C = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x0D = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x0E = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x0F = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x10 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x11 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x12 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x13 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x14 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x15 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x16 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x17 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x18 = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x1A = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x1B = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x1C = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x1D = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x1E = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x1F = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x20 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x21 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x22 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x23 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x24 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x25 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x26 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x27 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x28 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x29 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x2A = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x2B = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x2D = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x2E = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x2F = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x30 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x31 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x32 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x33 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x34 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x35 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x36 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x37 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x38 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x39 = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x3A = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x3B = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x3C = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x3D = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x3E = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x3F = Octet {x1 = X0; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x40 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x41 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x42 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x43 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x44 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x45 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x46 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x47 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x48 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x49 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x4A = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x4B = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x4C = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x4D = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x4E = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x4F = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x50 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x51 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x53 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x54 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x55 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x58 = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x5A = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x5B = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x5C = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x5D = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x5E = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x5F = Octet {x1 = X0; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x60 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x61 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x62 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x63 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x64 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x65 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x66 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x67 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x69 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x6A = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x6B = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x6C = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x6D = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x6E = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x6F = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x70 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x71 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x72 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x73 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x74 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x75 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x76 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x77 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x78 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x79 = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x7A = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x7B = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x7C = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x7D = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x7E = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x7F = Octet {x1 = X0; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x80 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x81 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x83 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x84 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x85 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x86 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x89 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x8C = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x8D = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x8E = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x8F = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const x90 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const x91 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const x92 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const x93 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const x94 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const x95 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const x96 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const x97 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const x98 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const x99 = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const x9A = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const x9B = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const x9C = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const x9D = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const x9E = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const x9F = Octet {x1 = X1; x2 = X0; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const xA1 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const xA0 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const xA3 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const xA4 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const xA5 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const xA6 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const xA7 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const xA8 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const xA9 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const xAA = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const xAB = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const xAC = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const xAE = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const xAF = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const xB0 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const xB1 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const xB2 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const xB3 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const xB5 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const xB6 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const xB8 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const xB9 = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const xBA = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const xBB = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const xBC = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const xBE = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const xBF = Octet {x1 = X1; x2 = X0; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const xC0 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const xC1 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const xC2 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const xC4 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const xC5 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const xC6 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const xC7 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const xC8 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const xC9 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const xCA = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const xCB = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const xCC = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const xCD = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const xCE = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const xD0 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const xD1 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const xD2 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const xD3 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const xD4 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const xD5 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const xD6 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const xD7 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const xD9 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const xD8 = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const xDB = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const xDC = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const xDD = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const xDE = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const xDF = Octet {x1 = X1; x2 = X1; x3 = X0; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const xE0 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const xE1 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const xE2 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const xE3 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const xE6 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const xE8 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const xE9 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const xEA = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const xEB = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const xEC = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const xED = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const xEE = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const xEF = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X0; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; const xF0 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; const xF1 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X0; x8 = X1}; const xF2 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X0}; const xF3 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X0; x7 = X1; x8 = X1}; const xF4 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X0}; const xF5 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X0; x8 = X1}; const xF6 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X0}; const xF7 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X0; x6 = X1; x7 = X1; x8 = X1}; const xF8 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X0}; const xF9 = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X0; x8 = X1}; const xFA = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X0}; const xFB = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X0; x7 = X1; x8 = X1}; const xFC = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X0}; const xFD = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X0; x8 = X1}; const xFE = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X0}; const xFF = Octet {x1 = X1; x2 = X1; x3 = X1; x4 = X1; x5 = X1; x6 = X1; x7 = X1; x8 = X1}; -

  function leftOctet1 (o1: Octet) returns (o: Octet); let o = Octet {x1 = o1.x2; x2 = o1.x3; x3 = o1.x4; x4 = o1.x5; x5 = o1.x6; x6 = o1.x7; x7 = o1.x8; x8 = X0}; tel;

  function leftOctet2 (o1: Octet) returns (o: Octet); let o = Octet {x1 = o1.x3; x2 = o1.x4; x3 = o1.x5; x4 = o1.x6; x5 = o1.x7; x6 = o1.x8; x7 = X0; x8 = X0}; tel;

  function leftOctet3 (o1: Octet) returns (o: Octet); let o = Octet {x1 = o1.x4; x2 = o1.x5; x3 = o1.x6; x4 = o1.x7; x5 = o1.x8; x6 = X0; x7 = X0; x8 = X0}; tel;

  function leftOctet4 (o1: Octet) returns (o: Octet); let o = Octet {x1 = o1.x5; x2 = o1.x6; x3 = o1.x7; x4 = o1.x8; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; tel;

  function leftOctet5 (o1: Octet) returns (o: Octet); let o = Octet {x1 = o1.x6; x2 = o1.x7; x3 = o1.x8; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; tel;

  function leftOctet6 (o1: Octet) returns (o: Octet); let o = Octet {x1 = o1.x7; x2 = o1.x8; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; tel;

  function leftOctet7 (o1: Octet) returns (o: Octet); let o = Octet {x1 = o1.x8; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = X0}; tel;

  function rightOctet1 (o1: Octet) returns (o: Octet); let o = Octet {x1 = X0; x2 = o1.x1; x3 = o1.x2; x4 = o1.x3; x5 = o1.x4; x6 = o1.x5; x7 = o1.x6; x8 = o1.x7}; tel;

  function rightOctet2 (o1: Octet) returns (o: Octet); let o = Octet {x1 = X0; x2 = X0; x3 = o1.x1; x4 = o1.x2; x5 = o1.x3; x6 = o1.x4; x7 = o1.x5; x8 = o1.x6}; tel;

  function rightOctet3 (o1: Octet) returns (o: Octet); let o = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = o1.x1; x5 = o1.x2; x6 = o1.x3; x7 = o1.x4; x8 = o1.x5}; tel;

  function rightOctet4 (o1: Octet) returns (o: Octet); let o = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = o1.x1; x6 = o1.x2; x7 = o1.x3; x8 = o1.x4}; tel;

  function rightOctet5 (o1: Octet) returns (o: Octet); let o = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = o1.x1; x7 = o1.x2; x8 = o1.x3}; tel; A.3. Definitions for Type OctetSum 123

  function rightOctet6 (o1: Octet) returns (o: Octet); let o = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = o1.x1; x8 = o1.x2}; tel;

  function rightOctet7 (o1: Octet) returns (o: Octet); let o = Octet {x1 = X0; x2 = X0; x3 = X0; x4 = X0; x5 = X0; x6 = X0; x7 = X0; x8 = o1.x1}; tel;

  function addBit (x1, x2, x3: Bit) returns (x: Bit); let x = xorBit (xorBit (x1, x2), x3); tel;

  function dropCarryOctetSum (os: OctetSum) returns (o: Octet); let o = os.o; tel;

  function addOctet (o1, o2: Octet) returns (o: Octet); let o = dropCarryOctetSum (addOctetSum (o1, o2, X0)); tel;

  const x0000 = Half {o1 = x00; o2 = x00}; const x0001 = Half {o1 = x00; o2 = x01}; -

  function mulOctetA (h1: Half; o1, o2: Octet) returns (h: Half); var o3: Octet; os: OctetSum; let o3 = addOctet (h1.o1, o1); os = addOctetSum (h1.o2, o2, X0); h = if os.x = X0 then Half {o1 = o3; o2 = os.o} else Half {o1 = addOctet (o3, x01); o2 = os.o}; tel;

  function addHalfSum (h1, h2: Half) returns (hs: HalfSum) var os, os1: OctetSum; let os = addOctetSum (h1.o2, h2.o2, X0); os1 = addOctetSum (h1.o1, h2.o1, os.x); hs = HalfSum {x = os1.x; h = Half {o1 = os1.o; o2 = os.o}}; tel;

  function addHalfOctet (o1: Octet; h1: Half) returns (h: Half); let h = addHalf (Half {o1 = x00; o2 = o1}, h1); tel;

  function addHalfOctets (o1, o2: Octet) returns (h: Half); let h = addHalf (Half {o1 = x00; o2 = o1}, Half {o1 = x00; o2 = o2}); tel;

  const x00000000 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x00}; const x00000001 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x01}; const x00000002 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x02}; const x00000003 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x03}; const x00000004 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x04}; const x00000005 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x05}; const x00000006 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x06}; const x00000007 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x07}; const x00000008 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x08}; const x00000009 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x09}; const x0000000A = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x0A}; const x0000000B = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x0B}; const x0000000C = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x0C}; const x0000000D = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x0D}; const x0000000E = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x0E}; const x0000000F = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x0F}; const x00000010 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x10}; const x00000012 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x12}; const x00000014 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x14}; const x00000016 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x16}; const x00000018 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x18}; const x0000001B = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x1B}; const x0000001D = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x1D}; const x0000001E = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x1E}; const x0000001F = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x1F}; const x00000031 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x31}; const x00000036 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x36}; const x00000060 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x60}; const x00000080 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = x80}; const x000000A5 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = xA5}; const x000000B6 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = xB6}; const x000000C4 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = xC4}; const x000000D2 = Block {o1 = x00; o2 = x00; o3 = x00; o4 = xD2}; const x00000100 = Block {o1 = x00; o2 = x00; o3 = x01; o4 = x00}; const x00000129 = Block {o1 = x00; o2 = x00; o3 = x01; o4 = x29}; const x0000018C = Block {o1 = x00; o2 = x00; o3 = x01; o4 = x8C}; const x00004000 = Block {o1 = x00; o2 = x00; o3 = x40; o4 = x00}; const x00010000 = Block {o1 = x00; o2 = x01; o3 = x00; o4 = x00}; const x00020000 = Block {o1 = x00; o2 = x02; o3 = x00; o4 = x00}; const x00030000 = Block {o1 = x00; o2 = x03; o3 = x00; o4 = x00}; const x00040000 = Block {o1 = x00; o2 = x04; o3 = x00; o4 = x00}; const x00060000 = Block {o1 = x00; o2 = x06; o3 = x00; o4 = x00}; const x00804021 = Block {o1 = x00; o2 = x80; o3 = x40; o4 = x21}; const x00FF00FF = Block {o1 = x00; o2 = xFF; o3 = x00; o4 = xFF}; const x0103050B = Block {o1 = x01; o2 = x03; o3 = x05; o4 = x0B}; const x01030703 = Block {o1 = x01; o2 = x03; o3 = x07; o4 = x03}; const x01030705 = Block {o1 = x01; o2 = x03; o3 = x07; o4 = x05}; const x0103070F = Block {o1 = x01; o2 = x03; o3 = x07; o4 = x0F}; const x02040801 = Block {o1 = x02; o2 = x04; o3 = x08; o4 = x01}; const x0297AF6F = Block {o1 = x02; o2 = x97; o3 = xAF; o4 = x6F}; const x07050301 = Block {o1 = x07; o2 = x05; o3 = x03; o4 = x01}; const x07C72EAA = Block {o1 = x07; o2 = xC7; o3 = x2E; o4 = xAA}; const x0A202020 = Block {o1 = x0A; o2 = x20; o3 = x20; o4 = x20}; const x0AD67E20 = Block {o1 = x0A; o2 = xD6; o3 = x7E; o4 = x20}; const x10000000 = Block {o1 = x10; o2 = x00; o3 = x00; o4 = x00}; const x11A9D254 = Block {o1 = x11; o2 = xA9; o3 = xD2; o4 = x54}; const x11AC46B8 = Block {o1 = x11; o2 = xAC; o3 = x46; o4 = xB8}; const x1277A6D4 = Block {o1 = x12; o2 = x77; o3 = xA6; o4 = xD4}; const x13647149 = Block {o1 = x13; o2 = x64; o3 = x71; o4 = x49}; const x160EE9B5 = Block {o1 = x16; o2 = x0E; o3 = xE9; o4 = xB5}; const x17065DBB = Block {o1 = x17; o2 = x06; o3 = x5D; o4 = xBB}; const x1D10D8D3 = Block {o1 = x1D; o2 = x10; o3 = xD8; o4 = xD3}; const x1D3B7760 = Block {o1 = x1D; o2 = x3B; o3 = x77; o4 = x60}; const x1D9C9655 = Block {o1 = x1D; o2 = x9C; o3 = x96; o4 = x55}; const x1F3F7FFF = Block {o1 = x1F; o2 = x3F; o3 = x7F; o4 = xFF}; const x21D869BA = Block {o1 = x21; o2 = xD8; o3 = x69; o4 = xBA}; const x24B66FB5 = Block {o1 = x24; o2 = xB6; o3 = x6F; o4 = xB5}; const x270EEDAF = Block {o1 = x27; o2 = x0E; o3 = xED; o4 = xAF}; const x277B4B25 = Block {o1 = x27; o2 = x7B; o3 = x4B; o4 = x25}; const x2829040B = Block {o1 = x28; o2 = x29; o3 = x04; o4 = x0B}; const x288FC786 = Block {o1 = x28; o2 = x8F; o3 = xC7; o4 = x86}; const x28EAD8B3 = Block {o1 = x28; o2 = xEA; o3 = xD8; o4 = xB3}; const x29907CD8 = Block {o1 = x29; o2 = x90; o3 = x7C; o4 = xD8}; const x29C1485F = Block {o1 = x29; o2 = xC1; o3 = x48; o4 = x5F}; const x29EEE96B = Block {o1 = x29; o2 = xEE; o3 = xE9; o4 = x6B}; const x2A6091AE = Block {o1 = x2A; o2 = x60; o3 = x91; o4 = xAE}; const x2BF8499A = Block {o1 = x2B; o2 = xF8; o3 = x49; o4 = x9A}; const x2E80AC30 = Block {o1 = x2E; o2 = x80; o3 = xAC; o4 = x30}; const x2FD76FFB = Block {o1 = x2F; o2 = xD7; o3 = x6F; o4 = xFB}; const x30261492 = Block {o1 = x30; o2 = x26; o3 = x14; o4 = x92}; const x303FF4AA = Block {o1 = x30; o2 = x3F; o3 = xF4; o4 = xAA}; const x33D5A466 = Block {o1 = x33; o2 = xD5; o3 = xA4; o4 = x66}; const x344925FC = Block {o1 = x34; o2 = x49; o3 = x25; o4 = xFC}; const x34ACF886 = Block {o1 = x34; o2 = xAC; o3 = xF8; o4 = x86}; const x3CD54DEB = Block {o1 = x3C; o2 = xD5; o3 = x4D; o4 = xEB}; const x3CF3A7D2 = Block {o1 = x3C; o2 = xF3; o3 = xA7; o4 = xD2}; const x3DD81AC6 = Block {o1 = x3D; o2 = xD8; o3 = x1A; o4 = xC6}; const x3F6F7248 = Block {o1 = x3F; o2 = x6F; o3 = x72; o4 = x48}; const x48B204D6 = Block {o1 = x48; o2 = xB2; o3 = x04; o4 = xD6}; const x4A645A01 = Block {o1 = x4A; o2 = x64; o3 = x5A; o4 = x01}; const x4C49AAE0 = Block {o1 = x4C; o2 = x49; o3 = xAA; o4 = xE0}; const x4CE933E1 = Block {o1 = x4C; o2 = xE9; o3 = x33; o4 = xE1}; const x4D53901A = Block {o1 = x4D; o2 = x53; o3 = x90; o4 = x1A}; const x4DA124A1 = Block {o1 = x4D; o2 = xA1; o3 = x24; o4 = xA1}; const x4F998E01 = Block {o1 = x4F; o2 = x99; o3 = x8E; o4 = x01}; const x50DEC930 = Block {o1 = x50; o2 = xDE; o3 = xC9; o4 = x30}; const x51AF3C1D = Block {o1 = x51; o2 = xAF; o3 = x3C; o4 = x1D}; const x51EDE9C7 = Block {o1 = x51; o2 = xED; o3 = xE9; o4 = xC7}; const x550D91CE = Block {o1 = x55; o2 = x0D; o3 = x91; o4 = xCE}; const x55555555 = Block {o1 = x55; o2 = x55; o3 = x55; o4 = x55}; const x55DD063F = Block {o1 = x55; o2 = xDD; o3 = x06; o4 = x3F}; const x5834A585 = Block {o1 = x58; o2 = x34; o3 = xA5; o4 = x85}; const x5A35D667 = Block {o1 = x5A; o2 = x35; o3 = xD6; o4 = x67}; const x5BC02502 = Block {o1 = x5B; o2 = xC0; o3 = x25; o4 = x02}; const x5CCA3239 = Block {o1 = x5C; o2 = xCA; o3 = x32; o4 = x39}; const x5EBA06C2 = Block {o1 = x5E; o2 = xBA; o3 = x06; o4 = xC2}; const xF0239DD5 = Block {o1 = xF0; o2 = x23; o3 = x9D; o4 = xD5}; const x5F38EEF1 = Block {o1 = x5F; o2 = x38; o3 = xEE; o4 = xF1}; const x613F8E2A = Block {o1 = x61; o2 = x3F; o3 = x8E; o4 = x2A}; const x63C70DBA = Block {o1 = x63; o2 = xC7; o3 = x0D; o4 = xBA}; const x6AD6E8A4 = Block {o1 = x6A; o2 = xD6; o3 = xE8; o4 = xA4}; const x6AEBACF8 = Block {o1 = x6A; o2 = xEB; o3 = xAC; o4 = xF8}; const x6D67E884 = Block {o1 = x6D; o2 = x67; o3 = xE8; o4 = x84}; const x7050EC5E = Block {o1 = x70; o2 = x50; o3 = xEC; o4 = x5E}; const x717153D5 = Block {o1 = x71; o2 = x71; o3 = x53; o4 = xD5}; const x7201F4DC = Block {o1 = x72; o2 = x01; o3 = xF4; o4 = xDC}; const x7397C9AE = Block {o1 = x73; o2 = x97; o3 = xC9; o4 = xAE}; const x74B39176 = Block {o1 = x74; o2 = xB3; o3 = x91; o4 = x76}; const x7783C51D = Block {o1 = x77; o2 = x83; o3 = xC5; o4 = x1D}; const x7792F9D4 = Block {o1 = x77; o2 = x92; o3 = xF9; o4 = xD4}; const x7BC180AB = Block {o1 = x7B; o2 = xC1; o3 = x80; o4 = xAB}; const x7DB2D9F4 = Block {o1 = x7D; o2 = xB2; o3 = xD9; o4 = xF4}; const x7DFEFBFF = Block {o1 = x7D; o2 = xFE; o3 = xFB; o4 = xFF}; const x7F76A3B0 = Block {o1 = x7F; o2 = x76; o3 = xA3; o4 = xB0}; const x7F839576 = Block {o1 = x7F; o2 = x83; o3 = x95; o4 = x76}; const x7FFFFFF0 = Block {o1 = x7F; o2 = xFF; o3 = xFF; o4 = xF0}; const x7FFFFFF1 = Block {o1 = x7F; o2 = xFF; o3 = xFF; o4 = xF1}; const x7FFFFFFC = Block {o1 = x7F; o2 = xFF; o3 = xFF; o4 = xFC}; const x7FFFFFFD = Block {o1 = x7F; o2 = xFF; o3 = xFF; o4 = xFD}; const x80000000 = Block {o1 = x80; o2 = x00; o3 = x00; o4 = x00}; const x80000002 = Block {o1 = x80; o2 = x00; o3 = x00; o4 = x02}; const x800000C2 = Block {o1 = x80; o2 = x00; o3 = x00; o4 = xC2}; const x80018000 = Block {o1 = x80; o2 = x01; o3 = x80; o4 = x00}; const x80018001 = Block {o1 = x80; o2 = x01; o3 = x80; o4 = x01}; const x80397302 = Block {o1 = x80; o2 = x39; o3 = x73; o4 = x02}; const x81D10CA3 = Block {o1 = x81; o2 = xD1; o3 = x0C; o4 = xA3}; const x89D635D7 = Block {o1 = x89; o2 = xD6; o3 = x35; o4 = xD7}; const x8CE37709 = Block {o1 = x8C; o2 = xE3; o3 = x77; o4 = x09}; const x8DC8BBDE = Block {o1 = x8D; o2 = xC8; o3 = xBB; o4 = xDE}; const x9115A558 = Block {o1 = x91; o2 = x15; o3 = xA5; o4 = x58}; const x91896CFA = Block {o1 = x91; o2 = x89; o3 = x6C; o4 = xFA}; const x9372CDC6 = Block {o1 = x93; o2 = x72; o3 = xCD; o4 = xC6}; const x98D1CC75 = Block {o1 = x98; o2 = xD1; o3 = xCC; o4 = x75}; const x9D15C437 = Block {o1 = x9D; o2 = x15; o3 = xC4; o4 = x37}; const x9DB15CF6 = Block {o1 = x9D; o2 = xB1; o3 = x5C; o4 = xF6}; const x9E2E7B36 = Block {o1 = x9E; o2 = x2E; o3 = x7B; o4 = x36}; const xA018C83B = Block {o1 = xA0; o2 = x18; o3 = xC8; o4 = x3B}; const xA0B87B77 = Block {o1 = xA0; o2 = xB8; o3 = x7B; o4 = x77}; const xA44AAAC0 = Block {o1 = xA4; o2 = x4A; o3 = xAA; o4 = xC0}; const xA511987A = Block {o1 = xA5; o2 = x11; o3 = x98; o4 = x7A}; const xA70FC148 = Block {o1 = xA7; o2 = x0F; o3 = xC1; o4 = x48}; const xA93BD410 = Block {o1 = xA9; o2 = x3B; o3 = xD4; o4 = x10}; const xAAAAAAAA = Block {o1 = xAA; o2 = xAA; o3 = xAA; o4 = xAA}; const xAB00FFCD = Block {o1 = xAB; o2 = x00; o3 = xFF; o4 = xCD}; const xAB01FCCD = Block {o1 = xAB; o2 = x01; o3 = xFC; o4 = xCD}; const xAB6EED4A = Block {o1 = xAB; o2 = x6E; o3 = xED; o4 = x4A}; const xABEEED6B = Block {o1 = xAB; o2 = xEE; o3 = xED; o4 = x6B}; const xACBC13DD = Block {o1 = xAC; o2 = xBC; o3 = x13; o4 = xDD}; const xB1CC1CC5 = Block {o1 = xB1; o2 = xCC; o3 = x1C; o4 = xC5}; const xB8142629 = Block {o1 = xB8; o2 = x14; o3 = x26; o4 = x29}; const xB99A62DE = Block {o1 = xB9; o2 = x9A; o3 = x62; o4 = xDE}; const xBA92DB12 = Block {o1 = xBA; o2 = x92; o3 = xDB; o4 = x12}; const xBBA57835 = Block {o1 = xBB; o2 = xA5; o3 = x78; o4 = x35}; const xBE9F0917 = Block {o1 = xBE; o2 = x9F; o3 = x09; o4 = x17}; const xBF2D7D85 = Block {o1 = xBF; o2 = x2D; o3 = x7D; o4 = x85}; const xBFEF7FDF = Block {o1 = xBF; o2 = xEF; o3 = x7F; o4 = xDF}; const xC1ED90DD = Block {o1 = xC1; o2 = xED; o3 = x90; o4 = xDD}; const xC21A1846 = Block {o1 = xC2; o2 = x1A; o3 = x18; o4 = x46}; const xC4EB1AEB = Block {o1 = xC4; o2 = xEB; o3 = x1A; o4 = xEB}; const xC6B1317E = Block {o1 = xC6; o2 = xB1; o3 = x31; o4 = x7E}; const xCBC865BA = Block {o1 = xCB; o2 = xC8; o3 = x65; o4 = xBA}; const xCD959B46 = Block {o1 = xCD; o2 = x95; o3 = x9B; o4 = x46}; const xD0482465 = Block {o1 = xD0; o2 = x48; o3 = x24; o4 = x65}; const xD636250D = Block {o1 = xD6; o2 = x36; o3 = x25; o4 = x0D}; const xD7843FDC = Block {o1 = xD7; o2 = x84; o3 = x3F; o4 = xDC}; const xD78634BC = Block {o1 = xD7; o2 = x86; o3 = x34; o4 = xBC}; const xD8804CA5 = Block {o1 = xD8; o2 = x80; o3 = x4C; o4 = xA5}; const xDB79FBDC = Block {o1 = xDB; o2 = x79; o3 = xFB; o4 = xDC}; const xDB9102B0 = Block {o1 = xDB; o2 = x91; o3 = x02; o4 = xB0}; const xE0C08000 = Block {o1 = xE0; o2 = xC0; o3 = x80; o4 = x00}; const xE6A12F07 = Block {o1 = xE6; o2 = xA1; o3 = x2F; o4 = x07}; const xEB35B97F = Block {o1 = xEB; o2 = x35; o3 = xB9; o4 = x7F}; const xF14D6E28 = Block {o1 = xF1; o2 = x4D; o3 = x6E; o4 = x28}; const xF2EF3501 = Block {o1 = xF2; o2 = xEF; o3 = x35; o4 = x01}; const xF6A09667 = Block {o1 = xF6; o2 = xA0; o3 = x96; o4 = x67}; const xFD297DA4 = Block {o1 = xFD; o2 = x29; o3 = x7D; o4 = xA4}; const xFDC1A8BA = Block {o1 = xFD; o2 = xC1; o3 = xA8; o4 = xBA}; const xFE4E5BDD = Block {o1 = xFE; o2 = x4E; o3 = x5B; o4 = xDD}; const xFECCAA6E = Block {o1 = xFE; o2 = xCC; o3 = xAA; o4 = x6E}; const xFEFC07F0 = Block {o1 = xFE; o2 = xFC; o3 = x07; o4 = xF0}; const xFF2D7DA5 = Block {o1 = xFF; o2 = x2D; o3 = x7D; o4 = xA5}; const xFFEF0001 = Block {o1 = xFF; o2 = xEF; o3 = x00; o4 = x01}; const xFFFF00FF = Block {o1 = xFF; o2 = xFF; o3 = x00; o4 = xFF}; const xFFFFFF2D = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = x2D}; const xFFFFFF3A = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = x3A}; const xFFFFFFF0 = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xF0}; const xFFFFFFF1 = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xF1}; const xFFFFFFF4 = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xF4}; const xFFFFFFF5 = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xF5}; const xFFFFFFF7 = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xF7}; const xFFFFFFF9 = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xF9}; const xFFFFFFFA = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xFA}; const xFFFFFFFB = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xFB}; const xFFFFFFFC = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xFC}; const xFFFFFFFD = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xFD}; const xFFFFFFFE = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xFE}; const xFFFFFFFF = Block {o1 = xFF; o2 = xFF; o3 = xFF; o4 = xFF}; -

  function xorBlock (w1, w2: Block) returns (w: Block); let w = Block {o1 = xorOctet (w1.o1, w2.o1); o2 = xorOctet (w1.o2, w2.o2); o3 = xorOctet (w1.o3, w2.o3); o4 = xorOctet (w1.o4, w2.o4)}; tel;

type

  OctetSum = struct {x: Bit; o: Octet}; type BlockSum = struct {x: Bit; b: Block}; -----------------------------------------function addBlockSum (w1, w2 : Block) returns (ws: BlockSum); var os, os1, os2, os3: OctetSum; function mulBlock (w1, w2: Block) returns (ww: Pair); var w11, w12, w21, w22, w3, w4, w5: Block; let w11 = mulHalf (HalfU (w1), HalfU (w2)); w12 = mulHalf (HalfU (w1), HalfL (w2)); w21 = mulHalf (HalfL (w1), HalfU (w2)); w22 = mulHalf (HalfL (w1), HalfL (w2)); w3 = addBlockHalf (HalfL (w12), addBlockHalves (HalfL (w21), HalfU (w22))); w4 = addBlockHalf (HalfU (w3), addBlockHalf (HalfL (w11), addBlockHalves (HalfU (w12), HalfU(w21)))); w5 = addBlockHalves (HalfU (w4), HalfU (w11)); ww = Pair {w1 = Block {o1 = w5.o3; o2 = w5.o4; o3 = w4.o3; o4 = w4.o4}; w2 = Block {o1 = w3.o3; o2 = w3.o4; o3 = w22.o3; o4 = w22.o4}}; tel;

  function CYC (w1: Block) returns (w: Block); let w = Block {o1 = Octet {x1 = w1.o1.x2; x2 = w1.o1.x3; x3 = w1.o1.x4; x4 = w1.o1.x5; x5 = w1.o1.x6; x6 = w1.o1.x7; x7 = w1.o1.x8; x8 = w1.o2.x1}; o2 = Octet {x1 = w1.o2.x2; x2 = w1.o2.x3; x3 = w1.o2.x4; x4 = w1.o2.x5; x5 = w1.o2.x6; x6 = w1.o2.x7; x7 = w1.o2.x8; x8 = w1.o3.x1}; o3 = Octet {x1 = w1.o3.x2; x2 = w1.o3.x3; x3 = w1.o3.x4; x4 = w1.o3.x5; x5 = w1.o3.x6; x6 = w1.o3.x7; x7 = w1.o3.x8; x8 = w1.o4.x1}; o4 = Octet {x1 = w1.o4.x2; x2 = w1.o4.x3; x3 = w1.o4.x4; x4 = w1.o4.x5; x5 = w1.o4.x6; x6 = w1.o4.x7; x7 = w1.o4.x8; x8 = w1.o1.x1};}; tel;-----------------------------------------function FIX1 (w1: Block) returns (w: Block); let w = andBlock (orBlock (w1, x02040801), xBFEF7FDF); tel;

  function FIX2 (w1: Block) returns (w: Block); let w = andBlock (orBlock (w1, x00804021), x7DFEFBFF); tel;-----------------------------------------function needAjust (o: Octet) returns (b: bool); let b = ((o = x00) or (o =xFF)); tel;-----------------------------------------function adjustCode (o: Octet) returns (x: Bit); let x = if needAjust (o) = true then X1 else X0; tel;-----------------------------------------function adjust (o1, o2: Octet) returns (o: Octet); let o = if needAjust (o1) = true then xorOctet (o1, o2) else o1; tel;

  function PAT(w1, w2: Block) returns (o: Octet); let o = Octet {x1 = adjustCode (w1.o1); x2 = adjustCode (w1.o2); x3 = adjustCode (w1.o3); x4 = adjustCode (w1.o4); x5 = adjustCode (w2.o1); x6 = adjustCode (w2.o2); x7 = adjustCode (w2.o3); x8 = adjustCode (w2.o4)}; tel;

  l_obs := tail (l_obs) end loop; return up_l end var end function -----------------------------------------function is_q1q2_in_R (R: Grid, A: Localization) : bool is var E : Edges, P: Edge in E := R.E; P := A.C; loop if E == {} then return false else if (head(E).q1) == P.q1 and (head(E).q2 == P.q2) then return true end if; E := tail(E) end if end loop end var end function-----------------------------------------function intersection (R: Grid, A: Localization) : bool is return is_q1q2_in_R (R, A) end function-----------------------------------------function get_localizalitation (L: Localization) : Edge is return L.C end function-----------------------------------------function get_graph (L: Localization) : Graph is return L.G end function

  function get_grid (R: Grid) : Edges is return R.E end function

  function get_obstacle (OW: Obstacle_Wait) : Obstacle is return OW.o end function-----------------------------------------function get_action (OW: Obstacle_Wait) : bool is return OW.waiting end function -----------------------------------------function get_false (b: Block_Sent) : bool is use b; return false end function-----------------------------------------function ret_b1 (b: Block_Init) : String is return b.b1 end function-----------------------------------------function ret_b2 (b: Block_Init) : String is return b.b2 end function

  (e) = (((e) -> [INCONCLUSIVE]) or ((e) -> [PASS])) end macro def verdict state (s: state): boolean = exists e:edge among out (s) in verdict edge (e) end exists and forall e:edge among out (s) in verdict edge (e) end forall end def def nb verdicts (s: state): natural =

Table 2 .

 2 1 compares synchronous test data generators according to: (1) the testing paradigm (white or black box); (2) the programming paradigm automating the test sequence generation, more particularly Constraint Logic Programming (CLP) or Binary Decision Diagrams (BDD); (3) the presence of a scenario guiding the test sequence generation; and (4) the presence of nondeterminism in the input constraint descriptions.

	verdict
	inputs / outputs

Table 2

 2

			.1: Synchronous test generation tools
	tool	test paradigm	programming scenario language nondeterminism time paradigm
	Lutess v1	black	BDD	behavioral model	no	no
	Lutess v2	black	CLP	no	no	no
	Lurette	black	BDD	Lutin scenario	yes	Lustre
	Gatel	white	CLP	no	no	Lustre
	Testium	black	CLP	SPTL scenario	yes	no

  {} is converted to nil, and {0} is converted to cons (0, nil). Value assignments to variables are performed with the := operator. For instance, the LNT function n_coins takes as input a number n and a coin value, and computes a list of n coins of this value:

	Similarly, Functions define operations on types. The predefined data types are already provided with
	predefined functions. Functions are defined with the function keyword. The passing of
	parameters to a function can be done by copy (parameter in), or by reference (parameter
	out or in out). By default, a parameter is passed by copy. A function can return a value
	of a certain type. Recursive calls are allowed. Control structures, such as conditional
	branching or loops, are available. Various statements can be used inside a function, for
	instance correct termination (null), sequential composition (;), function return (return),
	variable declaration (var), conditional construct (if), breakable loop construct (loop), for
	loop construct (for). function n_coins (n: int, value: coin) : coins is
	var cash: coins in
	cash := {};
	loop L
	if n <= 0 then break L
	else
	cash := cons (value, cash);
	n := n -1
	end if
	end loop;
	return cash
	end var
	end function
	type coin is
	5, 10, 20, 50, 1, 2
	end type
	type coins is
	list of coin
	end type
	The latter is syntactic sugar for:
	type coins is
	cons (head: coin, tail: coins)
	end type

  true* . COIN . true*. TEA > true

	b) The following MCL formula encodes a liveness property expressing inevitability using
	fixed point operators. It states that all transition sequences starting at the current
	state lead to TERMINATE actions after a finite number of steps, e.g., the vending machine
	system terminates on a COFFEE or TEA transition:
	mu X . (< true > true and [ not TERMINATE ] X)
	where TERMINATE is an MCL macro denoting the termination actions (COFFEE or TEA):
	macro TERMINATE () = ( COFFEE or TEA ) end macro
	c) The following MCL formula encodes a fairness property, that expresses reachability of
	actions by considering only fair execution sequences, e.g., after every COIN inserted,
	all fair execution sequences (i.e., by skipping cycles) will lead to the reception of a
	TERMINATE action:
	[ true* . COIN . (not TERMINATE)* ] < true* . TERMINATE > true
	d) The following MCL formula encodes a safety property, which expresses that something
	bad never happens, e.g., if the action COIN occurs, then while there is no action TEA or
	COFFEE, no other action COIN may happen:
	[ true*. COIN . ( not (COFFEE or TEA) )*. COIN ] false
	e) It is also possible to use action predicates in the MCL formulas, for instance the following
	MCL formula encodes a safety property, which expresses that a kid should not get a
	caffeine drink, denoted by the predicate caffeine(drink):
	[ true *. KID . {CUP ?drink:String where not (caffeine(drink))} ] false

  where P is a set of state.

	coins ?10
		coins ?20	c o in s ? 2 0	not ioco	coins ?20	ioco	c o i n s ? 2 0	c o in s ? 1 0
	coins ?10
	coins ?20	cup !coffee		c u p ! c o f f e e	c u p ! t e a		cup !coffee	coins ?10 coins ?20	cup !tea	coins ?10 coins ?20
	coins ?10 coins ?20								coins ?10 coins ?20
							coins ?20 coins ?10

Table 2 .

 2 2 compares these ioco conformance tools by taking into account the following six tool features: (1) online conformance testing (i.e., a simultaneous execution of the model and the SUT or/and offline); (2) a test selection to generate relevant tests; (3) ont-the-fly

	tests generation; (4) handling nondeterministic models; (5) handling timed models; and
	(6) handling infinite models.
	Table 2.2: Comparison of ioco model-based testing tools
	tool	online/ coverage offline criteria purpose test	on-the-fly nondeter.	timed LTS
	AGEDIS	offline	yes	yes	yes	yes

  Table2.3 compares these GALS modeling approaches by taking into account the five concepts described above, more particularly: (C1) the modelling of the synchronous atomicity; (C2-C3) the nondeterminism in order to model communication protocols, or an existing communication protocol; and (C4-C5) the modelling of activation strategies and of data constraints on the components.

		Table 2.3: Approaches to model GALS systems
	name	synchronous atomicity	communication nondeterministic protocol	constraints data activation
	CRSM Promela	Esterel synch. semantics	yes	no	yes	no
	SAM-LNT	functions	yes	user defined yes	no
	Signal Promela atomic constraints Promela	yes	LTTA	yes	auto clock constraints
	SYSTEMJ	Esterel synch. semantics	no	no	yes	no
	GRL	synch. blocks	yes	user defined yes	yes

  ical Laboratory (NPL) in response to a request of the UK Bankers Automated Clearing Services. The MAA was adopted by ISO in 1987 and became part of the international standards 8730 [ISO86] and 8731-2[START_REF] Iso | Approved Algorithms for Message Authentication -Part 1: Data Encryption Algorithm (DEA)[END_REF]. Later, cryptanalysis of the MAA revealed various weaknesses, including feasible brute-force attacks, existence of collision clusters, and key-recovery techniques [PvO96, RPD96, PRvO97, PvO99, Pre11]. For this reason, the MAA was withdrawn from ISO standards in 2002.Nowadays, message authentication codes are computed using different families of algorithms based on either cryptographic hash functions (HMAC), universal hash functions (UMAC), or block ciphers (CMAC, OMAC, PMAC, etc.). Contrary to these modern approaches, the MAA was designed as a standalone algorithm that does not rely on any preexisting hash function or cipher. In this section, we briefly explain the principles of the MAA. More detailed explanations can be found in[START_REF] Davies | A Message Authenticator Algorithm Suitable for a Mainframe Computer[END_REF][START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF] and [MvOV96, Algorithm 9.68].

  Table 5 of [DC88], checking if the MAA signature is correctly computed on four groups of checks, with two different keys and two different messages; T3 corresponds to 64 tests. (T4) checks all intermediary values of the algorithm with a message of 20 blocks containing only zeros directly taken from Table 6 of [DC88], T4 corresponds to 45 tests.

Table 3 .

 3 8 contains the test vector (T3), more precisely, four groups of checks, with two different keys and two different messages.

	MAA Variables	Message 1	Message 2	Message 3	Message 4
	J	00FF 00FF	00FF 00FF	5555 5555	5555 5555
	K	0000 0000	0000 0000	5A35 D667	5A35 D667
	P	FF	FF	00	00
	X0	4A64 5A01	4A64 5A01	34AC F886	34AC F886
	Y0	50DE C930	50DE C930	7397 C9AE	7397 C9AE
	V0	5CCA 3239	5CCA 3239	7201 F4DC	7201 F4DC
	W	FECC AA6E	FECC AA6E	2829 040B	2829 040B
	M1	5555 5555	AAAA AAAA	0000 0000	FFFF FFFF
	X	48B2 04D6	6AEB ACF8	2FD7 6FFB 8DC8 BBDE
	Y	5834 A585	9DB1 5CF6	550D 91CE FE4E 5BDD
	M2	AAAA AAAA	5555 5555	FFFF FFFF	0000 0000
	X	4F99 8E01	270E EDAF	A70F C148 CBC8 65BA
	Y	BE9F 0917	B814 2629	1D10 D8D3	0297 AF6F
	S	51ED E9C7	51ED E9C7	9E2E 7B36	9E2E 7B36
	X	3449 25FC	2990 7CD8	B1CC 1CC5 3CF3 A7D2
	Y	DB91 02B0	BA92 DB12	29C1 485F	160E E9B5
	T	24B6 6FB5	24B6 6FB5	1364 7149	1364 7149
	X	277B 4B25	28EA D8B3	288F C786	D048 2465
	Y	D636 250D	81D1 0CA3	9115 A558	7050 EC5E
	Z	F14D 6E28	A93B D410	B99A 62DE	A018 C83B
	Figure 3.8: Tests (T3) inspired by Table 5 of [DC88].

Table 3

 3

	.8.

lines and contains 9 types (structures), 442 constants, 100 functions, and 2 nodes. Our Lustre model of the MAA was validated by the 201 tests successfully.

  To check whether the MAA calculations are correct or not, the REC model was enriched with the 201 test vectors used also to validate the Lustre model, and 2 others to validate the "mode of operation" [GM17, Annexes B.18 to B.21]. The resulting REC model has 1575 lines and contains 13 sorts, 18 constructors, 644 nonconstructors, and 684 rewrite rules. Using a collection of translators developed at Inria Grenoble, the REC model was automatically translated into various languages: AProVE (TRS), Clean, Haskell, LNT, LOTOS, Maude, mCRL2, OCaml, Opal, Rascal, Scala, SML, Stratego/XT, and Tom. Using the interpreters, compilers, and checkers available for these languages, it was shown [GM17, Sect. 5] that the REC model terminates, that it is confluent, and that sall the 203 tests pass successfully.Then, we also performed a major revision of LOTOS-92 based upon the detailed knowledge of the MAA acquired during the development of the REC model. Our goal was to produce an executable LOTOS model (LOTOS-17) as simple as possible, even if it departed from the original not executable model LOTOS-91 written by Harold B. Munster. Many changes were brought: the Nat sort was replaced almost everywhere by the Block sort; about seventy operations were removed, while a dozen new operations were added; the Block constructor evolved by taking four bytes rather than thirty-two bits; the Prelude operation is executed only once per message, rather than once per segment; the detection of messages larger than 1,000,000 blocks is now written directly in C; etc. These changes led to a 266-line LOTOS model (see Annex C) with two companion C files (157 lines in total) implementing the basic operations on blocks. Interestingly, all these files taken together are smaller than the original model LOTOS-91, demonstrating that executability and conciseness are not necessarily antagonistic notions. Our LOTOS model was validated by the CAESAR.ADT compiler, which implements all the syntactic and semantic checks stated in the definition of LOTOS[START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF]. The C code generated from the LOTOS model passed the test vectors specified in [ISO90, Annexes E.3.4 and E.4].Finally, we entirely rewrote LNT-16 in order to obtain a simpler model. First, the same changes as for LOTOS-17 were applied to the LNT model. Also, the sorts Pair, TwoPairs, and ThreePairs, which had been introduced by Harold B. Munster to describe functions returning two, four, and six blocks, have been eliminated; this was done by having LNT functions that return their computed results using "out" or "in out" parameters (i.e., call by result or call by value result) rather than tuples of values; the principal functions (e.g., MUL1, MUL2, MUL2A, PRELUDE, CODA, MAC, etc.) have been simplified by taking advantage of the imperative style LNT, i.e., mutable variables and assignments; many auxiliary functions have been gathered and replaced by a few larger functions (e.g., PreludeJ, PreludeK, PreludeHJ, and PreludeHK) also written in the imperative style. These changes resulted in a 268-line LNT model with a 136-line companion C file, which have nearly the same size as LOTOS-17 , although the LNT version is more readable and closer to the original MAA model[START_REF] Davies | The Message Authenticator Algorithm (MAA) and its Implementation[END_REF], also expressed in an imperative style. As for Lustre, the LNT model was then enriched with the same collection of test vectors, and supplementary test vectors intended to specifically check for certain aspects (byte permutations and message segmentation) that were not enough covered by the above tests; this was done by introducing a makeMessage function acting as a pseudo-random message generator. Finally, the remaining test vectors of [ISO90, Annexes E.3.4 and E.4], which were too lengthy to be included in the Lustre model and the REC-17, have been stored in text files and can be checked by running the C code generated from the LNT model. This makes LNT-17 the most complete formal model of the MAA as far as validation is concerned. Our LNT model was validated by the LNT2LOTOS translator, which implements the syntactic checks and (part of) the semantic checks stated in the definition of LNT [CCG + 19] and generates LOTOS code, which is then validated by the CAESAR.ADT compiler, therefore performing the remaining semantics checks of LNT. The C code generated by the CAESAR.ADT compiler passed the test vectors specified in [ISO92, 17, Annex A], in [ISO90, Annexes E.3], in [ISO90, Annexes E.3.4 and E.4], and the supplementary test vectors based on an additional function building messages.

	The modelisation of the MAA and its validation enabled us to discover various mistakes
	in prior (informal and formal) specifications of the MAA:
	1. a mistake in the test vectors for the function PAT (part of the function Prelude),
	given in [ISO92, Annex A] and [DC88], the correction and more details are available
	in [GM17, Annex A];
	2. a mistake in the test vectors for the full MAA algorithm, given in [ISO90, Annex E],
	the correction and more details are available in [GM18, Annex A];

Table 4 .

 4 1: Run-time performance for selected examples

	TESTOR	TGV

  Given our formal LNT model of the TLS handshake and our test purposes, we automatically generated with TESTOR the abstract test cases, represented in a simplified form in Figures 4.5, 4.6, and 4.7 (TC I, TC II, and TC III). We simplified the labels by removing the arguments and replacing the channel names with the following ini-

				CR(..CA..)		CC(..)
	HRR(..)	SH(..)	EE(..)	CS(..)	CV(..)	FC(..)
	CH(..)	CH(..)			FS(..)	PASS
				CR(..VOID F..)
			Figure 4.7: TC III: TLS handshake with renegotiation
	The LNT models of these test purposes are given in [BMMW18, Appendix B1, B2, B3],
	respectively.

tials: client hello (CH), server hello (SH), hello retry request (HRR), encrypted extensions (EE), certificate request (CR), certificate (CS for the server and CC for the client), certificate verify (CV), and finished (FS for the server and FC for the client). Note that we voluntarily left the initials of the certificate names (CA and VOID F) for the certificate request actions, to keep a deterministic representation of the abstract test cases.

  MAP_MANAGEMENT.

	system MAIN (SEND_CURRENT_GRID, RECEIVE_CURRENT_GRID: Grid,
	POSITIONS: Car_Obstacle_Pos, REQUEST_PATH: Edges,
	RECEIVE_PATH: Itinerary, CAR_MOVE: Control, ...) is
	block list
	ACTION (?CAR_MOVE) [?REQUEST_PATH,RECEIVE_CURRENT_GRID,RECEIVE_PATH],
	RADAR (POSITIONS) [?SEND_CURRENT_GRID], ...
	medium list
	CURRENT_GRID [SEND_CURRENT_GRID, ?RECEIVE_CURRENT_GRID], ...
	environment list
	MAP_MANAGEMENT (RADAR, OBSTACLE_MOVE, ...
	?POSITIONS, ?UPDATE_POSITION, ...)
	end system

  .8: Test Purpose T 1 Table5.1: Sizes and run-time performance for the complete test graphs for the test purposes

		TP		CTG		time mem.
		states trans.	states	trans. (s) (MB)
	T 1	2	3 102,985 211,455 1237	231
	T 2	3	4	15,466	29,665	29	200
	T 3	3	4	15,444	29,957	26	200
	T 4	3	4	2,278	4,959	86	193
	T 5	3	5	21,930	42,788	36	201
	the resulting graph for weak trace equivalence (see Section 2.1.2), yielding the projected
	test graph CTG

C .

Table 5 .

 5 2: Sizes and run-time performance for the tests generated for the test purposes

		CTG RADAR	constraints	oracle	time mem.
		states trans. (Lutin lines) (Lustre lines) (s) (MB)
	T 1	584	3617	3622	1916 1237	231
	T 2	89	281	286	295	29	200
	T 3	83	258	263	282	26	200
	T 4	218	1119	1124	557	86	193
	T 5	105	356	361	344	36	201

  function is_q1q2_in_E (in var E: Edges, A: Edge) : Bool is loop if E == {} then return false else if (head(E).q1) == A.q1 and (head(E).q2 == A.q2) then

	return true
	end if;
	E := tail(E)
	end if
	end loop
	end function

This automaton is not an LTS.

This automaton is not an LTS.

More details about IOLTS are available in Section 2.1.1

Historically, GRL was defined as a pivot language between synchronous programs with graphical syntax (e.g., function-block diagrams) and LNT, and evolved subsequently into a plain language for GALS systems.

The names FIX1 and FIX2 are borrowed from [Mun91b, pages 36 and 77].

More details about LNT are available in Chapter 2 Section 2.3.1).

http://mars-workshop.org/repository/018-TLS.html

The TESTOR tool is available at http://convecs.inria.fr/software/testor

The petit prince cluster is part of the Grid'5000 testbed, which is supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organizations (see https://www.grid5000.fr).

 4 The S-boxes are executed sequentially rather than in parallel and the gate SUBKEY is left visible to separate the iterations of the DES algorithm and thus significantly reduce the size of τ -components. For the extraction of TC for the TP using REFUSE transitions, from the full version of the DES, TESTOR would run for several weeks and TGV would require more than 700 GB of RAM.

http://cadp.inria.fr/man/executor.html

The complete GRL model, test purpose, the MCL properties, XTL scripts, and other resources related to the example are available at http://convecs.inria.fr/software/projex_aQTspX.tgz.

Currently, for the interaction between a block and an environment, GRL requires to wrap several inputs or outputs into a single structured input or output.

More details about model checking and temporal properties are available in Section 2.1.3.

More details about XTL are available in Section 2.3.2

More details about the Lustre pre operator are available in Section 2.2.1

http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/

https://cadp.inria.fr/

-----------------------------------------environment Env_MAP_MANAGEMENT (block ACTION, block DECISION, block RADAR, block GPS, block OBSTACLE_EXECUTION, block FIN_CAR, block INIT_BLOCKS, in CAR_MOVE: Control, in OBSTACLE_MOVE: Obstacle_Wait, in ARRIVAL: bool, in FC: LOG_END_CAR, in E: Block_Sent, out UPDATE_POSITION: Edge,

Acknowledgements

Figure 5.3: Architecture of the GRL model of an autonomous car v := {0, 1, 2, 3, 4, 5, 6, 7, 8}; e := {Edge (0, Coronation_Street, 1

), Edge (0, Corporation_Street, 3), Edge (1, Coronation_Street_bis, 0), Edge (1, two_Coronation_Street, 2), Edge (1, Sackville, 4), Edge (2, two_Coronation_Street_bis, 1), Edge (2, Spring_Gardens, 5), Edge (3, Corporation_Street_bis, 0), Edge (3, Princess_Street, 4), Edge (3, two_Corporation_Street, 6), Edge (4, two_Princess_Street, 5), Edge (4, two_Sackville, 7), Edge (5, Spring_Gardens_bis, 2), Edge (5, two_Princess_Street_bis, 4), Edge (5, two_Spring_Gardens, 8), Edge (6, two_Corporation_Street_bis, 3), Edge (6, New_Cathedral_Street, 7), Edge (7, two_Sackville_bis, 4), Edge (7, New_Cathedral_Street_bis, 6), Edge (7, two_New_Cathedral_Street, 8), Edge (8, two_Spring_Gardens_bis, 5), Edge (8, two_New_Cathedral_Street_bis, 7) }; return Graph (v, e) end var end function

The GRL model is instantiated by providing global constants encoding the map, the initial position and destination of the car, and the set of obstacles with their initial positions and lists of movements.

Appendix A Formal Model of the MAA in Lustre

This annex presents the specification of the MAA in the Lustre language. This specification is fully self-contained, meaning that it does not depend on any externally-defined librarywith the minor disadvantage of somewhat lengthy definitions for byte and blocks constants. For readability, the specification has been split into 16 parts, each part being devoted to a particular type, a group of functions sharing a common purpose, or a collection of test vectors. The first parts contain general definitions that are largely independent from the MAA; starting from Section A.10, the definitions become increasingly more MAA-specific. All machine words (bytes, blocks, etc.) are represented according to the "big endian" convention, i.e., the first argument of each corresponding constructor denote the most significant bit.

A.1 Definitions for type Bit

We define bits using an enumeration Bit (X0 and X1), together with functions implementing logical operations on bits.

type Bit = enum {X0, X1}; ----------------------------------------- ----------------------------------------- tel; -----------------------------------------function dropCarryBlockSum (ws: BlockSum) returns (w: Block); let w = ws.w; tel; ------------------------------------------function addBlock (w1, w2 : Block) returns (w: Block); let w = dropCarryBlockSum (addBlockSum (w1, w2)); tel; -----------------------------------------function addBlockHalf (h1: Half; w1: Block) returns (w: Block); let w = addBlock (Block {o1 = x00; o2 = x00; o3 = h1.o1; o4 = h1.o2}, w1); tel; ----------------------------------------- ------------------------------------------A.8 Definitions for Type Pair

We define 64-bit words (named "pair" according to the MAA terminology) using a constructor buildPair that takes two blocks and returns a pair. The main function for this type is mulBlock (which takes two blocks and computes their 64-bit product); using auxiliary functions presented in Section A.6 implementing a 32-bit multiplier built using four 16-bit multipliers defined in Section A.4.

type Pair = struct {w1: Block; w2: Block}; ------------------------------------------let opat = PAT (w1, w2); w = Block {o1 = adjust (w1.o1, rightOctet7 (opat)); o2 = adjust (w1.o2, rightOctet6 (opat)); o3 = adjust (w1.o3, rightOctet5 (opat)); o4 = adjust (w1.o4, rightOctet4 (opat))}; wp = Block {o1 = adjust (w2.o1, rightOctet3 (opat)); o2 = adjust (w2.o2, rightOctet2 (opat)); o3 = adjust (w2.o3, rightOctet1 (opat)); o4 = adjust (w2.o4, opat)}; tel; ----------------------------------------- ------------------------------------------A.11 Definitions (2) of MAA-specific Cryptographic Functions

We define a second set of functions, namely the "multiplicative" functions used for MAA computations. The three principal operations are MUL1, MUL2, and MUL2A.

function MUL1 (w1, w2 : Block) returns (w: Block); var w1w2, w3w4: Pair; let w1w2 = mulBlock (w1, w2); w3w4 = ADDC (w1w2.w1, w1w2.w2); w = addBlock (w3w4.w2, w3w4.w1); tel; -----------------------------------------function MUL2 (w1, w2 : Block) returns (w: Block); var w1w2, w3w4, w5w6: Pair; w3: Block; let w1w2 = mulBlock (w1, w2); w3w4 = ADDC (w1w2.w1, w1w2.w1); w3 = addBlock (w3w4.w2, addBlock (w3w4.w1, w3w4.w1)); w5w6 = ADDC (w3, w1w2.w2); w = addBlock (w5w6.w2, addBlock (w5w6.w1, w5w6.w1)); tel; -----------------------------------------function MUL2A (w1, w2 : Block) returns (w: Block); var w1w2, w3w4: Pair; w3: Block; let w1w2 = mulBlock (w1, w2); w3 = addBlock (w1w2.w1, w1w2.w1); w3w4 = ADDC (w3, w1w2.w2); w = addBlock (w3w4.w2, addBlock (w3w4.w1, w3w4.w1)); tel; ------------------------------------------A.12 Definitions (3) of MAA-specific Cryptographic Functions

We define a third set of auxilary functions used for MAA computations, and the higherlevel functions that implement the MAA algorithm, namely the prelude, the inner loop, and the coda; the two principal functions are MAA (which computes the signature of a nonsegmented message) and MAC (which splits a message into 1024-byte segments and computes the overall signature of this message by iterating on each segment, the 4-byte signature of each segment being prepended to the bytes of the next segment).

function squareHalf (h: Half) returns (w: Block); ------------------------------------------function preludeJ (J1 : Block) returns (J12, J14, J16, J18: Block; J22, J24, J26, J28: Block); let J12 = MUL1 (J1, J1); J14 = MUL1 (J12, J12); J16 = MUL1 (J12, J14); J18 = MUL1 (J12, J16); J22 = MUL2 (J1, J1); J24 = MUL2 (J22, J22); J26 = MUL2 (J22, J24); J28 = MUL2 (J22, J26); tel; -----------------------------------------function preludeK (K1: Block) returns (K12, K14, K15, K17, K19: Block; K22, K24, K25, K27, K29: Block);

returns (H4, H6, H8: Block); let H4 = xorBlock (J14, J24); H6 = xorBlock (J16, J26); H8 = xorBlock (J18, J28); tel; -----------------------------------------function preludeHK (K15, K17, K19, K25, K27, K29: Block; P : Octet) returns (H0, H5, H7, H9: Block); let H0 = xorBlock (K15, K25); H5 = MUL2 (H0, Q (P)); H7 = xorBlock (K17, K27); H9 = xorBlock (K19, K29); tel; -----------------------------------------function prelude (J, K: Block) returns (X, Y, V, W, S, T: Block); var P: Octet; J1, J12, J14, J16, J18, J22, J24, J26, J28: Block; K1, K12, K14, K15, K17, K22, K24, K25, K27, K19, K29: Block; H4, H0, H5, H6, H7, H8, H9: Block; let J1, K1 = BYT (J, K); P = PAT (J, K); J12, J14, J16, J18, J22, J24, J26, J28 = preludeJ (J1); K12, K14, K15, K17, K19, K22, K24, K25, K27, K29 = preludeK (K1); H4, H6, H8 = preludeHJ (J14, J16, J18, J24, J26, J28); H0, H5, H7, H9 = preludeHK (K15, K17, K19, K25, K27, K29, P); X, Y = BYT (H4, H5); V, W = BYT (H6, H7); S, T = BYT (H8, H9); tel; -----------------------------------------

Y, V, W, S, T: Block) returns (Z: Block); var X1, X2, Y1, Y2, V1, V2: Block; let X1, Y1, V1 = mainLoop (X, Y, V, W, S); X2, Y2, V2 = mainLoop (X1, Y1, V1, W, T); Z = xorBlock (X2,Y2); tel; -----------------------------------------node MAC (KJ: Key; Mn: Block) returns (X, Y, V, W, S, T, Z: Block); var X0, Y0, V0: Block; init: bool; n: int; let init = true -> false; n = if init then 1 else if pre n = 256 then 0 else pre n + 1; --initialisations X0, Y0, V0, W, S, T = prelude (KJ.J, KJ.K); --mainloops X, Y, V = if init then mainLoop (X0, Y0, V0, W, Mn)

else if n = 0 then --mode of operations mainLoop2 (X0, Y0, V0, W, pre Z, Mn) else mainLoop (pre X, pre Y, pre V, W, Mn); --coda Z = coda (X, Y, V, W, S, T); tel;

A. 13 ----------------------------------------- -----------------------------------------

We complete the above tests with additional test vectors taken from [ISO90, Annex E.3.3], which only gives detailed values for the first block of the 84-block test message. ------------------------------------------We complete the above tests with additional test vectors taken from from [ISO90, Annex E.3.3], which gives prelude results computed for another key. ----------------------------------------- A.17 Functional Testing of MAA with Lurette

We automate the test execution process, by using the testing tool Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF], for this purpose we added a function selecting a message (get_mess_key), and adapted the main node MAC. ------------------------------------------node MAC (id: int; init: bool) returns (X, Y, V, W, S, T, Z: Block; n: int); var X0, Y0, V0: Block; KJ: Key; Mn: Block; let Mn, KJ = get_mess_key (id); n = if init then 1 else if pre n = 256 then 0 else pre n + 1; --initialisations X0, Y0, V0, W, S, T = prelude (KJ.J, KJ.K); --mainloops X, Y, V = if init then mainLoop (X0, Y0, V0, W, Mn) else if n = 0 then --mode of operations mainLoop2 (X0, Y0, V0, W, pre Z, Mn) else mainLoop (pre X, pre Y, pre V, W, Mn); --coda Z = coda (X, Y, V, W, S, T); tel; -----------------------------------------

Appendix B Formal Model of a Simple Autonomous Car in GRL

This appendix contains the sources for the running example of the Chapter 5. Precisely, this directory contains: the GRL model the autonomous car with required LNT libraries and the the XTL scripts to extract the synchronous test scenarios.

B.1 Definitions for the Synchronous Blocks

We define here each synchronous component of the autonomous car; ACTION, RADAR, DECISION, and GPS as a block. In order to model the environmnet, we also define three others blocks:

• OBSTACLE_EXECUTION block manages an obstacle action.

• INIT_BLOCKS block initialise and print the component information; i.e., the names of their inputs and their initialisation values.

• FIN_CAR block is activated when the car arrived, or a collision occurred between the car and an obstacle, or all obstacles have finished their list of movements. ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- -----------------------------------------

B.2 Definitions for the Asynchronous Mediums

The blocks exchange data via asynchronous communication media, which is represented in GRL as a medium. We define here the mediums POSITION, PATH, and CURRENT_GRID.

- ------------------------------------------ ------------------------------------------- -------------------------------------------

B.3 Definitions for the Asynchronous Environement

The interaction between blocks also respects environmental constraints, each one being represented in GRL as an environment. We present here the environment MAP_MANAGEMENT managing the positions of the car and obstacles on the map. ----------------------------------------------------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ------------------------------------------ ----------------------------------------- ----------------------------------------- ------------------------------------------type Block_Sent is already_values (b1: String, v1: Grid, b2: String, v2: Edge) end type --------------------------------------------Functions ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- ----------------------------------------- --------------------------------------------Radar visibility ----------------------------------------- --------------------------------------------Destination ----------------------------------------- --------------------------------------------Init itinary ----------------------------------------- --------------------------------------------Obstacles ----------------------------------------- --------------------------------------------Functions ----------------------------------------- ----------------------------------------- ------------------------------------------def print info (p1, p3, p5:raw, p2, p4, p6: natural) : action = printf (" and ") fby print (p1) fby printf (" = ") fby print (p2) fby printf (" and ") fby print (p3) fby printf (" = ") fby print (p4) fby printf (" and ") fby print (p5) fby printf (" = ") fby print (p6) end def ------------------------------------------( for init e: edge where init e -> [INITIAL VALUES ?in1:natural ?in2:natural ?in3:natural] apply (replace, replace, replace) from (0, 0, 0) to (in1, in2, in3) end for in -----------------------------------------printf ("node input constraints () returns (s, ") fby print (iv1) fby printf (", ") fby print (iv2) fby printf (", ") fby print (iv3) fby printf (": int) =\n") fby ( * initialisation * ) print (iv1) fby printf (" = ") fby print (in1) fby printf (" and ") fby print (iv2) fby printf (" = ") fby print (in2) fby printf (" and ") fby print (iv3) fby printf (" = ") fby print (in3) fby printf (" and s = 0 fby\n") fby ( * main reactive loop * ) printf ("loop {\n") fby printf (" | pre s = -1 and ") fby print (iv1) fby printf (" = ") fby print (in1) fby printf (" and ") fby print (iv2) fby printf (" = ") fby print (in2) fby printf (" and ") fby print (iv3) fby printf (" = ") fby print (in3) fby printf (" and s = 0\n

C.2 The Generation of Oracles (extract oracle)

We define here the XTL script extract oracle generating the oracles, by encoding CTG C as a deterministic node in Lustre, which, to each corner state and its set of inputs/outputs, associates a Boolean verdict, indicating whether the outputs are the expected ones and also defined for the verdict states coverage of CTG C .

- ---------------------------------------- for init e: edge where init e -> [ALREADY SENT ?already1:natural ?already2:natural] apply (replace, replace) from (0, 0) to (already1, already2) end for in -----------------------------------------printf ("node oracle (s, ") fby print (iv1) fby printf (", ") fby print (iv2) fby printf (", ") fby print (iv3) fby printf (", ") fby print (ov1) fby printf (", ") fby print (ov2) fby printf (": int)\n") fby printf ("returns (res, pass, inconclusive") fby ( * output profile containing all states * ) <| fby on s:state |> ( if ((mod (number (s), 9) = 0) and (number (s) > 0)) then printf (",\n s") else printf (", s") end if fby print (s) ) fby printf (", states covered: bool);\n") fby printf (" (s = 0 and") fby printf ("\n ") fby print (iv1) fby printf (" = ") fby print (in1) fby printf (" and ") fby print (iv2) fby printf (" = ") fby print (in2) fby printf (" and ") fby print (iv3) fby printf (" = ") fby print (in3) fby printf (")\n or") fby ( * default case: no change * ) printf ("\n (") fby print (iv1) fby printf (" = pre ") fby print (iv1) fby printf (" and ") fby print (iv2) fby printf (" = pre ") fby print (iv2) fby printf (" and ") fby print (iv3) fby printf (" = pre ") fby print (iv3) fby printf (" and ") fby print (ov1) fby printf (" = ") fby print (already1) fby printf (" and ") fby print (ov2) fby printf (" = ") fby print (already2) fby printf (")\n") fby printf (" );\n") fby printf (" if s = ") fby print (s) fby printf (" then\n") fby printf (" true\n") fby printf (" else\n") fby printf (" pre inconclusive;\n") ) fby ( * all states coverage * ) <| fby on s:state |> ( printf (" s") fby print (s) fby printf (" = false -> if s = ") fby print (s) fby printf (" then true else pre s") fby print (s) fby printf (";\n") ) fby printf (" states covered = false -> ") fby <| fby on s:state |> ( if ((mod (number (s), 6) = 0) and (number (s) > 0)) then printf ("\n s")