Gurvan Le Guernic

Benoit Combemale

José A Galindo

Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework

Many project-specific languages, including in particular filtering languages, are defined using nonformal specifications written in natural languages. This leads to ambiguities and errors in the specification of those languages. This paper reports on an industrial experiment on using a tool-supported language specification framework (K) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. This experimentation aims at estimating, in a specific industrial setting, the difficulty and benefits of formally specifying a packet filtering language using a tool-supported formal approach.

Introduction

Packet filtering (accepting, rejecting, modifying or generating packets, i.e. strings of bits, belonging to a sequence) is a recurring problematic in the domain of information systems security. Such filters can serve, among other uses, to reduce the attack surface by limiting the capacities of a communication link to the legitimate needs of the system it belongs to. This type of filtering can be applied to network links (which is the most common use), product interfaces, or even on the communication buses of a product. If the filtering policy needs to be adapted during the deployment or operational phases of the system or product, it is often required to design a specific language L (syntax and semantics) to express new filtering policies during the lifetime of the system or product. This language is the basis of the filters that are applied to the system or product. Hence, it plays an important role in the security of this system or product. It is therefore important to have strong guarantees regarding the expressivity, precision, and correctness of the language L (meaning that everything that need to be expressed can, and that everything that can be expressed has the most obvious semantics). Those guarantees can be partly provided by a formal design (and development) process.

Among diverse duties, the DGA (Direction Générale de l'Armement, a french procurement agency) is involved in the supervision of the design and development of filtering components or products. Those filters come in varying shapes and roles. Some of them are network apparatuses filtering standard Internet protocol packets (such as firewalls); while others are small parts of integrated circuits filtering specific proprietary packets transiting on computer buses. Their common definition is: "a tool sitting on a communication channel, analyzing the sequence of packets (strings of bits with a beginning and an end) transiting on that channel, and potentially dropping, modifying or adding packets in that sequence". Whenever the filtering algorithm applied is fixed for the lifetime of the component or product, this algorithm is often "hard coded" into the component or product with the potential addition of a configuration file allowing to slightly alter the behavior of the filter. However, sometimes the filtering algorithm to apply may depend on the deployment context, and may have to evolve during the lifetime of the component or product to adapt to new uses or attackers. In this case, it is often necessary to be able to easily write new filtering algorithms for the specific product and context. Those algorithms are then often described using a Domain Specific Language (DSL) that is designed for the expression of a specific type of filters for a specific product. The definition of the syntax and semantics of this DSL is an important task. This DSL is the link between the filtering objectives and the process that is really applied on the packet sequences. Often, language specifications (when there is one) are provided using natural language. In the majority of cases, this leads to ambiguities or errors in the specification which propagate to implementations and final user code. This is for example the case for common languages such as C/C++ or Java™ [START_REF]JSR-133 Java™ Memory Model and Thread Specification Revision. Java Specification Request (JSR)[END_REF].

"Unfortunately, the current specification has been found to be hard to understand and has subtle, often unintended, implications. Certain synchronization idioms sometimes recommended in books and articles are invalid according to the existing specification. Subtle, unintended implications of the existing specification prohibit common compiler optimizations done by many existing Java virtual machine implementations. [...] Several important issues, [...] simply aren't discussed in the existing specification."

JSR-133 expert group [START_REF]JSR-133 Java™ Memory Model and Thread Specification Revision. Java Specification Request (JSR)[END_REF] Some of those ambiguities, as the memory model of multi-threaded Java™ programs [START_REF]JSR-133 Java™ Memory Model and Thread Specification Revision. Java Specification Request (JSR)[END_REF], required a formal specification in order to be solved. This paper is an industrial experience report on the use of a tool-supported language specification framework (the K framework) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. The tool used to formally specify the DSL is introduced in Sect. 2. For confidentiality reasons, in order to be allowed by the DGA to communicate on this experimentation, the language specified for this experiment is not linked to any particular product or component. It is a generic packet filtering language that tries to cover the majority of features required by packet filtering languages. This language is introduced in Sect. 3 while its formal specification is described in Sect. 4. This language is tested in Sect. 5 by implementing and simulating a filtering policy enforcing a sequential interaction for a made-up protocol similar to DHCP. Before concluding in Sect. 7, this paper discusses the results of the experimentation in Sect. 6.

Introduction to the K Framework

Surprisingly, even if it is a niche for tools, there exists quite a number of tools specifically dedicated to the formal specification of languages (our focus in this work is on specifying rather than implementing DSLs). Those tools include among others: PLT Redex [START_REF] Felleisen | Semantics Engineering with PLT Redex[END_REF][START_REF] Klein | Run Your Research: On the Effectiveness of Lightweight Mechanization[END_REF], Ott [START_REF] Sewell | Ott: Effective Tool Support for the Working Semanticist[END_REF], Lem [START_REF] Mulligan | Lem: Reusable Engineering of Real-world Semantics[END_REF], Maude MSOS Tool [START_REF] Chalub | Maude MSOS Tool[END_REF], and the K framework [START_REF] Roşu | An Overview of the K Semantic Framework[END_REF][START_REF] Traian Florin Şerbȃnuţȃ | The K Primer (version 3.3)[END_REF]. All those tools focus on the (clear formal) specification of languages rather than their (efficient) implementation, which is more the focus of tools and languages such as Rascal [START_REF] Klint | RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation[END_REF][START_REF] Basten | Modular Language Implementation in Rascal -Experience Report[END_REF][START_REF] Klint | RLSRunner: Linking Rascal with K for Program Analysis[END_REF] or its ancestor The Meta-Environment [START_REF] Klint | Tribute to a great Meta-Technologist: from Centaur to The Meta-Environment[END_REF][START_REF] Van Der Storm | Using the Meta-Environment for Domain Specific Language Engineering[END_REF], Kermeta [START_REF] Jézéquel | Summer School on Generative and Transformational Techniques in Software Engineering, chapter Model Driven Language Engineering with Kermeta[END_REF][START_REF] Jézéquel | Mashup of metalanguages and its implementation in the Kermeta language workbench[END_REF], and others. PLT Redex is based on reduction relations. PLT Redex is an extension (internal DSL) of the Racket programming language [START_REF] Flatt | Reference: Racket[END_REF]. Ott and Lem are more oriented towards theorem provers. Ott and Lem allow to generate formal definitions of the language specified for Coq, HOL, and Isabelle. In addition, Lem can generate executable OCaml code. Ott is more programming language syntax oriented, while Lem is a more general purpose semantics specification tool. Ott and Lem can be used together in some contexts. The Maude MSOS Tool, whose development has stopped in 2011, is based on an encoding of modular structural operational semantics (MSOS) rules into Maude. Similarly to the Maude MSOS Tool, the K framework is based on rewriting and was also originally implemented on top of Maude.

The goal set for the experiment reported in this paper is to estimate the difficulty and benefits for an average engineer (i.e. an engineer with education and experience in computer science but no specific knowledge in formal language semantics) to use an "appropriate" tool for the formal specification of a packet filtering language. The "appropriate" tool needs to: be easy to use; be able to produce (or take as input) "human readable" language specifications; provide some level of correctness guarantees for the language specified; and be executable (simulatable) in order to test (evaluate) the language specified. The K framework seems to meet those requirements and has been chosen to be the "appropriate" tool after a short review of available tools. As there has been no in depth comparison of the different tools available, there is no claim in this paper that the K framework is better than the other tools, even in our specific setting.

This section introduces the K framework [START_REF] Roşu | K Overview and SIMPLE Case Study[END_REF] by relying on the example of a language allowing to compute additions over numbers using Peano's encoding [START_REF] Van Heijenoort | From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931[END_REF]. The K source code of this language specification is provided below. A K definition is divided into three parts: the syntax definition, the configuration definition, and the semantics (rewriting rules) definition. The definition of the language syntax is given in a module whose name is suffixed with "-SYNTAX". It uses a BNF-like notation [START_REF] Backus | The Syntax and Semantics of the Proposed International Algebraic Language of the Zurich ACM-GAMM Conference[END_REF][START_REF] Knuth | Backus Normal Form vs. Backus Naur Form[END_REF]. Every non-terminal is introduced by a syntax rule. For example, the definition of the notation for numbers (Nb) in this language, provided on line 2, is equivalent to the definition given by the regular expression "(Succ) * Zero".

• Map env $PGM:K k Figure 1: Peano's K configuration
The configuration definition part is introduced by the keyword configuration and defines a set of (potentially nested) cells described in an XML-like syntax. This configuration describes the "abstract machine" used for defining the semantics of the language. The initial state (or configuration) of the abstract machine is the one described in this configuration part. The parsed program (using the syntax definition of the previous part) is put in the cell containing the $PGM variable (of type K). For the Peano language, the env cell is used to store variable values in a map initially empty (.Map is the empty map). From this definition, the K framework can produce a graphical representation of the configuration, provided in Fig. 1 The semantics definition part is composed of a set of rewriting rules, each one of them introduced by the keyword rule. In the K source file, rules are roughly denoted as "CCF => NCF" where CCF and NCF are configuration fragments. The meaning of "CCF => NCF" can be summarized as: if CCF is a fragment of the current abstract machine state (or configuration) then the rule may apply and the fragment matching CCF in the current configuration would then be replaced by the new configuration fragment NCF. In order to increase the expressivity of rules, CCF may contain free variables that are reused in expressions in NCF. If a specific valuation of the free variables V in CCF allows a fragment of the current configuration to match CCF, then this fragment may be replaced by NCF where the variables V are replaced by their matching valuation.

The rules for addition over numbers (Nb and not Exp), on lines 15 and 16, follows closely this representation. For those rules, CCF is a program fragment that can be matched in any cell of the configuration. For those two rules, the K framework can then produce the following graphical representations:

RULE N:Nb + Zero N RULE N1:Nb + Succ N2:Nb ( Succ N1) + N2
For other rules, the configuration fragment matching is more complex and involves precise configuration cells that are explicitly identified. In order to compress the representation, CCF and NCF are not stated separately anymore. The common parts are stated only once, and the parts differing are again denoted "CCF i => NCF i ", where CCF i is a sub-fragment in CCF and NCF i is the corresponding sub-fragment in NCF. Cells that have no impact on a rule R and are not impacted by R do not appear explicitly in the rule. Cells heads and tails (potentially empty) that are not modified by a rule can be denoted "...", instead of using a free variable that would not be reused.

For example, the rule which starts on line 18is the rule used to evaluate variables. The current configuration needs to contain a mapping from a variable Var to a value Val ("X |-> V" denotes a mapping from X to V) somewhere in the map contained in the env cell. It also needs to contain the variable Var at the beginning of cell k. This rule has the effect of replacing the instance of Var at the beginning of cell k by the value Val. For this rule, the K framework generates the graphical representation given in Fig. 2.

The last rule on line 31 involves other internal aspects of the K framework. It roughly states that, in order to evaluate a statement S followed by the rest P of the program, S must first be evaluated to a KResult (defined on line 9) and then P is evaluated. The language specified in the experiment reported in this paper, named GPFL, is a generic packet filtering language. For confidentiality reasons, GPFL is not a language actually used in any specific real product. GPFL has been made-up in order to be able to communicate on the experimentation on tool supported formal specification of filtering languages reported in this paper. However, GPFL covers the majority of features needed in packet filtering languages dealt with by the DGA. GPFL can be seen as the "mother" of the majority of packet filtering languages.

GPFL Context

GPFL aims at expressing a wide variety of filters. Those filters can be placed at the level of network, interfaces, or even communication buses between electronic components. They can be applied on standard protocols such as IP, TCP, UDP, . . . or on proprietary protocols, which are more common for component communication protocols. However, all those filters are assumed to be placed on a communication link. Messages (packets) that get through the filter can only get through in two ways, either "going in" or "going out"; there is no switching taking place in GPFL filters. Those different use cases are illustrated in Fig. 3. GPFL focuses on the internal logic of the filter. Decoding and encoding of packets is assumed to be handled outside of GPFL programs (filters), potentially using technologies such as ASN.1 [START_REF]Information technology, Subcommittee SC 6, Telecommunications and information exchange between systems[END_REF][START_REF] Dubuisson | ASN.1 -Communication between Heterogeneous Systems[END_REF]. For GPFL programs, a packet is a record (a set of valued fields). A GPFL program (dynamically) inputs a sequence of records and outputs a sequence of records. Figure 4 describes the architecture of GPFLbased filters. An incoming packet (on either side) is first parsed (decoded) before being handed over to the GPFL program. If the packet can not be parsed, depending on the type of filter (white list or black list), the packet is either dropped or passed to the other side without going through the GPFL program. Any packet (record) output by the GPFL program (on either side) is encoded before being sent out. In addition, the GPFL program can generate alarms due to packets not complying with the encoded filtering policy. The GPFL language must allow to: drop, modify or accept the current packet being filtered; generate new packets; and generate alarms. GPFL must allow to base the decision to take any of those actions on information pieces concerning the current packet being filtered and previously filtered packets. Those information pieces must include: some timing information, current or previous packets directions through the filter ("in" or "out"), and characteristics of current or previous packets including field values and computed properties such as, for example, a packet "type" or total length. The computation of those properties and decoding of packet fields is outside of the scope of GPFL; it is left to the decoders.

GPFL Filter

In order to gradually build a decision, GPFL must allow to interact with variables (reading, writing, and computing expressions) and automata (triggering a transition in an automaton and querying its current state). The intent for automata is to be used to track the current step of sessions of complex protocols. GPFL must allow to combine filtering statements using: sequential control statements (executing two statements in sequence); conditional control statements (executing a statement only if a condition is true); iterating control statements (repeatedly executing a statement for a fixed number of repetitions). There is no requirement for a loop (or while) statement whose exit condition is controlled by an expression recomputed after every iteration. For the experiment reported in this paper (on formal specification of a filtering language), the iterating statement is considered sufficient for the intended use of GPFL and close enough to a loop statement from a semantics point of view, while exhibiting interesting properties for future analyses (for example, any GPFL program terminates).

GPFL's Specification

Due to lack of space, GPFL's specification and testing is only summarized in this paper. However, a full specification of GPFL and a testing section can be found in the companion technical report [START_REF] Le Guernic | Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework[END_REF]. Syntax. To the exception of expressions and expression fragments, GPFL's syntax is formally defined by the K source fragment provided below. 18 syntax Cmd ::= " nop " | " accept " | " drop " | " send ( " Port " ," Fields " ) "

| " alarm ( " Exp " ) " [ strict (1) ]

20

| " set (" Id " ," Exp " ) " [ strict (2) ] | " newAutomaton ( " String " ," AutomatonId ") "

22

| " step ( " AutomatonId " ," Exp " ," Stmt " ) "

[ strict (2) ] syntax Stmt ::= Cmd A GPFL program is composed of a prologue, executed only once in order to initialize the execution environment, and a filter statement, executed once for every incoming packet. A prologue is composed of automaton kind definitions and initialization sequences. An automaton kind definition specifies an identifier K, an initial state for automata of kind K and a set of transitions for automata of kind K. A transition definition is composed of: two automaton states F and T , and an automaton event that triggers the transition from F to T .

A GPFL statement is composed of GPFL commands or statements combined sequentially. Some statements can be guarded by an expression and executed only if that expression evaluates to true (cond). Some statements (iter), associated with an expression e, are exectued v times, where v is the value of e before the first iteration. Finally, newInterrupt statements register a statement to be executed in the future, potentially periodically.

GPFL commands are the basic units having an effect on the execution environment. The nop command has no effect and serves mainly as a place holder. The accept, resp. drop, command states to accept, resp. drop, the current packet and stop the filtering process for this packet. The send command sends a packet on one of the ports. The alarm command generates a message on the alarm channel. The set command sets the value of a variable. The newAutomaton command initializes an automaton of the provided kind, and assigns this newly created automaton to the provided identifier. The step command tries to trigger an automaton transition by sending an event e to an automaton a. If there is no transition from the current state of a triggered by the event e, then the associated statement is executed.

Semantics The full formal specification of GPFL's semantics can be found in the companion technical report [START_REF] Le Guernic | Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework[END_REF]. GPFL's semantics rules are defined on the configuration presented graphically in Fig. 5. The prg cell contains the GPFL program. After initialization of the program, automaton kind definitions are stored in the automatonKindDefs cell and the filter cell contains the filter (GPFL statement)

$PGM:K prg • K automataKind • K initialState • Map transitions automataKindDef* automataKindDefs • K lter • List nextInterrupts • K intTime • K intCode • K period interrupt* interrupts • K k 0 clock • K inHead • List inTail in • List alarm • List out streams • K time • K port • Map elds input • Map kinds • Map states automata • Map vars env Figure 5: K configuration of GPFL
that is to be executed for every packet. The interrupts cell contains a set of interrupt definitions (interrupt*). An interrupt is a triplet composed of: the time when the interrupt is to be triggered, the code (statement) to be executed, and a "Time" value equal to the interruption period for a periodic interruption (or nothing for a non-periodic interruption). In addition, the interrupts cell contains an ordered list of the next "times" when an interrupt is to be executed. The clock cell registers the current "time". The configuration also contains a k cell that holds the GPFL statement under execution. Each time a new packet is input, the content of the k cell is replaced by the content of the filter cell, and the newly arrived packet is stored in the input cell with its arrival time and port. Packets are input from the streams cell which contains: the packet input stream divided into the next packet to arrive (inHead) and the rest of the stream (inTail); the packet output stream; and the alarm output stream. In the input stream, resp. output stream, packets arriving, resp. leaving, on both ports are mixed together, but contains information on the port of entry, resp. exit. Some choices made to represent those streams are not an intrinsic part of GPFL's formal specification. The division of the input stream into a head and a tail is such a choice. Those choices are made in order to be able to execute the specification. It is then required to implement, in the K framework, a mechanism to retrieve and parse strings describing packet sequences sent to the filter. In order to help distinguish between the formal specification of GPFL and the mechanisms put in place to execute it, whenever possible, implementation choices, such as the format of strings describing packets, are defined in another file which is loaded in the main specification file with the require instruction.

Finally, the env cell is the main dynamic part of the execution environment. It corresponds to a "record" of maps that associate: automaton kind and current state to automaton identifiers (automata cell); and values to variables.

Testing GPFL's Specification

GPFL's specification, introduced above and contained in the companion technical report [START_REF] Le Guernic | Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework[END_REF], is not necessarily perfect. By a matter of fact, imperfections of GPFL's specification are of interest to the experimentation reported in this paper. Indeed, the goal of the experimentation is to see how a tool such as the K framework can help to spot and correct imperfections in filtering language specifications. One way to do so is by "testing" the new language specified, which is possible if the framework used to specify the language supports the execution or simulation of language specifications, which is the case for the K framework.

The test scenario used assumes a network of clients and servers. The clients request resources to servers using a made-up protocol, called "DHCP cherry", summarized in Fig. 6 sumes that servers behave poorly when interacting concurrently with different clients. The objective of the test scenario is then to filter communications in front of servers in order to prevent any concurrent client-server interactions with any given server. This test scenario is obviously made-up for this experimentation, which is a requirement due to confidentiality issues. However, it is still covering the most frequently used features of filtering languages similar to GPFL, while remaining simple enough for a first experimentation.

From the point of view of servers, non-concurrent interactions are sequential instances of only three generic atomic packet sequences. Those atomic packet sequences are the ones accepted by the automaton in Fig. 7. In this automaton, "in:MP", resp. "out:MP", is a transition trigger matching any incoming Figure 7: Automaton of server-side atomic packet sequences packet (from the rest of the network to the server), resp. outgoing packet, matching packet pattern MP. C, resp. R, is a client, resp. ressource, identifier variable. C, resp. R, has to be instantiated in the same way (have the same value) for any packet of the same atomic packet sequence accepted by the automaton. The automaton of Fig. 7 is refined into a filtering policy automaton described in Fig. 8. Variables C and R have the same constraints as for the automaton of Fig. 7. The variable " * " matches any value, packet pattern "out: * " matches any outgoing packet, and packet pattern "out: * -Ack(C)" matches any outgoing packet except Ack(C). This filtering policy accepts every outgoing packet; thus having no Figure 8: Filtering policy automaton effect on the packets generated by the server. For incoming packets, if the current state of the automaton has no transition whose trigger matches the packet then the packet is discarded; otherwise, the packet is accepted and the associated transition is triggered. This filtering policy assumes that clients comply with the DHCP cherry protocol and ensures only that the filtered server only interacts sequentially with clients. If there is no idle server ready to receive a packet from a client, this client gets no answer and is expected to retry later. This policy has been encoded in GPFL and executed using the following command (in Linux Bash): "krun dhcp.gpfpl < dhcp_input-dataset.txt > dhcp_output.txt" where the file dhcp_input-dataset.txt contains a sequence of packets already "parsed" (decoded packets, Fig. 4) input to the filter. The output of the simulation of the code (dhcp.gpfpl) written in the specified language (GPFL) is written in dhcp_output.txt.

Discussion on the Experimentation

The primary goal of this paper is not to set out the filtering policy described in Sect. 5 or, even, GPFL's specification described in Sect. 4. This paper is an industrial experience report on a primary evaluation of the cost and benefits of using formal specification tools in general, and the K framework in particular, to formally specify the syntax and semantics of filtering languages. Overall, it seems to the authors that using the K framework helped greatly to improve GPFL's specification quality. It forced the specification authors to be precise, and helped spot various errors and missing specification fragments.

With regard to the "cost", this experimentation argues in favor of tool supported formal specifications for high quality specifications of filtering languages. Of course, using natural language, it is possible to produce a cheaper, but ambiguous and approximate, specification. However, from the authors' natural language based experiences with packet filtering language specifications, using natural language to produce a specification with a similar level of precision and correctness would be more costly for engineers with operational semantics knowledge. With a decent knowledge of operational semantics concepts, the cost for newcomers to the K framework is relatively low, thanks to the numerous tutorials (in text and video), manuals and examples. In fact, having been exposed to operational semantics concepts (apart from general computer science concepts) seems to be the only prerequisite to efficiently using the K framework.

From the authors' previous experiences at formal specification of packet filtering language specifications without tool support, the cost of the constraints imposed by the K framework seems to the authors to be lower than the benefits provided by the tool support. Typically, the ability to simulate1 the formal specification of the filtering language requires a particular handling of input/output related rules. However, this same ability to simulate the formal specification of the filtering language is highly beneficial when validating the correctness of the specification and expressivity of the language by "executing" test and documentation programs.

Other benefits of tool supported formal specifications of languages are numerous. In natural language documents specifying new languages, it is too common for program examples to be inconsistent with the language grammar. It is easily explained by the modifications brought to the language grammar during the specification document development. Examples directly related to the modified statements are usually modified accordingly. However, examples related to other aspects of the language are often forgotten. Using a tool supported formal specification, it is easy to adopt a "continuous/frequent integration" approach where examples are: written in separate files, regularly parsed to verify that they comply with the current grammar, and automatically imported in the specification document (the creation of this paper used this approach).

Additionally, use of a tool-supported formal specification approach modifies the workflow often applied when using natural language specification documents. With natural language specifications, the specification document writing process usually starts early after a short engineering phase (it may not be true for a language development process, however it is often the case in pure language specification processes), and the main part of the language specification is done during the specification document writing process. With a tool-supported formal specification approach, the specification of the language tend to be first developed inside the tool, and then the language specification is clarified during the specification document writing process. With a tool-supported formal specification approach, the language specification becomes a two phases process with two different views on the language specification. The "two different views" aspect is particularly true with the K framework were semantics rules are entered textually in the source file and can be rendered graphically for the specification document. This two phases workflow (development then clarification and documentation) helps spot: differences of treatments (in particular for configuration cells), generalization and reuse opportunities (for example, in this experimentation, the use of only two internal commands, iSend and iHalt, to encode the three packet commands accept, drop and send), different concepts that are candidates to modularization (for example, in this experimentation, the externalization of packet data type definitions and string conversions), errors that manifest themselves in rare occasions (for example, in an earlier version of GPFL, automaton states and variable values where stored in the same map, which could trigger a key clash caused by variable and automaton identifiers having the same "name" part), or general simplifications (for example, during this report writing process, GPFL's configuration has been heavily reformatted to simplify the language specification and be closer to the concepts manipulated). From the authors experience, in general and compared to a natural language approach, a tool-supported formal specification process helps simplify and clarify a language specification. Moreover, the ability to execute the formal specification allows to adopt an incremental approach for the specification of the different statements semantics. In such an approach, the syntax of the language is first specified. Then a program example making use of all the statements of the language in as much context as reasonable is written. The semantics of the statements is then defined statements by statements. The program is executed using K's run time; and the execution stops when reaching a statement whose semantics is not defined yet. All the semantics rules associated to this statement are then defined. When stopping an execution, K's run time displays the current state of the configuration which can help specify the missing semantics rules. As the test program execution goes further and further during the language semantics specification process, this incremental approach is more rewarding for people in charge of the specification. The impact of using this incremental approach (which is not required by the K framework) on the quality of the specifications produced remains to be investigated.

Finally, the ability to execute the formal specification allows to test and validate the language specification. Two important points to validate are: the expressivity of the language and its expected semantics. GPFL's test code (Sect. 5) provided in the companion technical report [START_REF] Le Guernic | Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework[END_REF] emphasizes the limitations of the simple automata that can be defined using GPFL. It could be useful to have automaton state variables, and triggering conditions that test and check automaton state variable values. However, adding automaton state variables would complexify automata definitions. Similarly, GPFL's test code contains a recurring code sequence to handle alarms which is triggered only when a threshold of a specific event occurrences is reached. It could be useful to add a specific command to GPFL which would have the same semantics as this recurring sequence. The ability to test programs does not solve expressivity questions (which have to be answered on a per language basis), however it helps explicit those questions. With regard to expected semantics, writing test programs helps validate that programs have the semantics that users would expect. The initial version of GPFL's test code did not behave as expected. It ended up being a misplaced statement in the filter code, but could also have been a problem with the semantics specification. Discovering the cause of a misbehavior of a test program (error in the semantics or the program) could be greatly simplified by K's debugger which can "execute" formal specifications step by step; especially as Domain Specific Languages (specifications and implementations) usually have limited debugging facilities (which is in accordance with their philosophy of limited expressivity for the sake of simplification). However, sadly, K's debugger crashed on our program with the version of the K framework used for this experimentation (version 3.6). This can be explained by the fact that K development effort was focused on the next version to come (version 4.0 which exited the beta stage at the end of July 2016). Finally, the ability to execute the formal specification helps to validate a set of test programs that can be used as smoke test for language implementations.

Conclusion

This paper reports on an industrial experiment to formally specify the syntax and semantics of a filtering language (GPFL) using the tool-supported framework K. For confidentiality reasons, the filtering language specified in this report has been made up for this experimentation; however, it covers the majority of concepts usually encountered in filtering languages. No comparison between different tools is made in this experiment. The goal of the experiment is to study the feasibility of using a tool-supported formal approach for the specification of domain-specific filtering languages having a complexity similar to filtering languages encountered in real-life projects.

The K framework proved to be sufficiently expressive to naturally express the syntax and semantics of GPFL in a formal way. The effort required by this formal specification is judged reasonable by the authors, and within reach of average engineers which have been exposed previously to operational semantics theories. Newcomers life is made easier by the numerous manuals, examples and tutorials available for the K framework. The tool support is a welcome help during the specification process. In particular, the ability to execute (or simulate) K formal specifications helps greatly when developing and fine tuning the language specification, and when producing smoke tests for the implementation.

Following such a specification process may seem to be in complete contradiction to any agile development principles [START_REF] Cockburn | Agile Software Development: The Cooperative Game[END_REF]. However, using a tool-supported executable specification methodology allows to comply with one of the pillars of agile development: early feedback. As the language specification is executable, it is possible to ask final users (if some are available) to test the language and provide feedbacks on different aspects of the language, including its expressivity. In fact, IBM's Continuous Engineering development methodology [START_REF] Shamieh | Continuous Engineering For Dummies ®[END_REF] advocates for the use of executable models at every steps of the development.

To summarize, with regard to the benefits of putting the effort to produce a formal specification, the authors opinion, on improved quality and usefulness of formal specifications compared to non formal specifications written in natural language, is relatively well summarized in the following statement by David Schmidt [START_REF] Schmidt | Programming Language Semantics[END_REF], which is supported by the numerous ambiguities (and their consequences) in natural language specifications of common programming languages like C/C++ or Java [START_REF]JSR-133 Java™ Memory Model and Thread Specification Revision. Java Specification Request (JSR)[END_REF].

"Since data structures like symbol tables and storage vectors are explicit, a language's subtleties are stated clearly and its flaws are exposed as awkward codings in the semantics. This helps a designer tune the language's definition and write a better language manual. With a semantics definition in hand, a compiler writer can produce a correct implementation of the language; similarly, a user can study the semantics definition instead of writing random test programs." David Schmidt in ACM Computing Surveys [START_REF] Schmidt | Programming Language Semantics[END_REF] In the experimentation reported in this paper, no formal analysis of the formal specification produced has been attempted. In future work, the authors plan to try some of the experimental tools available with the K framework on GPFL's specification. If time allows, a similar experimentation could be repeated with other tools oriented toward the formal specification of languages.

1

  module PEANO -SYNTAX syntax Nb ::= " Zero " | " Succ " Nb 3 syntax Exp ::= Nb | Id | Exp "+" Exp [ strict , left ] syntax Stmt ::= Id " := " Exp ";" [ strict (2) ] 5 syntax Prg ::= Stmt | Stmt Prg endmodule 7 module PEANO imports PEANO -SYNTAX 9 syntax KResult ::= Nb 11 configuration < env color =" green " > . Map </ env > 13 <k color =" cyan " > $PGM :K </k > 15 rule N : Nb + Zero => N rule N1 : Nb + Succ N2 : Nb => ( Succ N1 ) + N2 17 rule 19 <env > ... Var : Id |-> Val : Nb ... </ env > <k > ( Var : Id = > Val : Nb ) ... </k > 21 rule 23 <env > Rho : Map (. Map = > Var | -> Val ) </ env > <k > Var : Id := Val : Nb ; => . ... </k > 25 when notBool ( Var in keys ( Rho ) ) 27 rule <env > ... Var |-> ( _ = > Val ) ... </ env > 29 <k > Var : Id := Val : Nb ; => . ... </k > 31 rule S : Stmt P : Prg => S ~> P [ structural ] endmodule

Figure 2 :

 2 Figure 2: Peano's K rule for variables

Figure 3 :

 3 Figure 3: Use cases for GPFL-based filters

Figure 4 :

 4 Figure 4: Architecture of GPFL-based filters

24 | 26 |

 2426 " cond ( " Exp " ," Stmt " ) " [ strict[START_REF] Backus | The Syntax and Semantics of the Proposed International Algebraic Language of the Zurich ACM-GAMM Conference[END_REF] ] | " iter ( " Exp " ," Stmt " ) "[ strict[START_REF] Backus | The Syntax and Semantics of the Proposed International Algebraic Language of the Zurich ACM-GAMM Conference[END_REF] ] " newInterrupt ( " Int " ," Bool " ," Stmt " ) " := " AUTOMATA " String AutomataDefTail syntax AutomataDefTail ::= " init " "= " AStateId ATransitions | ATransitions 32 syntax ATransitions ::= List { ATransition , " " } syntax ATransition ::= AStateId " -" AEvtId " ->" AStateId 34 syntax AStateId ::= String syntax AEvtId ::= String 36 syntax InitSeq ::= " INIT " Stmt syntax PrologElt ::= AutomataDef | InitSeq 38 syntax Prologues ::= PrologElt | PrologElt Prologues 40 syntax Program ::= " PROLOGUE " Prologues " FILTER " Stmt

Figure 6 :

 6 Figure 6: Nominal packet sequences of DHCP cherry protocol

  . The test scenario as-

	msc Nominal acquire sequence
	Server 1	Client	Server 2
	Server	Client	Server	msc Nominal release sequence
	Disc	Disc		Server 1	Client
	Off(R1)	Off(R2)	Server	Client
	Req(R1)	Rej(R2)	Rel(R1)
		Ack
	locks R1			unlocks R1
	Ack			Ack

The authors prefer to talk of "simulation" rather than "execution", as the loading time of the execution environment and limited ability to interact with other components would most likely prevent to use such an execution in a real world setting.


Jacques Roubaud Geneviève

Geneviève Guétemme

Roubaud Jacques

Jacques Roubaud

He

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

writing has been continuously entwining his double interest. His first book of poetry, for example, published in 1966 by Gallimard and called ∈ (Sign of belonging), is a collection of mathematically structured sonnets -the use of a fixed form, especially the sonnet, about which he published several books, being a constant in his work.

With this publication, he was inducted into the Oulipo (Ouvroir de littérature potentielle -"workshop" of potential literature), under the tutelage of co-founder Raymond Queneau who was also passionate about mathematics.

His mathematic and literary experience involves numbers, calculations and walks. Je marche. Je mâche l'air avec mes pieds, je médite l'espace en arpentant la terre, ses routes, ses rues, ses sentiers, ses chemins. [I walk. I chew the air with my feet, I meditate while walking the earth, its roads, its streets, its trails, its paths.] ('le grand incendie de londres ', 119-120) From his walks, comes a poetry that mimic the fatal rhythmical alternation of (as he puts it) the prosodic arsis and thesis ('le grand incendie de londres ', 1299). For him, language works like a musical line and the numerically determined accents and measures act on memory. This can be illustrated in the research he did with Jacques Lusson for a particular abstract rhythm Theory (T.R.A.(M,m): question d'une poétique formelle).

Le Flip-flop du lever-tomber du pied droit puis du pied gauche, et réciproquement (est-il iambique ou trochaïque ? Cela dépend du point de vue), se transmet au cerveau, où il suscite l'éveil des images, des images de mémoire, les images-mémoire qui sont la matière première de la poésie. [The Flip-flop of Literary Encyclopaedia -http://www.litencyc.com/php/speople.php?rec=true&UID=13139 2 the raise-fall from the right foot and left foot, and vice versa (is it iambic or trochaic? It depends on the point of view), is transmitted to the brain, where it causes the awakening of images, pictures of the memory, memory-images which are the raw material of poetry.] ('le grand incendie de londres', 1300) Each walk comes with a rule, which removes its predictability while the rules often have to do with numbers or counting. One of these rules, for example, is to note Parisian number plates in ascending order while walking. At other times, Roubaud Here, "Lazaréen" relates to the Parisian train station St Lazare, but also makes the poetry born out of the route 29, a sequel of the Lazarus myth. It transforms the moving poetry -from bus-stop to bus-stop -into a miraculous resurrection from the dead or, less dramatically, into a way of bringing places, people or texts from the past (his own and everyone's past) back to light. This structured poetical motion through past spaces and times is part of his work with the Oulipo. Indeed, the modus operandi of the group: raising formal constraints, create new ones, use them and sometimes, come up with a clinamen (a deviation or creative inflection from the rule) when falling into deadlocks, is not just a game with literature and language. It helps to bring back personal and cultural memories. The rule, Joséphine, he invented in 2006 for example, and named after the mathematician Flavius Josephe (Histoire des Juifs, 79 AD), allows him to define an upward and downward poetical form of permutation where a word-rhyme is successively deleted from each verse following the order of the permutation. It therefore relates poetry to a Literary Encyclopaedia -http://www.litencyc.com/php/speople.php?rec=true&UID=13139 3 mathematical decimation problem that was a life and death problem. He also invented the Mongine (2006), another rule of permutation inspired by Monge, the 18 th century French mathematician and, more famously, the n-nine. This rule is related to the quenine invented by Queneau as an extension of the sextine, a very structured medieval form written in the Romance language of Old Occitan with six stanzas of six lines of six words, changing places on each line, following a combinatorial model. All these rules bring back past mathematical and poetical structures, as well as old names and texts to the present time. But they also draw the self-portrait of a mathematician who sees himself as a descendant of the troubadours. More generally, they put him in line with a very old tradition in literature and in the arts at large: a tradition of erudition that helps the past shape our language and our future.

For Jacques Roubaud, poetic innovation is indeed a matter of proofreading the past (the sonnet being one of its most exemplary forms) and he describes his working method as such: J'imagine, je lis, je compose, j'apprends, je recopie, je traduis, je plagie, j'écris de la poésie depuis près de quarante ans. Il m'arrive d'en publier. [I guess, I read, I write, I learn, I copy, I translate, I plagiarize, I write poetry for nearly forty years.

Sometimes I publish.] (Cahiers de Poétique Comparée, Mezura n°9)

Comparing himself as an earthworm, working and tilling the field of poetry, "as his father and grandfather before" (Les Animaux de tout le monde, 10), his aim is to perpetuate and help evolve the forms he admires the most -the sonnet or the tanka (its Japanese double) being some of them. He wants to go backwards to reach the "sharpness and minimal complexity of form" ('le grand incendie de londres', 1380).

Or, to say it differently, his idea is to reach "the node of the error, to take a different path" ('le grand incendie de londres', 1381). Like Queneau working before him on the medieval sextine and far from the surrealism or from the modernist ideal of clean slate, Roubaud wants to invent a new poetry through an act of memory. This work, according to Roubaud himself, started in February 1962 ('le grand incendie de londres', 1439) after a dream he had (following the death of his brother). This dream gave him the title of a novel he should write: The Great fire of London and this novel became his Project. "composer of mathematics and of poetry". It was based on a system of constraints related to mathematics and minstrel poetics, but was later abandoned and redeveloped into another 'project' -a "minimal project" as Roubaud calls it: still really huge, but much more ambiguous. This new 'project', is a 'false' autobiography that allows him to say "I" and recall different episodes of his own life, his successes and his failures, but that is never only about him. It is more the intellectual autobiography of an author currently writing and explaining how his thoughts on poetry and mathematics have evolved, failed and restarted differently. It is the story of his 'project', an act of memory, a game with the rules of autobiography as a literary genre and a recollection of many literary references. Jacques Roubaud calls it his "prose cycle" or "memory prose". It started on 11 June 1985 and has been taking -as a 'work in progress' in six branches (one of them being in two parts) that follows a hyper textual and ramified structure -the oulipian self-consciousness of writing to the extreme. Theses branches were published one after the other from 1990 onwards and have been reunited (minus one) under the title 'the great fire of london' in 2009 by the Editions du Seuil.

To fulfil this 'project', Jacques Roubaud gave himself a rule: write every morning, before sunrise sans ratures, sans repentirs, sans impatience, aux mêmes heures toujours, le plus près possible de la continuité myope du présent irréversible et détesté […] [comme] mesure de mon avance, de l'envahissement du blanc des pages par l'encre, de l'éloignement de tout ce qui a précédé le signe noir initial : ce que je fuis. [Without erasures, without repentance, without impatience, always at the same times, as close as possible to the continuity of this myopic irreversible and hated present [...] [as a] measure of my advance, of the invasion of the white on the pages with the ink, of the removal of anything that preceded the initial black sign: which I'm fleeing.] ('le grand incendie de londres', 28)

The slow writing drags him away from an initial black sign, "the node of the error" referring here to the sudden death of his young wife Alix Cléo in 1983. She died of pulmonary embolism less than three years after they had married. It allows him to express his grief and to recall his wife's own project with her own black sign, visible on a set of seventeen photographs exhibited in Arles with the title: If something black, the year she died. But it is also a description of how his big Project became a 'project' and a deep exploration of memory within writing. The Loop (or second branch of the 'project') starts for example, with a very old childhood image of snow in Carcassonne, where snow is very rare. And it finishes also with snow. The snow connects his writing with an outer and an inner space and his memory with the present. But it also transforms an obsessive image -repeated in many other texts and brought back all the way from his real, imagined and recreated childhood -into an emblem of the wandering of old memories, which come back and disappear again and again; similar to the abandoned Project that became something else while always being there. In fact, it makes the reader follow Roubaud from loop to loop, from time to time and from book to book, from his poetry to his prose, novels (or pseudo-novels as he calls them), essays or theater -as well as from bus-stop to bus-stop -into his memory process. It shows how the memories come back through the writing and change all the time. It also separates Roubaud's thoughts on memory from Proust's involuntary, spontaneous and uncontrolled memory. Roubaud's recollections actually don't try to recover anything from his past. On the contrary, he insists on wishing to destroy his memory "because of some sadness in it" (interview with Marcella Durand). His work is more of an exploration of the functioning of memory with clear references to Frances Yates magisterial Art of memory. The false-true autobiography or true-lie, underlining 'the great fire of london' mixes indeed very old traditions of memorizing and recollecting long texts. It also relates to other interests such as the "ecological memory".

One scientist, Marjorie Linton, made an experiment that inspired me. She tried to transcribe all the different memories she had, which came to about 8,000.

After that, she said, "When I tried to add another one, I found that it would be one I had already written down and remembered a bit differently. That's when I stopped. (Interview with Marcella Durand) Hence the idea to bring back all his poetical memories through a literary and personal dialogue between him and each one of his texts and with the work of many other authors from a different genre, time and language such as Jauffre Rudel, Lewis Literary Encyclopaedia -http://www.litencyc.com/php/speople.php?rec=true&UID=13139 6 Carroll, Victor Hugo, Raymond Queneau, Georges Perec, medieval Japanese poets, 20th century American writers… This writing, as an act of memory, allowed Le Voyage d'hier (Yesterday's journey): the first following of The Voyage d'hiver (The Winter Journey) by Perec and started the first collective oulipian novel. It also underlines the literary and photographic dialogue he has been having with his late wife since her death. This dialogue started in 1984 with the publication of Alix Cléo's diary. It is still present in more recent books including Eros mélancolique, written with Anne F. Garreta (it is about a photographer trying a make a picture of a ghostwoman). Then, it is famously at the heart of Some thing black, a book of elegiac poems published in 1986. The poems, alternatively in verse and in prose (another dialogue), are Roubaud's poetic answer to Alix's photographic cycle. They address her directly, expose Jacques Roubaud's grief and transpose, in his own work, the photographs (still on the wall) and the thoughts (from the Journal) she left him. One poem tells, for example, of the difficulties to write, "marié(e) à une morte" [married to a dead woman] (Quelque chose noir, 63), with a (e), being also a [ə], recalling Alix's own difficulties to write (she abandoned the idea of becoming a writer) "married to a poet" ( Journal (1979( Journal ( -1983), 143)), 143). This continued dialogue -beyond the gravecaptures the essence of love. It is also an answer to her artistic research about the disappearance of her body (she was severely asthmatic) and about the 'future-past' in photography (this 'future-past' was pointed out by Roland Barthes who considered that "whether or not the subject is already dead, every photograph is this catastrophe." (La Chambre claire, notes sur la photographie, 150)). But the [ə] reveals also the transformation of her body -without any possibility of recovery -into pneuma, this substance that Plato evokes in the Timaeus as an intermediate between the material and the immaterial, the body and the spiritual. Alix has become [ə]: a physical, intangible and invisible element that has always been very important for Roubaud and for other writers -he started to write about it long before Alix's death (i.e. La Vieillesse d'Alexandre). For him, the [ə] is indeed the memory of a singularity of Romance languages. It is a rhythmical element that comes with the feminine's rimes and thereby, brings back the memory of a breathing female body: Alix Cléo's body with her (difficult) breathing, but more generally, the body of La poésie.

For Roubaud, poetry is like a dying (female?) body that he tries to keep alive with extra [ə] or air; thereby elucidating the public reading he has always thought important to give, the insertion of blank between the words and the lines or the Literary Encyclopaedia -http://www.litencyc.com/php/speople.php?rec=true&UID=13139 7 metaphor of the earthworm preventing the world from suffocating under dead words (Les Animaux de tout le monde, 10). Hence as well, the rule he gave himself to refer to a period when poetry was shining: the Provencal 12th century.

La poésie la plus contemporaine, pour survivre, doit se défense de l'effacement, de l'oubli, de la dérision par le choix d'un archaïsme : l'archaïsme du trobar est le mien. His Graal Fiction, which he defines himself as a mix of the Tale, the Story, the Theory and unpublished revelations from the Arthurian legend and, with Florence Delay, the Graal Theater (a cycle of ten plays inspired by the Arthurian legend) have been written in the same spirit. And his lighthearted Poetry for children goes back to the thousands of lines of poetry that he had learned when he was younger. Sometimes, he also inserts colored parenthesis using first red, then blue (for a parenthesis inside the red parenthesis) and green (for a parenthesis within the blue parenthesis)… The choice and order of colours follows, as he puts it, the evolution of how colours appeared in languages. This allows colours and memories, like Homer's wine coloured sea, to take over the narrative. It helps the tradition -and the poetry -to survive.

In fact, Jacques Roubaud's poetic experiments are endless and he is sometimes accused of writing too much. But then he pleads guilty. When asked by Jean-François Puff where he stands in French Literature, he declares he has been just trying not to be exaggeratedly new (Roubaud; rencontre avec Jean-François Puff, 45).

GENEVIEVE GUETEMME Université d'Orléans

(

  will focus on the thirty-five stops of the Parisian bus lane 29. This transforms each text into a vertiginous logical construction connecting the writing with feelings and memory. It brings him for example to write:Ce n'est pas par hazare : Ode à la ligne 29 des autobus parisiens)

[

  Most contemporary poetry, to survive, must defend itself from erasure, forgetfulness, derision by choosing some archaism: the trobar is my own archaism.] (La Fleur inverse, 17) And this archaism can bring some playful results like in the Hortense novels, a cycle of three fiction books whose narrative structure refers at the same time, to the sextine and to the English detective novel -La belle Hortense (Our Beautiful Heroine), L'exil d'Hortense (Hortense in Exile), and L'enlèvement d'Hortense (Hortense is Abducted).

  Literary Encyclopaedia -http://www.litencyc.com/php/speople.php?rec=true&UID=13139 4 Dismissing a first collection of poetry named Poésies juvéniles (Youthful Poem), published at the age of 12 in 1944, and an anthology entitled Voyage du soir (Evening journey) in 1952, the Project is a description of what made him decide to become a

Works cited:

Roland Barthes, La Chambre claire, notes sur la photographie, Seuil, Cahiers du cinéma, 1980 Roubaud;rencontre avec Jean-François Puff, Paris, Argol, 2008 Jacques Roubaud, Interview with Marcella Durand, in BOMB Garreta, Eros Mélancolique, Grasset, 2009. Alix Cléo Roubaud, Journal (1979-1983), Seuil, 1984-2009


Maxime Carrere

Frédéric Alexandre
email: frederic.alexandre@inria.fr

A System-level Model of Noradrenergic function

Keywords: Neuromodulation, bio-inspiration, decision making

Neuromodulation is an interesting way to display different modes of functioning in a complex network. The effect of Noradrenaline has often been related to the exploration/exploitation trade-off and implemented in models by modulation of the gain of activation function. In this paper, we show that this mechanism is not sufficient for system-level networks and propose another way to implement it, exploiting reported inhibition of a striatal region by Noradrenaline. We describe here the corresponding model and report its performances in a reversal task.

Introduction

In neuromodulation, a principle of neural activation already observed in crustacea [START_REF] Bouret | Network reset: a simplified overarching theory of locus coeruleus noradrenaline function[END_REF], a small set of neurons projects to most regions of the brain and can modify their functioning and learning modes by acting on the intrinsic properties of neurons and on the synaptic weights. Neuromodulators have been popularized in the modeling domain by a paper by K. Doya [START_REF] Doya | Metalearning and neuromodulation[END_REF], proposing how different phases of reinforcement learning might be implemented by global signals representing such neuromodulators, where "dopamine signals the error in reward prediction, serotonin controls the time scale of reward prediction, noradrenaline controls the randomness in action selection, and acetylcholine controls the speed of memory update" (quoted from [START_REF] Doya | Metalearning and neuromodulation[END_REF]).

Concerning dopamine [START_REF] O'reilly | PVLV: The primary value and learned value Pavlovian learning algorithm[END_REF] and acetylcholine [START_REF] Pauli | Attentional control of associative learning-a possible role of the central cholinergic system[END_REF], the role of these neuromodulators has been defined more precisely, relying on experimental data and on more precise or more biologically informed models. In this paper, we propose to revisit the role of noradrenaline (or norepinephrine, NE) and particularly of its effects on other brain regions. Whereas an excitatory attentional effect is generally reported for NE, we mention here a new inhibitory effect on a specific striatal region and explain why, in the brain and also in models, this additional effect is important for the global dynamics of the network. In the next sections, we introduce more precisely some information about noradrenaline and the way it is presently integrated in models, including data and results that will be important for our model that is subsequently presented together with simulation results.

The noradrenergic system

NE originates mainly from the Locus Coeruleus (LC), a brainstem nucleus [START_REF] Berridge | The locus coeruleus-noradrenergic system: modulation of behavioral state and state-dependent cognitive processes[END_REF]. One acknowledged role of NE is to modify sensory processing in the thalamus and the cortex [START_REF] Sadacca | Toward a theoretical role for tonic norepinephrine in the orbitofrontal cortex in facilitating flexible learning[END_REF][START_REF] Sara | Orienting and Reorienting: The Locus Coeruleus Mediates Cognition through Arousal[END_REF], depending on the level of arousal and attention required by the external situation, proposed to be encoded by the tonic levels of NE [START_REF] Berridge | The locus coeruleus-noradrenergic system: modulation of behavioral state and state-dependent cognitive processes[END_REF]. At low level, the animal is at rest (sleeping or grooming). A highly salient stimulus (for example reliably announcing a reward) is going to increase tonic NE level and trigger phasic NE burst to precisely focus attentional processing on that stimulus and resist to distractors. The highest tonic levels of NE are observed when the conditions are no longer predictable (for example in unknown or changing environments) and require to explore among possible relevant stimuli to extract new contingencies [START_REF] Aston-Jones | An integrative theory of Locus Coeruleus-Norepinephrine function: Adaptive Gain and Optimal Performance[END_REF].

This general view relating the level of NE to the level of arousal is consistent with its often mentioned implication in choosing between exploitation and exploration (with higher levels) of sensory criteria to select actions [START_REF] Aston-Jones | An integrative theory of Locus Coeruleus-Norepinephrine function: Adaptive Gain and Optimal Performance[END_REF]. This is also consistent with the reported implication of NE during reversal [START_REF] Aston-Jones | Conditioned responses of monkey locus coeruleus neurons anticipate acquisition of discriminative behavior in a vigilance task[END_REF] when a sensory criterion to predict a reward becomes suddenly invalid and requires to look for another predictive sensory criterion. This has been termed unexpected uncertainty in [START_REF] Yu | Uncertainty, Neuromodulation, and Attention[END_REF], in contrast to expected uncertainty, corresponding to the stochasticity of the criterion and encoded by another neuromodulator, acetylcholine, and requiring only patience and not reconsideration of the criterion.

Going deeper in the description of LC afferents and efferents can allow for a more precise interpretation of the role of NE, based on information available in LC to decide on the release of NE and the nature of NE actions in LC targets. Inputs to LC are of three kinds. Low level signals from peripheral centres give basic information about level of arousal from the sympathetic system and about salient sensory inputs from the oculomotor system [START_REF] Berridge | The locus coeruleus-noradrenergic system: modulation of behavioral state and state-dependent cognitive processes[END_REF]. More elaborated elements of information are sent by the central nucleus of the amygdala and the medial prefrontal cortex towards LC [START_REF] Sara | Orienting and Reorienting: The Locus Coeruleus Mediates Cognition through Arousal[END_REF]. They are generally believed to contribute to evaluate the nature of the present situation, and correspond to information like reward history or response conflicts and errors [START_REF] Aston-Jones | An integrative theory of Locus Coeruleus-Norepinephrine function: Adaptive Gain and Optimal Performance[END_REF]. Other noteworthy inputs to LC are from other neuromodulatory centres which reciprocally influence LC [START_REF] Sara | Orienting and Reorienting: The Locus Coeruleus Mediates Cognition through Arousal[END_REF].

LC projects to most brain regions and more heavily to attentional structures like the parietal sensory cortex, where NE can enhance evoked activity [START_REF] Aston-Jones | Role of locus coeruleus in attention and behavioral flexibility[END_REF]. Importantly, the basal ganglia is the only cerebral structure not receiving projections from LC, except for the shell region of the nucleus accumbens, where NE is reported to have an inhibitory effect [START_REF] Nicola | Modulation of synaptic transmission by dopamine and norepinephrine in ventral but not dorsal striatum[END_REF].

Modeling the role of noradrenaline

In addition to [START_REF] Doya | Metalearning and neuromodulation[END_REF][START_REF] Yu | Uncertainty, Neuromodulation, and Attention[END_REF] other modeling papers have proposed to implement NE mechanisms. McClure and colleagues [START_REF] Mcclure | An exploration-exploitation model based on norepinepherine and dopamine activity[END_REF] propose that the level of NE is estimated by an evaluation function depending on the reward rate (corresponding to input of the orbitofrontal cortex to LC) and measures of response conflict (corresponding to input of the anterior cingulate cortex, ACC, to LC), computed from two windows of long term and short term history of activity.

The model by Aston Jones and colleagues [START_REF] Aston-Jones | An integrative theory of Locus Coeruleus-Norepinephrine function: Adaptive Gain and Optimal Performance[END_REF] proposes a mechanism implementing the trade-off between exploration and exploitation, with the Drift Diffusion Model (DDM). This model can be applied for tasks with two choices with two units acting as accumulators, integrating over time possibly noisy signals favoring each choice and responding when the difference of levels exceeds a threshold. Interestingly, DDM has been originally proposed to reproduce reaction times and error rates in decision making processes but appears to explain well neuronal responses recorded during such processes. In the model, the value of the threshold is of course an important parameter, but also the gain of accumulator integration that can be modified to reach the threshold at different speeds. This simple model, which can be equivalently implemented with units in mutual inhibition, has been shown to be a good approximation of the optimal decision [START_REF] Brown | Simple Neural Networks that optimize decisions[END_REF] but remains limited to two-alternative choices. It has also been shown to maximize the signal-to-noise ratio in the difference between the input signals and, when this ratio changes, [START_REF] Brown | Simple Neural Networks that optimize decisions[END_REF] shows that the gain of the units (or their mutually inhibiting strength) must be modified accordingly.

It is proposed in [START_REF] Aston-Jones | An integrative theory of Locus Coeruleus-Norepinephrine function: Adaptive Gain and Optimal Performance[END_REF] that, when tonic NE is released (in a situation identified as unexpected uncertainty), the gain of the sensory units will increase and this will facilitate random activation of sensory neurons and accordingly exploration. Nevertheless, we have observed some limitations, trying to apply DDM to act not only on a sensory layer of units representing candidate stimuli (as it is the case in [START_REF] Aston-Jones | An integrative theory of Locus Coeruleus-Norepinephrine function: Adaptive Gain and Optimal Performance[END_REF][START_REF] Brown | Simple Neural Networks that optimize decisions[END_REF]) but on the sensory part of a neural network learning to associate a representation of the value of stimuli to the best response, presented in [START_REF] Guthrie | Interaction between cognitive and motor cortico-basal ganglia loops during decision making: a computational study[END_REF] as an implementation of decision making in the brain.

In the [START_REF] Guthrie | Interaction between cognitive and motor cortico-basal ganglia loops during decision making: a computational study[END_REF] network, associations have been learned between sensory neurons and neurons triggering the actions. Even if by NE gain increase a new stimulus is more activated, associative weights might compensate and trigger the habitual action. To tell it differently, an excitatory noise in the sensory layer does not necessarily trigger motor exploration.

Our model

We have mentioned above a biological fact that has not yet been exploited in models, the inhibitory effect of NE in the shell [START_REF] Nicola | Modulation of synaptic transmission by dopamine and norepinephrine in ventral but not dorsal striatum[END_REF]. In fact, the shell is a striatal region known to participate in the evaluation of the value of stimuli in the orbitofontal cortex which can in turn activate motor responses toward stimuli. We can consequently explore another alternative of NE neuromodulation effect, where its action in the shell can inhibit previously learned sensorimotor associations.

Our model uses the DANA library for neuronal representation and computation [START_REF] Rougier | DANA: Distributed (asynchronous) Numerical and Adaptive modelling framework[END_REF]. It extends the model presented in [START_REF] Guthrie | Interaction between cognitive and motor cortico-basal ganglia loops during decision making: a computational study[END_REF] by studying the effect of exploration and tonic NE on it. All the code for the model and parameters are open-source and available online at https://github.com/carreremax/basal-ganglia-ne. We will only describe and discuss here changes made from the Guthrie model. Fig. 1. Main features of our model compared to [START_REF] Guthrie | Interaction between cognitive and motor cortico-basal ganglia loops during decision making: a computational study[END_REF]. ST-PRED and LT-PRED are respectively short-term predictor and long-term predictor which predict reward arrival as the average reward from a long and short amount of trials. Each prediction inhibits the excitatory input of the other in ACC, resulting in ACC activation and NE release in LC only in case of discrepancy between the predictions, ie. in case of unexpected uncertainty. NE release is then used to trigger exploration in [START_REF] Guthrie | Interaction between cognitive and motor cortico-basal ganglia loops during decision making: a computational study[END_REF], by facilitation of cortical excitation and inhibition of striatal inputs.

The level of NE is computed as the difference (or conflict) between a slow and a fast predictor as follows:

The noradrenaline system receives inputs from short and long-term reward predictors, as shown in figure 1. Short and long-term predictors are computed as the average reward on the respectively n st trials and n lt trials last trials. These rewards are respectively sent as inputs to two ACC units computing the conflict between the two predictions, ne s and ne l:

dU ne s dt = τ * (-U ne s + st prediction -lt prediction)
Similarly :

dU ne l dt = τ * (-U ne l + lt prediction -st prediction)
So the long-term prediction is inhibiting the ne s, and the short-term one is inhibiting ne l. The level of NE release, ne, is then taken as the sum of ne s and ne l activities. As a result, if both old and recent predictions are not predicting any reward, neither ne s nor ne l activities are strong, and then NE concentration is low. Symmetrically, if both systems are predicting rewards, the two predictions will inhibit the projections of each other, thus resulting in a low NE release. However, if only one system is predicting a reward, ie if the prediction following recent history is different from the prediction based on long history, the corresponding NE population will have a strong, non-inhibited activation, thus triggering a high level of NE release, corresponding to the fact that the reward contingency has recently changed. Consistent with previous models, NE effect at the cortical level is an excitatory gain :

dV ctx dt = f (U ctx * (1 + ne) * (1 + noise))
where V ctx and U ctx are respectively the firing rate and membrane potential of cortical neurons, f and noise respectively the sigmoid function and activation noise used in [START_REF] Guthrie | Interaction between cognitive and motor cortico-basal ganglia loops during decision making: a computational study[END_REF]. NE inhibitory effect is an original mechanism added in our model, and impacts the output gain of projection from cortex to shell : gain = g ctx cog str cog * ne modulation with g ctx cog str cog the constant gain between cortex and striatum in the sensory loop, and ne modulation the modulatory effect of NE.

ne modulation = max(0.5, 1 -ne ef f iciency * ne)

NE modulatory effect is limited to halving excitatory projections from cortex to shell, consistent with the effect of NE observed in [START_REF] Nicola | Modulation of synaptic transmission by dopamine and norepinephrine in ventral but not dorsal striatum[END_REF]. ne ef f iciency is a constant set to 0.8, so that only maximum values of ne will provoke a minimum value of ne modulation. Fig. 2. Description and values of the parameters added or modified compared to [START_REF] Guthrie | Interaction between cognitive and motor cortico-basal ganglia loops during decision making: a computational study[END_REF].

One of the main problems with unexpected uncertainty-based exploration is the learning rate of the model. If the learning speed of the network is too slow, the network will perform exploration, but will not be able to learn based on this exploration. At the opposite, if the learning is fast enough to learn from a few trials of exploration, it may converge too quickly, which can lead to sub-optimal choice or stability issues. To address this problem, we modified the learning rate of the critic module in the Guthrie's model, from previously 0.025 to 0.2, so that the critic could learn based on exploration, and we added critics' prediction as a sensory input of the network. Consequently, exploration helps the critic to learn insights of the values of alternative strategies, and such values are taken into account in the sensory loop, which in turn helps the network to choose the relevant alternative strategies, and learn it.

Experiments

In order to analyze NE effects in the cortex and the shell, together with the switch between exploration and exploitation, we tested our model on reversal learning. At each trial, two sensory CS are simultaneously presented to the network, on two random positions during 2500ms and the network has to perform an action toward one of the CS. As soon as the model performs an action, reward is distributed accordingly to the reward probability of the chosen CS. If no CS is selected after the 2500ms of presentation, the network will not receive any reward. Then neural activities go down to their initial values, and we proceed to the next trial. The acquisition phase consists in 40 trials, in order to perform over-training and to allow habit formation. In each trial, one CS is systematically rewarded while the other is not. During the reversal, which lasts for 40 trials, reward rates for each CS are switched, so the network has to detect the change in reward contingencies and to switch to the other CS.

In fig. 3, we report the average performance and decision time on 100 reversal experiments with and without NE release. Each experiment is performed with a "naive" model. The model correctly learns to choose the best rewarded CS during the exploration and reversal phases. However, NE release allows to perform random exploration, and to gradually learn from this exploration, resulting in a faster convergence than networks without exploration (fig. 3.A). In addition NE release also increases the decision time of the model during the first trials of reversal (fig. 3.B). This is in accordance with [START_REF] Mason | An investigation of the role of cortical and cerebellar noradrenaline in associative motor learning in the rat[END_REF] results, showing that animals with NE depletion respond with greater rapidity when perseverating. Fig. 3.C shows the release of noradrenaline during trials, which is indeed proportional to unexpected uncertainty, with a peak at the reversal onset.

Conclusion

In this paper, we have reported a model and associated experiments that illustrate the interest of neuromodulation, as a way to modulate existing networks, instead of complexifying their architecture. This is particularly the case for noradrenaline, and its confirmed role in the trade-off between exploration and exploitation. As illustrated in our experiments, NE-based exploration increases the convergence speed of a decision network in an unexpected situation, which is a decisive adaptive property for animals and other autonomous systems.

We have pointed out that another solution for NE-based exploration can be the inhibition of learnt rules rather than the excitation of the sensory gain, and have shown a biologically-inspired, neuronal implementation of it, using reported NE effect in the shell [START_REF] Nicola | Modulation of synaptic transmission by dopamine and norepinephrine in ventral but not dorsal striatum[END_REF]. Its excitatory effect in the cortex, widely used in other models, is still present here. Yet, simulation of the model with only striatal NE (not reported here) still exhibits exploration, but with longer decision time. We hypothetize here that because the task does not require exploration of additional representation in the cortex, cortical NE is not necessary for exploration. If the task needs discovery and creation of adequate cortical representation, like for extra-dimensional shift, it would need cortical NE. Another prediction to be tested in both computational and experimental neuroscience is that inhibiting NE release in the shell should both impede exploration and decrease the decision time. These predictions are explored in ongoing work.

  lt prediction = ( k∈n lt trials reward k )/n lt trials st prediction = ( k∈n st trials reward k )/n st trials with reward k the reward received at trial k.

Fig. 3 .

 3 Fig. 3. Reversal experiments for our decision making model with NE effects (blue) or without NE effects (red). Each curve is the average of 100 experiments performed each time with a "naive" model. Surrounding shaded areas indicate the standard deviation for each curve. (A) Average performance by trials. Both NE and non-NE models are able to acquire CS values and to learn reversal. Exploration allows NE model to detect quicker the change in reward contingency, and to correctly perform faster than the non-NE one. (B) Average convergence time. During the first trials of reversal, exploration by inhibition of the striatum induces a larger response time for NE model. (C) Average release of NE. NE release is important at the beginning of exploration, and larger during the first trials of reversal. It correlates with unexpected uncertainty.