Panagiotis Andriotis

Atsuhiro Takasu

Theo Tryfonas

Smartphone Message Sentiment Analysis

Keywords: SMS messages, Twitter feeds, emotion, timeline

Introduction

The evolution of mobile phones from simple telephone devices to sophisticated handheld computers has transformed how users communicate. Modern smartphones are widely used to send email and chat with friends via instant messages. However, the older SMS (short message service) is still one of the most popular mobile phone services because of its simplicity. The textual information in SMS messages convey the thoughts and emotions of the sender.

A forensic investigation typically involves the examination of electronic devices such as computers, hard drives, tablets and smartphones. The goal is to retrieve relevant information, recover deleted files and present the extracted data in an efficient and intuitive manner. Text messages are an integral part of mobile communications and potentially constitute valuable evidence.

Research efforts in the areas of natural language processing and information retrieval have studied micro-blogging services such as Twitter because of their openness, ubiquity and information content [START_REF] Li | Using text mining and sentiment analysis for online forums hotspot detection and forecast[END_REF][START_REF] Pak | Twitter as a corpus for sentiment analysis and opinion mining[END_REF]. The extraction of the emotional polarity of text messages is an active research topic. Other researchers (e.g., [START_REF] Taboada | Lexiconbased methods for sentiment analysis[END_REF]) note the marked similarity between a tweet (Twitter post) and an SMS message, claiming that Twitter feed analysis techniques can be used to analyze SMS messages. The two formats do indeed have common characteristics. Both involve a limited number of characters (140 for tweets and 160 for SMS messages). In addition, the "@" feature in Twitter can be viewed as a direct message to a specific person, just like an SMS message sent to a contact. Moreover, special symbols such as emoticons and other abbreviations are widely used in Twitter and SMS communications.

This paper extends the textual sentiment analysis work to the domain of digital forensics. It has four main contributions. First, the efficiency of a lexicon-based sentiment analysis algorithm on various datasets (Twitter feeds and SMS messages) is investigated, and the claim that mood analysis methods used on Twitter feeds can also be used on SMS messages is evaluated. Second, the importance of word pre-processing methods is examined along with their contribution to sentiment scoring. Third, the significance of a lexicon is studied and the optimization of a lexicon-based method to improve SMS mood scores is discussed. Finally, a forensic tool that performs sentiment analysis is described; the tool can be used by investigators to search for keywords, compute the sentiment scores of messages and present the sentiment scores in a timeline view.

Background

Sentiment analysis is the process of identifying positive and negative opinions about a subject or topic from a piece of text. Prior work in this field used lexical knowledge and the emotional valence of the words included in vocabularies [START_REF] Melville | Sentiment analysis of blogs by combining lexical knowledge with text classification[END_REF].

Knowledge-based methods use linguistic models to categorize the sentiment of passages of text. These methods construct and use dictionaries in order to capture the sentiments of words. The models can be crafted in a manual [START_REF] Das | Yahoo! for Amazon: Sentiment extraction from small talk on the web[END_REF] or semi-automated manner [START_REF] Yu | Towards answering opinion questions: Separating facts from opinions and identifying the polarity of opinion sentences[END_REF]. Pang, et al. [START_REF] Pang | Thumbs up? Sentiment classification using machine learning techniques[END_REF] implemented three classifiers (naive Bayes, maximum entropy and support vector machines) to evaluate their efficiency in categorizing movie reviews as negative or positive; they conclude that support vector machines work better in most cases. They emphasize that using a more complicated linguistic model such as n-grams does not dramatically improve the results, suggesting that a unigram approach may be sufficient.

Sentiment analysis has been applied to diverse problems ranging from online forum hotspot detection [START_REF] Li | Using text mining and sentiment analysis for online forums hotspot detection and forecast[END_REF] to sentiment classification in microblogs [START_REF] Bermingham | Classifying sentiment in microblogs: Is brevity an advantage[END_REF][START_REF] Ding | A holistic lexicon-based approach to opinion mining[END_REF]. Melville, et al. [START_REF] Melville | Sentiment analysis of blogs by combining lexical knowledge with text classification[END_REF] have developed a framework for sentiment analysis of blogs that combines lexical knowledge with supervised learning for text categorization; they report that it is preferable to incorporate both methods to obtain good results for blog analysis. Taboada, et al. [START_REF] Taboada | Lexiconbased methods for sentiment analysis[END_REF] have used dictionaries of words with predefined characteristics (polarity and strength) and show that lexicon-based methods for sentiment analysis are robust and can be used in a variety of domains without any training with domain-specific data. Their lexicon-based implementation performs well on diverse tasks ranging from video game reviews to blog post classification.

Twitter is an open micro-blogging service that makes all posts available to the public. The public nature of the data provides researchers with the opportunity to use Twitter as a corpus [START_REF] Pak | Twitter as a corpus for sentiment analysis and opinion mining[END_REF]. Bermingham and Smeaton [START_REF] Bermingham | Classifying sentiment in microblogs: Is brevity an advantage[END_REF] suggest that it is easier to infer the sentiment polarity of micro-blogging posts compared with blogs, which have richer textual content (they also note the similarity between micro-blogging posts and SMS messages). However, the automatic processing of micro-blogging posts can be problematic because of the use of non-standard words and unusual punctuation [START_REF] Laboreiro | Tokenizing micro-blogging messages using a text classification approach[END_REF]. Leong, et al. [START_REF] Leong | Mining sentiments in SMS texts for teaching evaluation[END_REF] use sentiment mining to analyze SMS messages in teaching evaluations.

In the area of digital forensics, text analysis has been used to extract patterns from email and to construct user-profiles from text [START_REF] Estival | Author profiling for English emails[END_REF]. Several researchers (see, e.g., [START_REF] Choudhury | Investigation and modeling of the structure of texting language[END_REF]) have focused on investigations and the modeling of texting languages. Despite an extensive search of the literature on mood analysis, we were unable to find any research that engaged principles from opinion and text mining to conduct mobile device forensics.

Experimental Setup and Datasets

This section describes the datasets used in the research, the algorithm and the experimental setup.

The Twitter dataset (TWT) used in the research contained 6,566 tweets collected from 33 popular Twitter accounts on August 5, 2013. The accounts belonged to musicians, actors, athletes and managers. A dataset (SENT140) of tweets classified as positive (PoSENT140) and negative (NegSENT140) was also used [START_REF] Go | Twitter Sentiment Classification using Distant Supervision[END_REF].

The SMS dataset contained 5,574 messages with duplicates [START_REF] Almeida | Contributions to the study of SMS spam filtering: New collection and results[END_REF]. Removing the duplicates yielded 4,827 unique messages that were manually classified as conveying positive or negative sentiments. Negative messages were assumed to express anger, fear, sadness, disgust and boredom (919 messages). Positive messages were assumed to express joy and happiness (1,867 messages). Numerous messages that were not classified as positive or negative were marked as neutral.

The algorithm uses a bag-of-words approach and employed three lexicons containing words linked to positive or negative emotions. The AFINN lexicon [START_REF] Hansen | Good friends, bad news-affect and virality in Twitter[END_REF] contains words with valences ranging from -5 to 5. The Wordnet-Affect lexicon [START_REF] Strapparava | Semeval-2007 Task 14: Affective text, Proceedings of the Fourth International Workshop on Semantic Evaluations[END_REF] consists of synsets linked to affective labels and words. The NRC lexicon [START_REF] Mohammad | NRC-Canada: Building the state-of-the-art in sentiment analysis of tweets[END_REF] was originally used in a competition on sentiment analysis on Twitter feeds. The lexicons were sanitized by eliminating hashtag symbols (#) and words that appeared to be irrelevant to sentiment analysis (e.g., "5yo" and plain letters like "t"). The sanitized vocabularies consisted of 25,675 words and abbreviations corresponding to positive emotions, and 20,636 corresponding to negative emotions.

The methodology for calculating sentiment scores used the three lexicons to score each tweet and SMS. Let L p be the set of positive textual markers (positive lexicon) with l pi ∈ L p for i = 1, 2, . . . , m and let L n be the set of negative textual markers (negative lexicon) with l nj ∈ L n for j = 1, 2, . . . , n. The corpus C consists of tweets and SMS messages and t k ∈ C denotes an individual message for k = 1, 2, . . . , q. If a positive marker l pi appears in a tweet or SMS (t k ) in the corpus:

l pi (t k ) = 1. (1)
Otherwise, l pi (t k ) is set to zero. The same calculations were performed for negative markers l nj . The Boolean assignment is based on the fact that the documents are of limited size; thus, there is a limited range of markers in each tweet that contribute to the tweet sentiment score. The tweet sentiment score s(t k ) is equal to the number of positive markers found in a tweet minus the number of negative markers found in the tweet:

s(t k ) = i l pi (t k ) - j l nj (t k ). (2)

Experimental Results

This section describes the experimental results related to determining the impact of stemming on the dataset, identifying the lexicon that results in the best classification accuracy, and analyzing the impact of emoticons.

Stemming Results

Stemming is a popular text pre-processing method to obtain the root of a word. For example, the words "connect," "connected" and "connection" have the same root that can be represented by the lemma "connect" [START_REF] Porter | An algorithm for suffix stripping[END_REF]. The stemming test discussed in this section evaluates if stemming combined with Equation ( 2) increases classification accuracy. The experiments used the AFINN lexicon on the Twitter dataset and subsequently on the SMS dataset. Each tweet from the TWT and SENT140 datasets was stemmed using Porter's stemming algorithm from the Apache Lucene Library prior to calculating the sentiment score. Table 1 compares the sentiment scores obtained with and without stemming. The column "None" lists the percentages of tweets that did not contain matching words from the lexicon. "Total" lists the percentages of tweets that contained at least one matching word (positive or negative). "Neutral" lists the percentages of tweets that had a sentiment score of zero. Table 2 shows the number of textual markers found in a single tweet.

Table 1 shows that stemming improves the identification of tweets. Another observation is that the Boolean sentiment scores have high "Neutral" classifications. The algorithm sorted 48% of the tweets as neutral, but the percentage of the messages that did not contain any matching words was 39.1%. This difference is because several tweets have zero sentiment scores (i.e., equal numbers of positive and negative markers). In fact, Table 2 shows that the positive and negative datasets have almost the same numbers of matching words. This finding is an indication that a balanced lexicon (i.e., AFINN) is used in the bag-ofwords approach. Tables 3 and4 present the results of the same experiment conducted on the SMS dataset. The lexicon used the AFINN vocabulary and the SMS dataset was first analyzed without stemming and then with stemming after applying Porter's algorithm. Table 3 shows that stemming enhances the efficiency of SMS sentiment analysis because the number of classified messages is increased from 59.4% to 68.1%. Table 4 supports the assessment that AFINN is a balanced lexicon with similar numbers of positive and negative scores. The results also confirm that the methods used for Twitter sentiment analysis help discern the emotional trends of users during forensic examinations of smartphones.

Lexicon Results

Three vocabularies were compared to test the generalizability of the sentiment score: (i) the AFINN lexicon (Tables 1 through 4); (ii) the WordNet-Affect lexicon, which contains formal words that are not widely used in the micro-blogging world; and (iii) the NRC lexicon, which contains many words and hashtags (#) associated with positive or negative emotions. The NRC lexicon was sanitized to fit the bag-of-words approach, but many lemmas such as "okayyy" were present in both categories (positive and negative), making us skeptical about its use. The NRC lexicon also included symbols and Internet slang.

In the case of the WordNet-Affect lexicon, roughly one to three matching words were found in each tweet and 68.5% of the tweets had neutral sentiment scores. For the NRC lexicon, 20.6% of the tweets had neutral emotional scores while 96.9% of the tweets contained at least one word from the lexicon. However, the distributions of matching words were very different compared with the previous results. For example, there were as many as 20 "matching" words in a single tweet. This occurred because many textual markers were present in the positive and negative lexicons. The fact that such an extensive and diverse lexicon could not decrease the percentage of tweets rated with s(t k ) = 0 motivated us to use the AFINN lexicon in the remainder of the study.

Emoticon Results

Many people, particularly young smartphone users, include symbols and special words to abbreviate their messages and produce more concise text. The most popular symbols are called "emoticons." An emoticon is a symbol that expresses an emotion; for example, happiness is represented using a smiling face ":)" emoticon. Based on the characteristics of the SMS dataset, the AFINN lexicon was extended to include emoticons.

Due to the number of neutral sentiment scores, the computation of sentiment scores was modified to include valence. In lexicons such as NRC and AFINN, words are presented with their emotional valence. In AFINN, for example, the textual marker "amazing" has a valence of 4 and the word "approval" has a valence of 2. The maximum valence is 5 and the minimum valence is -5, denoting the most powerful negative emotion. We rated the emoticons as having higher valences on the assumption that users add these symbols to their text messages to express strong feelings. Hence, emoticons should have the highest weight when incorporated in the sentiment scores. In this case, Equation (2) does not change, and the difference arises in the manner in which the contribution of each marker to the final score is computed. Instead, l pi (t k ) = 1 in Equation ( 1) is changed to l pi (t k ) = v where v ∈ {-5, -4, . . . , 4, 5} is the valence of each textual marker.

Table 5 shows the results obtained after repeating the tests on the SMS dataset with the emoticon-enhanced AFINN lexicon and the revised sentiment score computation that includes valence. Note that the addition of emoticons and valence both have a positive effect on the success rates and reduce the numbers of false positives and false negatives.

Combining Sentiment Analysis with Forensics

A common practice during forensic analysis is to use Linux commands such as strings and grep to view and elaborate text. Additionally, an analyst may use open source tools such as the SQLite Database Browser and SQLiteman to view the contents of databases. Our forensic tool extends the database view and incorporates the sentiment analysis approach presented in this paper. This enables the tool to be used to search for keywords in a database, compute the sentiment scores of messages, and present the sentiment scores in a timeline view.

SQLite MySQL

Apache Lucene Indexing Display Search Results Figure 1 shows a schematic diagram of the forensic tool. First, all the requested content from an SMS SQLite database (/data/com.android. providers.telephony/databases/mmssms.db) is stored in a MySQL database. Next, Apache Lucene is used to produce unstemmed SMS message keywords for searching, and stemmed words for SMS mood analysis. After all the data is processed, search indexes are constructed to answer text queries posed by forensic examiners.

The forensic tool was tested on an image extracted from a Samsung Galaxy Y S5360 smartphone running the Android 2.3.5 operating system. Unfortunately, the database contained non-English messages; since these messages had no lexical matches, no sentiment scores were generated. We substituted SMS messages in mmssms.db with random tweets from the TWT database. After running the tool, we had a MySQL database containing the data from mmssms.db and the keywords extracted from each "message" along with the computed sentiment scores.

The forensic tool is designed to provide forensic examiners with a timeline analysis interface that conveys the emotion of each SMS message found on a smartphone. This could provide a quick indication of the emotional states of a user over time. For example, if the person being investigated was generally in a good mood, except for a certain period of time when negative emotions were observed, it might be worthwhile for a forensic examiner to focus on that specific time period.

Figure 2 shows the mood timeline of SMS messages extracted from the SQLite database, including the messages sent to and received from all contacts. Note that the smartphone user mostly exchanged messages that have positive emotional fingerprints. However, there are some periods (e.g., from 12th August until 17th August) when the sentiment scores are negative. The timeline view provides the forensic examiner with a general perspective of user behavior as well as the opportunity to focus on periods that may be of special interest.

The forensic tool enables an examiner to focus on the communications between two parties, or to view the sentiment scores of only the received or sent messages. For example, Figure 3(a) shows the sentiment scores of all the messages exchanged with a specific device. Figure 3(b) shows the scores of all the messages sent by the user.

Finally, the MySQL database may be searched using the index. Figure 4 shows the results obtained for the search term "happy." The tool returned four hits, each with details such as the message ID in the origi-

Conclusions

Current methods used for Twitter sentiment analysis are very useful for depicting the emotional polarity of SMS messages. The results obtained using emoticons and the sentiment valence of words demonstrate the value of a bag-of-words approach. Furthermore, the results can be enhanced by employing a dynamic lexicon.

The digital forensic tool described in this paper merges traditional string searches with text mining to expedite the retrieval of sentiment indications from SMS messages. In particular, the tool can be used by investigators to search for keywords, compute the sentiment scores of messages and present the sentiment scores in a timeline view. This functionality can enrich a forensic investigation by revealing the psychological patterns of users from their text messages.

Our future research will employ the mood analysis approach to produce a timeline view of all smartphone content, including email, instant messages, notes and social network activities. Also, we plan to investigate the application of support vector machine classifiers to enhance the efficiency of the digital forensic tool.

Figure 1 .

 1 Figure 1. Schematic diagram of the forensic tool.

Figure 2 .

 2 Figure 2. Timeline emotional analysis of SMS messages.

Table 1 .

 1 Effect of stemming on Twitter sentiment scores.

		Dataset	None Total Neutral
		TWT	39.1% 60.9%	48.0%
	No Stem	PoSENT140 28.4% 71.6%	41.5%
		NegSent140	25.3% 74.7%	39.3%
		TWT	31.8% 68.2%	42.3%
	Stem	PoSENT140 23.3% 76.7%	36.6%
		NegSent140	18.7% 81.3%	34.7%

Table 2 .

 2 Distribution of textual markers in the Twitter datasets.

		Dataset	1	2	3	4	5	6	7+
		TWT	47.7% 28.7% 14.3% 5.9% 2.1% 0.8% 0.5%
	No Stem	PoSENT140 40.8% 29.0% 16.1% 8.0% 3.6% 1.5% 1.0%
		NegSent140 43.4% 28.3% 15.4% 7.4% 3.4% 1.3% 0.8%
		TWT	41.6% 28.6% 16.6% 7.8% 3.3% 1.3% 0.8%
	Stem	PoSENT140 36.6% 28.0% 17.7% 9.5% 4.7% 2.1% 1.4%
		NegSent140 36.9% 28.1% 17.4% 9.4% 4.7% 2.1% 1.4%

Table 3 .

 3 Effect of stemming on SMS sentiment scores.

		None Total Neutral s(t k )
	No Stem 40.6% 59.4%	50.2%
	Stem	31.9% 68.1%	42.8%

Table 4 .

 4 Distribution of textual markers in the SMS dataset.

		1	2	3	4	5	6	7	8 / 9 1 0 +
	No Stem 45.1% 25.2% 14.5% 6.8% 3.7% 2.5% 0.8% 1.0% 0.4%
	Stem	42.2% 25.0% 14.6% 7.5% 4.4% 2.6% 1.7% 1.6% 0.4%

Table 5 .

 5 Success and failure rates of lexicon-based sentiment analysis.

		Datasets Total FPR	FNR Hit Rate
	AFINN	Positive Negative	1,867 919	12.1% 32.6% 22.7% 32.4%	55.3% 44.8%
	Emoticons	Positive Negative	1,867 919	11.5% 31.1% 22.0% 31.7%	57.4% 46.3%
	Emoticons	Positive	1,867	7.3%	23.9%	68.8%
	and Valence Negative	919	29.2% 25.0%	45.8%

Acknowledgement

This research was supported by the European Union's Prevention of and Fight against Crime Programme "Illegal Use of Internet" -ISEC 2010 Action Grants (HOME/2010/ISEC/AG/INT-002), the National Institute of Informatics, the Systems Centre of the University of Bristol and Project NIFTy (HOME/2012/ISEC/AG/INT/4000003892).

nal SQLite database, the date the message was sent or received, and the contact involved in the communication.


Maxime Puys

Jean-Louis Roch

Marie-Laure Potet

Domain Specific Stateful Filtering with Worst-Case Bandwidth

Industrial systems are publicly the target of cyberattacks since Stuxnet. Nowadays they are increasingly communicating over insecure media such as Internet. Due to their interaction with the real world, it is crucial to ensure their security. In this paper, we propose a domain specific stateful filtering that keeps track of the value of predetermined variables. Such filter allows to express rules depending on the context of the system. Moreover, it must guarantee bounded memory and execution time to be resilient against malicious adversaries. Our approach is illustrated on an example.

Introduction

Industrial systems also called SCADA (Supervisory Control And Data Acquisition) are the target of cyberattacks since the Stuxnet worm [START_REF] Langner | Stuxnet: Dissecting a cyberwarfare weapon[END_REF] in 2010. Nowadays, these systems control nuclear power plants, water purification or power distribution. Due to the criticality of their interaction with the real world, they can potentially be really harmful for humans and environment. The frequency of attacks against these systems is increasing to become one of the priorities for government agencies, e.g.: [START_REF] Anssi | Managing cybersecurity for ICS[END_REF] from the French Agence Nationale de la Sécurité des Systèmes d'Information (ANSSI).

State-of-the-art. To face such adversaries, industrial systems can be protected by intrusion detection systems [START_REF] Verba | Idaho national laboratory supervisory control and data acquisition intrusion detection system (scada ids)[END_REF][START_REF] Paxson | Bro: a system for detecting network intruders in real-time[END_REF][START_REF] Oisf | Suricata: Open source ids[END_REF][START_REF]Snort: Open source network intrusion prevention system[END_REF] which will only detect the attack and do not circumvent it. Intrusion protection systems [START_REF]Dispositif d'échange sécurisé d'informations sans interconnexion réseau[END_REF][START_REF] Seclab-Fr | Dz-network[END_REF] also exist and are able to block a malicious message when it arrives. Those kind of filters are usually stateless, meaning that the legitimacy of a message is only based on the message itself but not on the context. However, attacks may occur because a sequence of messages is received in a certain order or in a certain amount of time, each message being legitimate on its own. Such attack has been demonstrated through the Aurora project [9], lead by the US National Idaho Laboratory in 2007 (and classified until 2014). In order to test a diesel generator against cyberattacks, researchers rapidly sent opening and closing commands to circuit breakers. The frequency of orders being to high, it caused the generator to explode. Electrical disconnectors also require to be managed by commands in a precise order. If any electric current runs through a disconnector while it is manipulated, an electric arc will appear, harming humans around and damaging equipment. To answer this problematic, stateful filtering mechanisms were first proposed by Schneider in 2000 [START_REF] Schneider | Enforceable security policies[END_REF]. Those contributions lead to many researches on runtime-enforcement to ensure at execution time that a system meets a desirable behavior and circumvent property violations. In 2010, Falcone et al. [START_REF] Falcone | What can you verify and enforce at runtime?[END_REF] proposed a detailed survey on this topic. In 2014, Chen et al. [START_REF] Chen | A model-based approach to self-protection in scada systems[END_REF] detailed a similar monitoring technique applied to SCADA networks. However, their approach seems limited to the MODBUS protocol. Finally in 2015, Stergiopoulos et al. [START_REF] Stergiopoulos | Using logical error detection in software controlling remote-terminal units to predict critical information infrastructures failures[END_REF] described a method for predicting failures in industrial software source codes.

Contributions:

We propose a protocol-independent language to describe a stateful type of domain specific filtering. Such filter is able to keep track of the value of predetermined variables. While filtering messages, the values of some variables are saved when they go through. This is a tedious task since the filter must be the single point of passage of all commands to not miss any. However, having a single point of passage for commands also means a single point of failure. Thus, to be resilient against malicious adversaries, we designed our filtering process to guarantee worst-case bandwidth and memory.

Outline: First, Section 2 explains more deeply stateful filtering and its pros and cons. Then Section 3 describes our filtering model and Section 4 illustrates it on an example. Finally, Section 5 concludes.

Classical Stateful Filtering

In this Section, we discuss what is stateful filtering and its shortcomings. Stateful filtering consists in keeping track of the value of predetermined variables of servers. The filter saves their values when they go through. As we said in Section 1 this supposes the filter to be the single point of passage of all messages. It implies that the filter must be hardened to resist against attacks. It also requires it to run in bounded memory and execution time to not delay real time message or overfill the memory of the filter when processing a memory-worst-case message. Moreover, no decision can be taken for a variable if it has not yet been seen before. For this sake, one might want to use three values logic such as Kleene's logic.This also holds if the server can update variables on his own (such as temperature, pressure, etc) and they are not read frequently enough. Three values logics introduce a value neither true or false, called unknown or irrelevant and extend classic logic operators to handle such value. Thus a default policy is needed when the filter is not able to take a decision.

Two major concerns in filtering are [START_REF] Langner | Stuxnet: Dissecting a cyberwarfare weapon[END_REF] the time intervals between successive messages and (2) the ordering of messages. As the language we present in Section 3 does not rely on the time between messages, we are not concern by the first one. The second is obviously important since two different message orderings may lead in two different filtering decisions. Thus as the filter handles messages in the order they arrive, it is crucial that client and servers communicating have deterministic behavior when ordering messages (which they shall do since this matter particularly applies to industrial communications).

Attacker model. We consider any client-side attacker who has access to the rules configured for the filter and their implementations but cannot change any of them. Such attacker is able to intercept, modify, replay legitimate traffic or forge his own messages. The attacker is considered as any client sending (possibly malicious) commands to a server situated on the other side of the filter. Thus every client including the attacker has to send commands complying with the rules configured.

Filtering and Safety properties. For each command message received, the filter decides whether to accept or reject it, based on its state. This decision has to be computed in statically bounded time and memory space. Only accepted command are transmit to the server that returns an acknowledgment; rejected commands are logged and the corresponding input channel is closed (until a reset). The filter behaves as a classical safety run time monitor. Following [START_REF] Roşu | On safety properties and their monitoring[END_REF], a property is a set of finite or infinite traces; a safety property P is a behavioral property which, once violated, cannot be satisfied anymore; thus P is prefix-closed: if w.u ∈ P , then w ∈ P . The requirement to ensure safety property in bounded time and memory space is equivalent for the filter to implement a finite state automaton. For the sake of simplicity and without restriction, this automaton can be defined by a finite number of state variables with values in finite domains and a function transition φ. φ is a finite set of pairwise exclusive Boolean conditions C i , each related to an action A i (atomic update of state variables). The Boolean conditions are evaluated from both the input command and the state variables value. Either none is verified and the command is rejected; or exactly one condition C i is verified and the command is accepted and its corresponding action A i is performed before checking the next input command. Such rule system is usually known as Event-Condition-Action (EC) and XACML is an example [START_REF] Lorch | First experiences using xacml for access control in distributed systems[END_REF].

Towards SCADA Specific Filtering

In this section, we explain how we restrict general stateful mechanisms explained in Section 2 in order to guarantee a worst-case bandwidth. The filters manages local state variables (acting as local copy of server variables) and rules.

Server variables: Variables present on a server and used to define safety property are known by filter where they are matched to local state variables. Thus a variable represented by a numerical identifier is associated to a server (associated to a protocol), a data type and the path on the server to access it (e.g.: a MODBUS address or an OPC-UA node). Variables can also have a sequence of dimensions (e.g.: the length of an array or the dimensions of a matrix). Their definition is shown in Listing 1. Local state variable: some commands on a server variable (especially write requests or read results) provide information of the variable value; the LocalVal declaration enforces the filter to store this value in a local state variable that acts as a delayed copy of the server variable. Yet, when such a command is accepted, the default action is to update the value of the state variable. To prevent space overhead in case of multidimensional variables, this only applies to one cell; we use the Index keyword followed by corresponding valid array keys to obtain a scalar value. Such constraint can be lifted if and only if the size and dimensions of a variable cannot be modified once set. The value of a local variable shall be updated when a message containing the value goes through the filter. In a traditional ECA rule system, updating a local variable should be specified as actions to do when a condition is met. In the case of SCADA filtering, we can easily keep such action implicit due to the restricted number of event able to update local variables (it mainly applies to read responses and write requests). Moreover, updates on write requests must be reversible since the request can possibly be rejected by the server. An example of the definition of local variables is shown in Listing 2. Rules: Finally, rules can be set on variables using the previously declared local variables: conditions are evaluated from the local values of state variables; actions implicitly update those values. They can target either a whole variable or a subrange when multidimensional. They take the form of Boolean functions taking two arguments, separated by AND and OR operators. These functions implement Boolean conditions such as equality, integer relations, etc. Arguments of these predicates can either be: (i) constant numbers, (ii) NewVal designating the value to be written in a write request or (iii) Local-Val designating a previously defined local variable by its identifier. A rule can be either an assertion that will block a message when violated or a warning that will authorize the message but log the violation for later event analysis. An example of the definition of rules is shown in Listing 3.

# Variable 1 should never been set to its current value # (e.g.: opening a currently opened circuit breaker ) Declare Rule Variable 1 Assert NotEqual(NewVal, LocalVal [START_REF] Langner | Stuxnet: Dissecting a cyberwarfare weapon[END_REF]) # The first three rows of variable 2 must remain between 0 and 100. Declare Rule Variable 2 Range 0-5 0-2 Warning \ GreaterThan(NewVal,0) AND LessThan(NewVal,100)

Listing 3. Rule definition example

To ensure constant processing time and memory, both conditions and actions have to be processed in constant time. In our language, all conditions are Boolean conditions that can be verified in O(1) complexity due to the fact that arguments are restricted scalar values (constants, local variables, etc). Moreover, actions are limited to: (i) either block or transmit the message (ii) log information, (iii) update a local variable and all of them also are in constant time. Thus processing one command only depends on the number of rules. In the worst case, a message would be checked against all predicates (for example in the case of a legitimate message). Thus if we associate a constant processing time τ i to each predicate P i appearing n i times total in all the rules, we can compute the worst case processing time T of a message as: T = τ i n i .

Use-Case Example: an Electrical Disconnector

To illustrate our stateful filtering process, we propose the following simple example. An electrical disconnector D separates three electrical feeders such as feeders 2 and 3 are connected to the same input of D. As we told in Section 1, a disconnector cannot be manipulated while current is passing to avoid the creation of an electric arc. To ensure safety, three circuit breakers B 1 , B 2 and B 3 are placed between D and each electrical feeder. Figure 1 describes this setup. Thus, any sequence of messages violating the rule will be blocked ensuring the safety of the disconnector.

B 1 D B 3 B 2 F 1 F 3 F 2 Fig.
In this paper we present a language to describe a stateful type of domain specific filtering able to keep track of the value of predetermined variables. It guarantees bounded memory space and execution time to be resilient against malicious adversaries since processing one command only depends on the number of rules and memory to store monitor is controlled by only monitoring scalar variables or cells. In the future, we plan on extending the Boolean predicates to handle more complex arithmetic such has "Equal(2*NewVal+1, LocalVal[1]**2)". Such verification are still performed in constant time since we are only evaluating the expression with concrete values. We would also be able to specify rules to avoid Denial-of-service. Such rules would limit the number of access to a certain variable within a period of time (e.g.: no more than 10 Read commands per minute) while keeping our bounded time and memory properties.

# A MODBUS server Declare Server 1 10 Listing 1 .

 1101 Protocol Modbus Addr 10.0.0.1 Port 502 # A MODBUS coil (read / write Boolean) Declare Variable 1 Server 1 Type Boolean Addr coils :0x1000 # An OPC-UA server Declare Server 2 Protocol OpcUa Addr 10.0.0.2 Port 48010 # An OPC-UA unsigned integer 5× 10 matrix Declare Variable 2 Server 2 Type UInt32 Addr numeric:5000 Dims 5 Variable definition example

# 4 Listing 2 .

 42 A local variable on a MODBUS coil Declare LocalVal 1 Variable 1 # A local var . on a cell of an OPC-UA unsigned integer 5× 10 matrix Declare LocalVal 2 Variable 2 Index 3 Local variable definition example

  1. Example infrastructure Within a MODBUS server, D, B 1 , B 2 and B 3 can be represented as coils (i.e.: read/write Booleans) with opened state represented by False. In this example, D can be manipulated if and only if either B 1 is opened or if both B 2 and B 3 are open. Thus the configuration presented in Listing 4 is enough to describe this rule. Note that in the rule definition, the AND operator has priority on the OR operator.

	Declare Server 1 Protocol Modbus Addr 10.0.0.1 Port 502
	Declare Variable 1 Server 1 Type Boolean Addr coils :0x1001 # B1
	Declare Variable 2 Server 1 Type Boolean Addr coils :0x1002 # B2
	Declare Variable 3 Server 1 Type Boolean Addr coils :0x1003 # B3
	Declare Variable 4 Server 1 Type Boolean Addr coils :0x1004 # D
	Declare LocalVal 1 Variable 1 # Local variable on B1
	Declare LocalVal 2 Variable 2 # Local variable on B2
	Declare LocalVal 3 Variable 3 # Local variable on B3
	Declare Rule Variable 4 Assert	\ # Rule on variable 4 = D
	Equal(LocalVal [1], False ) OR \ # Using local variable on B1, B2, B3
	Equal(LocalVal [2], False ) AND Equal(LocalVal[3], False )
	Listing 4. Example configuration

This work has been partially supported by the LabEx PERSYVAL-Lab (ANR-11-LABX-0025) and the project PIA ARAMIS (P3342-146798).


Lijun Shan
email: lijun.shan@imag.fr

Susanne Graf
email: susanne.graf@imag.fr

Sophie Quinton
email: sophie.quinton@inria.fr

RTLib: A Library of Timed Automata for Modeling Real-Time Systems

Keywords: Real-time systems, schedulability analysis, Timed Automata, formal semantics

There exists a large variety of schedulability analysis tools based on different, often incomparable timing analysis models. This variety makes it difficult to choose the best fit for analyzing a given real-time system. We have developed RTLib, a library of timed automata templates that represent the semantics of a large variety of timing related concepts proposed by existing models and corresponding timing analysis tools. The key specificity of RTLib is that it is structured to be modular, such that (1) defining a new variant of a given concept requires only a localized change, and (2) non contradictory variants can be trivially combined.

The extensibility of RTLib is demonstrated using five examples ranging from simple variants of the task activation model to the more complex mixed-criticality paradigm. RTLib provides the formal basis needed to compare the concepts offered by models of different timing analysis tools at the semantic level. This in turn will allow us to provide a syntactic mapping between the input of different tools. Our final goal is to help the research community to better evaluate analysis models and their underlying methods.

I. Introduction

Schedulability analysis is an offline approach to evaluating the temporal correctness of real-time (RT) systems in terms of whether all tasks satisfy their deadlines at runtime. Since the 1970s numerous timing models and corresponding schedulability analysis tests have been proposed; see [START_REF] Sha | Real time scheduling theory: A historical perspective[END_REF] [START_REF] Davis | A survey of hard real-time scheduling for multiprocessor systems[END_REF] for surveys. Some of them have been implemented in tools, called analyzers in the sequel, e.g. MAST [START_REF] Harbour | Mast: Modeling and analysis suite for real time applications[END_REF], TIMES [START_REF] Amnell | TIMES: a tool for schedulability analysis and code generation of real-time systems[END_REF], Cheddar [START_REF] Singhoff | Cheddar: a flexible real time scheduling framework[END_REF], SymTA/S [START_REF] Henia | System level performance analysis-the SymTA/S approach[END_REF], SchedMCore [START_REF] Cordovilla | Developing critical embedded systems on multicore architectures: the Prelude-SchedMCore toolset[END_REF], pyCPA [START_REF] Diemer | Compositional performance analysis in python with pyCPA[END_REF], etc. This variety of analyzers makes it difficult to choose the best fit for a given real-time system under study. Indeed, the timing models underlying analyzers are often incomparable, mainly because they make incomparable choices on the precision with which one can express the timing-relevant aspects of RT systems. Such choices mainly concern the models describing (1) the activation of tasks, (2) their resource requirements and (3) the scheduling policies used to arbitrate between them. Also, schedulability is only one possible type of timing requirement: other options include e.g. weakly-hard properties (no more than m deadline misses out of k executions).

To compare the expressivity of the models used by analyzers as well as the precision of the analysis results that they produce, we need a common set of test cases provided in a common input format. Several frameworks exist (e.g. MARTE [START_REF] Omg | UML profile for MARTE: Modeling and analysis of real-time embedded systems[END_REF] and Amalthea [START_REF]Amalthea project[END_REF]) whose goal is to be as expressive as possible. Unfortunately they are not suitable for our purpose as they do not provide a formal semantics. In contrast, Timed Automata [START_REF] Alur | Timed automata[END_REF] provide a formal model which can be used to represent real-time systems at an arbitrary level of precision, and can thus express the operational semantics of any RT system model. This expressivity comes at a price: there is currently no generic way of specifying real-time systems in a Timed Automata based tool such as UPPAAL [START_REF] Larsen | UPPAAL in a nutshell[END_REF].

In this paper, we present RTLib, a library of UPPAAL templates formalizing concepts that may vary from one system model to another, independently of other concepts. The key advantages of RTLib are: (1) its formal basis, (2) its expressivity, which can be easily increased if needed; (3) its modularity, which makes it much easier to compare different models by allowing the user to focus on the concepts that differ. The RTLib library is structured around a core of basic concepts that exist in most frameworks. Thanks to its modular structure, one can easily enrich RTLib with extensions, i.e., variants of one or more templates of the basic library. Two extensions that can be meaningfully combined at the conceptual level can be combined directly at the library level.

RTLib can be used for specifying concrete RT systems on which the UPPAAL model checker can conduct exact schedulability analysis. This can help evaluating the correctness and accuracy of other analyzers on small systems. At a higher abstraction level, RTLib is meant to provide a common, formal basis to describe the semantics of the system models used by analyzers. This will help proposing formally verified transformations between models. Our objective is to complement RTLib with a simple language and associated model transformations to connect it to a wide set of analyzers.

The RTLib files (UPPAAL input) and a user manual are at https://www.dropbox.com/sh/hjftdvhghe04cnh/AAC3L-TjbMXhpQZVS48VCUjNa?dl=0.

The library has been developed using v4.1.19, the latest development version of UPPAAL. The rest of the paper is organized as follows: Section II positions RTLib with respect to related work. Section III describes and justifies the structure of RTLib. Section IV illustrates the modularity of RTLib on hand of four simple extensions, and a more complex paradigm switch. Finally, Section V discusses our contribution and future work.

II. Related Work

The purpose of RTLib is to propose a unified semantic framework for specifying real-time systems. In this section, we review existing formalisms which could provide such a framework and show their limitations.

A. Tool-specific input formats

In principle, the input format for any existing analyzer could be a candidate for the role of common input format. The issue is that these specification languages can only express, quite understandably, the system features that their analyzer can handle. For example, only a few tools such as pyCPA [START_REF] Diemer | Compositional performance analysis in python with pyCPA[END_REF] propose an expressive activation model which specifies the minimum distance between k task activations. Using an input format which does not encompass such functions would be unfair towards the corresponding family of tools and analysis methods. The same goes for input formats which do not allow specifying offsets, or dependent tasks etc. Some simulation tools, e.g. ARTISST [START_REF] Decotigny | Artisst: An extensible and modular simulation tool for real-time systems[END_REF], provide much more expressive specification languages. In that case however, the semantics of the input format is not formally given and can only be clarified through simulation. This approach is not suitable for a comparison between input formats.

B. High-level specification languages

There exist a few approaches aiming at generality. For example, MARTE [START_REF] Omg | UML profile for MARTE: Modeling and analysis of real-time embedded systems[END_REF] is a UML profile for embedded and real-time aspects of systems that has been defined with the aim of putting together all the concepts used in some existing framework or tool. This generality, however, is mainly meant at the level of vocabulary. No formal semantics is given for the different concepts in the vocabulary, and this is done on purpose, in order to leave room for semantic variations. The only semantic framework that is provided would allow to define a declarative semantics -defined by a set of constraints on timed event streams.

Amalthea [START_REF]Amalthea project[END_REF] is an open source framework for specifying real-time embedded systems maintained by an industrial consortium. It aims to be comprehensive with respect of the realtime features captured by its language. It additionally provides connections to simulation and analysis. Unfortunately, there is no explicit effort to formally define a semantics for the Amalthea language. Instead, the semantics is implicitly defined by the connections with these external tools, and hopefully in a non-contradictory manner.

We view our RTLib contribution as complementary to an initiative such as Amalthea or MARTE. Indeed, our effort is less focused on having an exhaustive set of timing features available in our language than on providing a well-founded semantic background for those features that can currently be handled by at least one verification tool.

C. Timed Automata based formats

The UPPAAL [START_REF] Larsen | UPPAAL in a nutshell[END_REF] model checker can be used for the verification of real-time systems. For example, TIMES [START_REF] Amnell | TIMES: a tool for schedulability analysis and code generation of real-time systems[END_REF] is a frontend for UPPAAL dedicated to schedulability analysis. TIMES however deals with a restricted set of concepts (uniprocessor systems with sporadic tasks).

UPPAAL is also used for the timing analysis of industrial case studies, e.g. [START_REF] Mikučionis | Schedulability analysis using UPPAAL: Herschel-planck case study[END_REF], [START_REF] Shan | Formal verification of lunar rover control software using UPPAAL[END_REF]. The model proposed in [START_REF] Mikučionis | Schedulability analysis using UPPAAL: Herschel-planck case study[END_REF] and extended in [START_REF] Shan | Formal verification of lunar rover control software using UPPAAL[END_REF] allows describing uniprocessor systems of independent periodic tasks with a preemptive fixed-priority scheduler and shared memory. Synchronization protocols for shared memory access are implemented, including priorityinheritance and priority-ceiling.

Even more relevant to us are two UPPAAL based modeling frameworks: [START_REF] David | Model-based framework for schedulability analysis using UPPAAL 4.1. Model-based design for embedded systems[END_REF] comprises 5 Timed Automata (TA) templates to specify sporadic tasks, partitioned schedulers on multiprocessor systems, and a sub-template for job enqueuing for each scheduling policy. [START_REF] Boudjadar | Statistical and exact schedulability analysis of hierarchical scheduling systems[END_REF] proposes a framework for hierarchical scheduling systems which consists of templates for specifying sporadic tasks, schedulers and processing units.

All these approaches are of rather limited expressivity. They do not support, for example, the GMF model or weaklyhard RT systems. To fit our purpose, they would therefore need to be easily extendable. This is unfortunately not the case because they have not been designed with modularity and reusability in mind. For example, the Task template in all these frameworks captures not only the task activation and task execution pattern, but also its worst case response time computation and deadline-miss analysis. As a result, one cannot define independently variants of, e. g., the activation pattern and of the execution pattern. Instead, one would need to define a specific template for all possible combinations of variants of the aspects handled in Task.

In comparison, the primary focus of RTLib is on modularity, as we emphasize throughout the paper. Our work builds on top of the TA based representations of real-time systemsin particular tasks and schedulers -of [START_REF] Mikučionis | Schedulability analysis using UPPAAL: Herschel-planck case study[END_REF] and the tasks activation patterns of [START_REF] Fersman | Task automata: Schedulability, decidability and undecidability[END_REF] (which use Task Automata, a variant of TA for expressing task activation patterns).

III. General Structure of RTLib

RTLib is organized in a set of UPPAAL files, one for the so-called basic library, RTLib Basic, and one per extension.

UPPAAL is the standard tool for editing, executing and analyzing Timed Automata1 . A real-time system is represented as a network of automata running in parallel and interacting through synchronization channels and global variables. Time progress and time dependent behavior are expressed using a set of clocks -which represent stop watches -that can be started, halted, reset and read. Automata are instances of parameterized automaton "types" defined by templates. In UPPAAL, a system definition consists of three major parts:

• Declarations: defines the data types, synchronization channels, variables and functions utilized in templates;

• Templates: consists of a set of templates defined as an automaton and parameters; • System declarations: defines a system instance as a network of Timed Automata which are instances of templates and their parameters.

Each template in RTLib represents the common behavior of some component of an RT system. RTLib Basic comprises 15 templates. It includes at least one semantic variant of the ingredients present in every real-time system. Note that the decision to consider some templates as part of the basic library rather than extensions is arbitrary and has little consequence.

Following the principle of separation of concerns, we make templates as hierarchical as possible, so as to ease their understanding and increase their reusability. We encapsulate parts of the behavior of a template into sub-templates, so that the main-template can invoke its sub-templates like a function calls its sub-functions. In the following, templates are denoted by the use of the sans serif font (e.g. Task).

A. Generic structure of RT systems

A real-time system comprises three components: a platform which provides computation and communication resources including processors, buses and memory; a set of tasks which require access to these resources; and a set of schedulers which manage the allocation of resources to tasks.

In this paper, we address the diversity of task models and scheduling policies. We have at the moment a rather limited platform model (no shared memory for example). A more comprehensive set of templates for specifying complex platforms is left for future work. We focus here on the specification of task sets and schedulers. We also discuss how to specify timing requirements other than schedulability.

B. Tasks

In RTLib a task specification has three components: its arrival pattern, its resource requirement (e.g. for execution time) and its timing constraint. We have chosen this structure because it appears that task models, e.g. the periodic and sporadic task models, often differ in only one of these three aspects . In RTLib Basic, the task related templates are:

• Task: releases a job after synchronization with its activation pattern sub-template. The activation pattern of a task is represented by one of the following two sub-templates:

-ActivationPattern Dependent: describes the precedence of a dependent task. -ActivationPattern Independent: describes the initial arrival and recurrence pattern of an independent task. Three sub-templates, Offset, Interval and Jitter, capture the corresponding properties of an independent task.

• Job: represents the life cycle of a job, i.e. an instance of a task. A sub-template ExecutionPattern represents a job's execution process, which in turn has a sub-template ExeTime representing the job's execution time, i.e. its requirement on CPU resource.

Note that defining a sub-template for each parameter allows us to extend these behaviors independently, possibly by replacing the very simple behavior described in the basic library by an arbitrarily complex one.

To build a concrete RT system model in UPPAAL using the above templates, we need to instantiate the Task automaton once for each task. We also need to instantiate the Job template as many times for each task as there may be simultaneously pending jobs of that task. For a schedulable RT system, a task can have at most Deadline/MinInterval jobs. In weakly hard RT systems, a task may have more pending jobs.

C. Schedulers

A platform described in RTLib Basic has a number of nodes, onto which the task set is partitioned. Each node is a multiprocessor system managed by a global scheduler. A platform with a single node is in fact a multiprocessor system under global scheduling. If every node contains only one processor, it is a multiprocessor system under partitioned scheduling. For capturing more complicated types of platforms, e.g. multicore systems with shared memory, RTLib Basic needs to be extended.

A scheduler in RTLib is either non-priority, e.g. FIFO, or fixed priority, e.g. Deadline Monotonic, or user-designated task priority or dynamic priority such as EDF. A scheduler is either preemptive or non-preemptive. A global scheduler allows job migration or task migration.

RTLib Basic implements event-triggered schedulers. Such a scheduler reacts to two kinds of events: job arrival and job finish. A scheduler's reactions to these events are specified in separate templates. For representing these different kinds of schedulers, RTLib Basic provides the following templates.

• Scheduler: reschedules when a job arrives or a job finishes. This is handled by two of the following subtemplates depending on the scheduler type:

-OnJobFinish: schedules a ready job on the processor which just got idle. -OnJobArrive FP: enqueues the arrived job according to its fixed priority (notice that FIFO is a special case). -OnJobArrive EDF: enqueues the arrived job under the EDF policy. A sub-template Enqueue inserts a job into the ready job queue.

D. Timing requirements

A timing requirement is defined at two levels, it is given by the deadline of each task and a system-level requirement. The system-level requirement determines the goal of the timing analysis. In RTlib Basic, the system level requirement is that no deadline can be missed, which is the usual requirement for hard real-time systems. In the extensions, we also consider weakly-hard systems which tolerate certain deadline misses. We use two templates to represent timing requirements:

• ResponseTime represents the task-level timing requirement (deadline). For each job, a ResponseTime automaton measures the time elapsed from its release until its finish, and it sends a message to DeadlineMiss when the elapsed time exceeds the deadline. • DeadlineMiss represents the system-level timing requirement. For each task, a DeadlineMiss automaton terminates the analysis on the first detection of a deadline miss.

IV. RTLib Extensions

By extension, we understand either the introduction of an entirely new concept or a new variant of an existing one. To define an extension, one must proceed in two steps: [START_REF] Adelberg | Emulating soft real-time scheduling using traditional operating system schedulers[END_REF] possibly extend the data type definitions to express the new concepts; (2) add or replace the relevant templates. We present now five such extensions to demonstrate that the chosen level of decomposition achieves sufficient modularity 2 .

A. The minimum distance activation model

The event stream model [START_REF] Albers | An event stream driven approximation for the analysis of real-time systems[END_REF] is a generalization of the sporadic task model which constrains not only the minimal time distance between any 2 consecutive activations of task τ, but may for any k impose a stronger constraint for the minimal time interval that may contain k activations. In practice, it is sufficient to consider a strictly increasing constraint sequence only for some first N values for k. Thus, such a minimum distance function can be specified by a vector [D 0 , D 1 , ..., D N-1 ] of minimal distances D i between the activation of job τ k and τ k+i+1 ∀k. Note that a sporadic model is specified by a minimum distance vector with a single element D 0 . Extending the basic activation pattern of the sporadic task model to handle minimum distance functions only requires to modify the Interval template (see Figure 1) which specifies that the inter-arrival time (i.e. the time interval between two consecutive activations), recorded by the clock x, is between a minimum value Min I and a maximum value Max I.

To represent a vector of N minimum distances requires N clocks. Figure 2 shows the template for N = 3. It extends the Interval template with two additional clocks: x1 records the distance between τ k and τ k+2 , and x2 records the distance 2 We use the following conventions. Template A B is a specialization of template A for extension B. Synchronization channels are named as follows:

• A e B: automaton A sends a message to B on event e; • A call B: automaton A calls its sub-automaton B;

• A return B: automaton A, a sub-automaton of B, returns. between τ k and τ k+3 . Function countJob() counts the first job arrivals up to N -1.

B. The GMF task model

Remember, a sporadic task is characterized by timing attributes defining arrival pattern, resource requirement and timing constraint. Some tasks' timing characteristics vary greatly from one activation to another. The sporadic task model takes into account the worst case for defining each attribute, which leads to safe analysis but possibly a waste of computation resources. To enable more precise analysis, the Generalized Multi-Frame (GMF) task model characterizes such tasks by a set of frames defining different versions of this task [START_REF] Baruah | Generalized multiframe tasks[END_REF]. For a task with M frames, each of the timing attributes is now a vector of length M. A cyclic GMF (cGMF) task cycles through its frames, while a non-cyclic GMF [START_REF] Moyo | On schedulability analysis of non-cyclic generalized multiframe tasks[END_REF] task takes them in an arbitrary order.

The Task template in Figure 3 defines the task activation behavior for a simple sporadic task: at system start and after each job release, a sub-template ActivationPattern is invoked; on termination of the invoked behavior, the activation pattern is met, and the task releases the next job. This means that the definition of Task is independent of the actual ActivationPattern. To represent GMF task model, we need to extend the Task template to take into account multiple frames. A multiframe task depicted in Figure 4 must choose a frame before invoking ActivationPattern. Choosing a frame is done by invoking the behavior defined by the sub-template FrameControl GMF, which selects a frame for a cGMF or ncGMF task, as shown in Figure 5.

In addition, since a GMF task is defined by arrays, the get-functions of the form get(para, taskID) used in diverse templates have to be extended to arrays with an additional parameter for the array index. The only modification that is needed in any of the other templates, including ActivationPattern, is to replace the get-functions.

C. Weakly-hard real-time requirements

A hard RT system does not allow any deadline miss, whereas a weakly hard RT system tolerates a certain number of deadline misses. Therefore to analyze weakly hard systems, Fig. 5. FrameControl GMF we have to modify the system level requirement. There is no other modification needed.

DeadlineMiss in Figure 6 represents the timing requirement for a hard RT system, which terminates the analysis on a deadline miss. For weakly hard RT systems, one usually considers for each task, different restrictions on the allowed patterns of deadline misses in a window of m task invocations [START_REF] Bernat | Weakly hard real-time systems[END_REF]. Now to represent the weakly hard requirement, only the DeadlineMiss template needs to be modified. Instead on systematically terminating the analysis with "error" on occurrence of a deadline miss, one has to analyze whether this is an allowed deadline miss or not, and only a forbidden deadline miss terminates the analysis. To determine whether a deadline miss is allowed, additional variables are needed to store the relevant deadline miss history in the window of the last m invocations depending on the chosen criterion.

The template DeadlineMiss WeaklyHard in Figure 7 shows this behavior. The evaluation of whether a deadline miss is allowed or not is hidden in the boolean function bOverMiss and the recording of the relevant history in the functions onMeet and onMiss.

D. The abort-on-miss execution paradigm

In a soft RT or weakly hard RT system, several option to deal with a deadline overrun situation which depends on the specific overload management policy [START_REF] Adelberg | Emulating soft real-time scheduling using traditional operating system schedulers[END_REF]: run-to-completion means to continue the overrun job until it completes, somehow assuming "better late than never". abort-on-miss means to abort a job as soon as it misses its deadline, assuming that "whatever it has been doing, this is now useless".

The overload management policy, which determines the execution pattern of overrun jobs, is modeled by Execution-Pattern template in RTLib. In RTLib Basic, the template ExecutionPattern Completion in Figure 8 implements the run-to-completion policy. It is the only template to modify for representing the abort-on-miss policy. In the template ExecutionPattern Abort (see Figure 9), Elapse is a clock recording the time elapsed since a job has been released. The invariant on Elapse on the locations Ready and ExeTime imposes the constraint that a job cannot exceed its deadline when it is ready or running. When the deadline is reached before proper termination, the job "kills itself" and informs the scheduler. Note that this does of course not represent the behavior of the implementation, but it nevertheless correctly represents the corresponding timed behavior. This is sufficient for our purpose.

E. Mixed Criticality: a special system model

The recent years has witnessed an increasing research interest on Mixed Criticality systems [START_REF] Baruah | Response-time analysis for mixed criticality systems[END_REF]. Such a system has two groups of tasks: high and low critical ones. A high critical task has two versions of worst case execution time: C(LO) and C(HI), where C(LO) < C(HI) [START_REF] Burns | Towards a more practical model for mixed criticality systems[END_REF]. When a high critical task overruns C(LO) and enters the long execution mode where it needs at most C(HI) CPU time, the system switches to a "high criticality" mode, where all the low critical jobs in the ready queue are killed to save CPU time.

The MixedCrit extension describes a system's mode switch in 3 steps: (1) A high critical job informs the scheduler to switch to high criticality mode as soon as its execution time exceeds C(LO); c) Scheduler MixedCrit: The template Scheduler in Figure 10 is extended with the scheduler's reaction to a mode switch, as shown in Figure 11. The scheduler sends a broadcast message S ched discard Job to terminate all low critical jobs. Function dequeueLowCrit(schID) removes the low critical jobs from the ready queue. Furthermore, the subtemplate OnJobArrival is extended to take care of discarding low critical jobs which are released after the system switches to the high criticality mode. In the current RTLib, a system stays at the high criticality mode once it switches to it. The template Job is extended to Job MixedCrit, so that low critical jobs can be killed.

V. Discussion and Conclusion

We see RTLib as the first easily extensible framework for defining the formal semantics of a wide scope of realtime system models. Thanks to its fine-grained modularity, adding a feature to RTLib can be realized through localized modifications, and extensions on different aspects can be composed. Once a timing model is constructed, it can be used to formalize concrete RT systems, where users only need to instantiate some templates in RTLib with actual parameters of specific RT systems.

Note that the fact that model checking does not scale is not an issue for us. RTLib can of course be used for exact schedulability analysis to assess the correctness and accuracy of the results obtained using a given analyzer. But we do not mean to use RTLib for directly analyzing industrial systems. Instead, the strength of RTLib is that it provides a framework for explicitly defining the semantics of the terminology related to RT systems, thus bridging the gap between analyzers which are currently uncomparable. RTLib can be used to formally compare the expressivity of different analyzers, and thus better assess the chosen compromises between precision of the timing model and accuracy of the analysis. The comparsion and evaluation help users to combine various analyzers in the analysis of concrete systems.

RTLib is the first step in a project for evaluating and comparing RT schedulability analysis techniques and tools, including: (1) an intermediate formalism on top of RTLib, called RTSpec, for specifying RT systems, (2) a set of benchmarks specified in RTSpec, (3) automatic translators between RTSpec and existing analyzers, and (4) translations from RTSpec to formal models. In this approach, RTLib serves as the underlying, easily extensible semantics of RTSpec. Our future work also includes to develop a toolset to facilitate the application and extension of RTLib, so that RT system researchers and engineers who may not be experts in formal methods can conduct lightweight extensions on RTLib.

Fig. 1 .

 1 Fig. 1. Interval Fig. 2. Interval MinDistance for 3 distances

Fig. 3 .

 3 Fig. 3. Task Fig. 4. Task MultiFrame

Fig. 6 .

 6 Fig. 6. DeadlineMiss Fig. 7. DeadlineMiss WeaklyHard

Fig. 8 .

 8 Fig. 8. ExePattern Completion Fig. 9. ExePattern Abort

( 2 )

 2 The scheduler kills all the low critical jobs in the ready job queue; (3) The high critical job completes when its execution time reaches C(HI). a) FrameControl MixedCrit: A high critical task has two frames: one has C(LO) as its WCET and the other C(HI). The template Task MultiFrame in Figure 4 is reused here. Its sub-template FrameControl MixedCrit randomly chooses either frame before each activation of a high critical task. b) ExecutionPattern Completion MixedCrit: The Ex-ecutionPattern Completion template in Figure 8 is extended to represent the execution of high and low critical jobs. If a high critical job is in the long execution frame, its execution consists of two stages [0, C(LO)] and (C(LO), C(HI)]. The first stage is represented by a sub-template ExeTime in RTLib Basic. The second stage is represented by another sub-template ExeTime MixedCrit, which is a variant of ExeTime.

Fig. 10 .

 10 Fig. 10. Scheduler Fig. 11. Scheduler MixedCrit d) Job MixedCrit:The template Job is extended to Job MixedCrit, so that low critical jobs can be killed.

We assume that the reader is familiar with TA and with UPPAAL.


Maximilien Guislain

Julie Digne

Raphaëlle Chaine

Dimitri Kudelski

Pascal Lefebvre-Albaret

Detecting and Correcting Shadows in Urban Point Clouds and Image Collections

Introduction

As more and more cities embrace the digital revolution, there is a growing demand for digitization technologies able to reconstruct urban scenes from geometric measurements and pictures. The goal might be, for example, to plan urban evolution or allow virtual tours of the city. A common way to perform these measurements is through a LiDAR acquisition campaign. Indeed, range laser scanners as well as cameras can be embedded aboard a vehicle moving in the streets, taking laser measures and pictures as it goes. The final result is a point cloud and a series of pictures that are either registered by calibration or by optimization algorithms. Thus the geometric information can be aug- * maximilien.guislain@liris.cnrs.fr mented with some color information. However, this information depends strongly on the lighting conditions during the acquisition which in turn depend on the daytime, season and weather. This leads to the question of retrieving illumination-free colors in order to have a time-independent urban scene acquisition. In urban scenes the most important problem lies in the shadows projected by the buildings or by the street furniture and trees.

In this paper we focus on shadow detection in the point cloud by jointly analyzing the geometry, reflective and color properties of the scene. The detection and correction of shadows is closely linked to the intrinsic image recovery problem, which decomposes an image into a reflectance and a shading layer [9]. However we will use a simplified illumination model compatible with our input data and avoiding user interaction. To do so, we build on a simple characterization of the shadow edge: two points lie on two sides of a shadow boundary if they have similar laser reflectances but very different color values. Indeed, the value of the laser reflectance depends solely on the reflective properties of the surface and not on the fact that the surface lies in the shadows or in an illuminated area.

Input data. We consider unstructured point clouds and associated pictures acquired from urban scenes. The point cloud is endowed with the laser reflectance intensity which depends on the reflective properties of the surface impacted by the laser. It is typically given by the amount of photon that flies back toward the LiDAR. The pictures GPS positioning is also available which will be important for the illumination correction step. Images are considered to be precisely registered relatively to the point cloud. They can be taken at the same time as the LiDAR acquisition process or at a different time, but they are assumed to be taken in a relatively small period of time so that all images have consistent illumination conditions.

To summarize, our contributions are the following:

• A shadow characterization that does not require user interaction

• A new energy minimization formulation for segmenting shadows and sunlit areas

• The joint exploitation of the image structure and Li-DAR data reflectance properties

The remainder of this paper is divided as follows: in section 2 we review relevant previous work. Section 3 gives an overview of our method. Then, sections 4 and 5 detail the methods for detecting and correcting the shadows. Finally, the results are shown in section 6.

Related work

Shadow detection and removal is already a widely explored field. Methods have been developed to detect shadows either on a single image, a sequence of images or datasets containing both geometric information such as a LiDAR point set and registered images. Each of these problem settings requires a specific problem formulation, although some common ideas can be found in all these approaches. We review below relevant work emphasizing concepts that are linked to our approach.

Single image shadow detection

The detection and correction of shadows in a single image is a difficult problem that has been extensively studied. We restrict our analysis to some recent works that not only propose methods to detect the shadows but also address the re-illumination problem.

Lalonde et al. [START_REF] Lalonde | Detecting ground shadows in outdoor consumer photographs[END_REF] present a method to locate and remove the shadows based on machine learning. First the shadows are detected using a watershed segmentation and a Canny edge detection. Descriptors composed of histograms and skewness of the pixels intensities are analyzed on both sides of the detected edges. Shadow edges are then consolidated using a probabilistic model. Finally the scene layout (decomposition between ground, sky, and vertical surfaces) is added to only detect and consider the shadows laying on the ground.

Corke et al.

[3] propose a method to recover a grayscale intrinsic image from a standard RGB image by considering the physical properties of the light and using also the Log-Chromaticity colorspace. In this particular colorspace, the colors of all materials under varying illuminations change along parallel directions. By projecting the points on a line perpendicular to these directions, an illumination-free color can be found. It however requires user interaction to define two regions of the same material under different illumination conditions and a perfect knowledge of the camera sensor response.

Xiao et al. [START_REF] Xiao | Fast shadow removal using adaptive multi-scale illumination transfer[END_REF] remove shadows from a single image using a multiscale illumination transfer in the La*b* colorspace. Shadowed and lighted regions are roughly sketched by the user and then segmented using a Gaussian Mixture Model. A multi-scale illumination transfer between the shadowed and lighted regions is then performed assuming lambertian surface illumination properties. Finally the shadow boundaries are reprocessed using a Bayesian framework to remove relighting artifacts.

Images sequence and 3D proxy

Over the past ten years, fast and robust photogrammetric methods have been developed to compute a 3D model from a series of pictures. Two of the most well known methods are Structure from Motion (SfM) [13] and Patch-based Multi-View Stereo (PMVS) [START_REF] Furukawa | Accurate, dense, and robust multiview stereopsis[END_REF]. These multiview methods have been exploited to enrich the information of 2D images in order to retrieve specific lighting properties.

Laffont et al.

[7] propose a complete and precise process to retrieve the intrinsic characteristic from a set of images. This algorithm requires a set of HDR images, a set of LDR images from which a proxy 3D model is built, and a measured environment map. User interaction is also required to define the sun orientation and obtain two gray color values in the sunlight and in the shadow. This set of input data are used to decompose the illumination of each vertex of the proxy model into the original albedo and the sun, sky and indirect luminance. Finally these vertices are projected onto the image planes to retrieve the intrinsic images. Although this method proves efficient, it requires a lot of additional information that are not available in our context, in addition to user interaction, something we avoid.

In a somewhat similar manner, Wehrwein et al. [START_REF] Wehrwein | Shadow detection and sun direction in photo collections[END_REF] automatically detect the shadows and the sun direction in a series of picture. Applying SfM to the pictures yields a 3D model. A set of colors is associated to each vertex of the mesh that comes from all the images that see the vertex. From the statistics of the proposed colors, the algorithm can guess which points lie in the shadow in each image. These shadow point labels are used to consolidate the shadow edges and estimate the orientation of the sun.

Shadow detection on 3D LiDAR data

Detection of shadows on 3D LiDAR data is a less explored environment compared to single image and images collections.

Troccoli and Allen [14] relight a 3D point cloud model using multiple HDR overlapping images taken under different illumination conditions. Their strategy is to compute and analyze illumination ratio in overlapping areas and use these ratios to relight the whole image. This approach however requires a mesh reconstruction step to get rid of the point cloud and work on a watertight surface.

Ramakrishnan et al. [START_REF] Ramakrishnan | Shadow compensation for outdoor perception[END_REF] propose to correct the colors of a point cloud using a consistent and continuous illumi-nation model by removing the direct sun illumination and normalizing the sky illumination. The indirect illumination from the other part of the scene is considered negligible. The sun orientation is obtained using the GPS coordinates of the scene as well as the known sun position relative to this position at the time of the scene acquisition. Similarly to [3], pairs of points of the same material are selected by the user both in sunlight and in the shadowed parts of the cloud. These pairs are used to compute the sun illumination and sky illumination contributions which yield an estimation of the illumination values for each point of the cloud. Unlike our approach, this method requires user interaction. Furthermore, this algorithm is tested on LiDAR scans measured on separated buildings, a setting quite different from our complex urban scene point clouds, where the buildings are concentrated and the streets narrow. Finally, this method relies heavily on having a clean 3D model. However in our context, the 3D model is only imperfectly measured, which can affect the quality of the sun visibility estimation (there can be missing building parts) and alter the final results.

Overview

Our approach takes as input a point cloud endowed with laser reflectance information as well as a series of pictures aligned with the point cloud. From this relatively common input data, we propose to detect the ground shadows and to correct them using a simplified illumination model. The main characteristic of our algorithm lies in the joint exploitation of both images and point clouds.

Our shadow detection algorithm proceeds in several steps:

• Shadow interfaces are identified using reflectance and luminance properties of the colored point cloud • Interface points are filtered using local histogram analysis • The shadows are segmented in the image plane using graph cut with well chosen graph edge costs

Once the shadows are detected the correction is a twostep method building on a simplified illumination model performing a luminance correction in the first step and a chrominance correction in a second step.

Shadow detection

Our shadow detection method relies on the observation that a shadow barely impacts the reflectance value of a point while it strongly impacts the color value. Indeed the laser reflectance only depends on the material properties of the surface whereas the color takes into account the illumination of a point. Therefore our first step is to look for shadow interface areas that have low reflectance gradients and high color gradients.

Shadow interface detection

In this first step, the algorithm works directly on the point cloud and finds pairs of close points that are likely to lie on each side of a shadow interface.

We define the neighborhood of a point as the set of its K nearest neighbors and estimate the color gradient ∇c and reflectance gradient ∇R in this neighborhood. Since the value of K impacts the computation time, we use a small value K = 4 at the risk of loosing some interfaces. As will be seen below, we still get enough interfaces to detect the shadows. The gradients between two neighboring points p and q are defined as follows:

∇R = |R p -R q | R p + R q ∇c = E 00 (C p , C q )
where E 00 is a weighted difference of the color expressed in the La*b* coordinates to render the gradient perceptually meaningful. The exact formula for E 00 can be found in [12]. To detect relevant pairs of points we use a threshold that loosely selects a set of shadow interfaces. This threshold is set experimentally: two points are considered to lie at a shadow interface if |∇c| ≥ 2.33 and |∇R| ≤ 0.05. It may appear counterintuitive to use the color gradient instead of the luminance gradient since the luminance should contain all illumination information. However, in the case of outdoors scenes, not only the luminance but also the chromaticity of the points is affected by the sun visibility, as noted by Khan and Reinhard [START_REF] Khan | Evaluation of color spaces for edge classification in outdoor scenes[END_REF] and Corke [3]. Indeed, sunlit areas tend to be more yellowish (due to the sun light spectrum), while unlighted areas tend to appear more blueish (due to Rayleigh scattering). Therefore, it is better to use the full color difference rather than the luminance only. This assumption was verified experimentally by a higher number of meaningful detection. Since our threshold is not tight, irrelevant detected pairs of points are filtered out based on a local density criterion: if a single pair is detected in a large area then it is likely that this pair is a false positive. In practice we remove the pairs of points that do not contain at least 1/4 of their K nearest neighbors as potential shadow interface (K = 21). While this step does not remove all the outliers it is sufficient to reduce the computational burden of the next filtering step.

Shadow interfaces filtering

A further filtering of the shadow interfaces is achieved by analyzing the luminance histograms around a detected shadow interface pair of points. Indeed, histograms around a pair corresponding to a true shadow interface should have a bimodal distribution reflecting the light and shadow parts, as illustrated by figure 1. Following this observation, points pairs should only be kept if their histograms indeed display a bimodal distribution. Luminance histograms are computed by considering points that lie close to the pair and exhibit similar normal and reflectance values. This avoids considering luminance coming from potentially different materials in the vicinity of the pair. Histograms are then smoothed using a convolution and the peaks are detected by computing the first derivative of the distribution function. Small peaks are discarded if their heights are less than 75% of the highest peak. The remaining number of peaks should be exactly equal to 2 for the distribution to be considered bimodal. In this case, the interface pair is kept. The values of the two peaks define L L and L S the luminance in sunlit areas and in the shadowed areas respectively.

Shadow consolidation

Previous steps allowed for the detection of interface points pairs which should next be turned into a complete segmentation method. To do so we momentarily set aside the point cloud, and exploit the detected interfaces directly in the image plane, since an image is a denser information. Thus, we project our shadow interface pairs in the image plane, using the camera known pose and intrinsic parame-ters.

Using these interface points to estimate the sun position and deduce the segmentation might look like an appealing idea but it would require a complete and consistent geometry to be able to retrieve the shadow mask. However if it is indeed the case on most terrestrial scans, some scanners may either miss occluding geometry or even do not account for all the geometry of the scene. For example, the Velodyn scanner of the KITTI dataset [5] measures points that are less than around 2 meters off the ground. We propose a different approach, relying on the images to compute a shadow segmentation: we look for a labelling δ of the image pixels, equal to 1 if the pixel lies in a shadow and 0 otherwise. The segmentation problem can be stated as an energy minimization with the following objective:

E(δ) = p:image pixel E data (δ, p) + γ (p, q): neighboring pixels E smooth (δ, p, q) (1)
where

E smooth = e -1 2σ 2 (L(p)-L(q)) 1 δ(p) =δ(q) , E data (δ, p) = e -1 2σ 2 (L(p)-L S ) 2 if δ(p) = 0 e -1 2σ 2 (L(p)-L L ) 2 if δ(p) = 1
and γ is a weighting term set to 1 in our experiments.

This type of energy can be easily minimized using graph cuts [2] [START_REF] Boykov | An experimental comparison of min-cut/max-flow algorithms for energy minimization in vision[END_REF] by using E data as the source and sink edge costs and E smooth as the inter-pixel edge cost. The labels obtained by the graph cut are then back-projected on the point cloud to assign the points to the shadow mask. On figure 2, we show the results of initial interface detection, interfaces filtered by density, by histogram analysis and the final graph cut result, demonstrating how the graph cut turns the sparse set of shadow edges into a full segmentation. This step retrieved the proper shadowed areas in a scene where the surface reflectance changes widely due to material variation (ie., white building wall vs darker building wall).

Shadow Correction

Once the shadows are segmented, the next step is to project the labelling on the point cloud, and to modify the color of the points so as to obtain a shadow-free point cloud.

Illumination model

According to [START_REF] Yu | Inverse global illumination: Recovering reflectance models of real scenes from photographs[END_REF], [7] and [START_REF] Ramakrishnan | Shadow compensation for outdoor perception[END_REF] the luminance of a point lying on an lambertian outdoor surface can be defined as:

L = R(S sun + S sky + S indirect )
(2)

S sun = V sun cosαE sun (3)
S indirect = Ω indirect cosθ indirect E indirect (5)
With I the illumination, R the albedo of the material, S sun the lighting contribution of the sun, S sky the lighting contribution of the sky (ambient light) and S indirect the lighting contribution of the light reflected by the objects in the scene. All notations are summarised on figure 3. Using this simplified model, our algorithm proceeds in two steps, correcting first the luminance component and second the chrominance component at each point.

Luminance correction

The luminance correction step requires an approximation of the sunlight orientation to be able to separate the different component of the scene lighting. Although the method proposed by [START_REF] Wehrwein | Shadow detection and sun direction in photo collections[END_REF] locates the sun orientation without a priori information, it cannot be applied on large urban scans due to the lack of precision on the surface to detect attached shadows. However, the sun azimuth and elevation can be estimated if the approximate GPS position and time of the data acquisition are known [START_REF] Reda | Solar position algorithm for solar radiation applications[END_REF], leading to the sun orientation estimate. That is the method that was used to obtain the sun ray orientation relative to the scene. Knowing the position of several shadow points, the amount of illumination provided by the sky can be roughly estimated. Indeed, for shadow points the sun contribution can be safely ignored and the luminance of these points writes: L = R(S Sky + S Indirect ), where R is the surface reflectance. We simplify the problem by considering that S Sky + S Indirect = β ×E sky where β = 0.5× n(p), n ground +1. Thus β varies proportionally to the dot product of the ground normal n ground and the point normal n(p).

This estimated lighting ratio β from the sky is errorprone in the case of urban environment where streets can be tightly enclosed by buildings, greatly reducing the real contribution of the sky compared to the contribution of indirect lightening. However it is still a good first approximation of the amount of light coming from the environment. It is thus possible to make the luminance uniform for shadowed points by computing β the average β in the shadowed area:

L (p) = L(p) β β(p) (6)
The matter is quite different for sunlit points. In a similar manner as [START_REF] Ramakrishnan | Shadow compensation for outdoor perception[END_REF] we define the sun-sky-ratio (SSR) of lighting between the sun and the sky:

SSR = LL βS -LS βL LL (cosα) L ( 7
)
where α is the angle between the sun direction and the points normal. The straight bar above the notation means that the quantity is averaged on a light or a shadow area respectively, depending on the indice L or S . More details on the derivation of this formula can be found in the original publication [START_REF] Ramakrishnan | Shadow compensation for outdoor perception[END_REF].

This ratio allowing us to recompute the luminance of points in sunlight:

L (p) = L(p) βS SSR cos α + β(p) (8)
Applying these transformations to the luminance of the point successfully relight them in a realistic manner. Once the luminance is corrected, the chrominance can also be adapted.

Chrominance correction

The chrominance correction is simpler: it uses a simple chrominance ratio between the sunlit points and the shad- This trivial update is enough for chrominance correction, as presented below in our experiments.

Penumbra zones

After this two-step correction, there may remain some artifacts near the boundaries of the shadowed and sunlit areas which should be corrected (figure 4). Indeed, having a binary shadow mask may lead to unwanted effects along the shadow edges where the boundary between light and darkness is not sharply defined. These effects are typically due to under-or over-compensation in the luminance and chrominance correction around the shadow edges, which induces the apparition of a strong linear artifact along the border. This artifact is clearly visible in figure 4c. To alleviate this effect we perform an in-painting step around the known shadow border. Since the area to inpaint is very small, we avoid any sophisticated inpainting method such as variational or patch-based inpainting and use a median filter to guess the missing pixel colors. This last step, despite not being perfect, mitigates the visual artifacts caused by overcompensation as depicted in figure 4d.

Results and Discussion

We demonstrate the efficiency of our shadow detection and correction schemes on two different sets of data. Both these sets are composed of points clouds with intensity values and registered images that are used to color the point cloud. The GPS positioning of the images is also available. In these two sets, images and point clouds have been acquired at the same time.

Leica Pegasus Dataset

Our main test-case is a dataset containing point clouds with reflectance values and associated images provided by Leica Geosystems, acquired in the city of Shrewsbury, UK. This point cloud offers smooth reflectances features that reflect well the luminance variation of the materials, almost without any noise. As can be seen in figure 5, it is possible to relight a point cloud by switching its dark points to a sunlight state or switching the sunlight points to a shadow state (see figure 5d).

Other locations displaying strong shadows were tested as well, as shown on figures 6, 7 and 8. In most cases the shadow is properly detected on the ground plane and extracted using the graph cut.

KITTI Dataset

Our second test case is the KITTI Dataset [5]. Due to the nature of data, some pre-processing was performed to obtain a point cloud dense enough with smooth reflectance values. First a set of 20 scans around an image were merged together. From this merged point cloud, the point density was regularized. This point cloud was then colored using the color camera. This small pre-processing yielded a point cloud dense enough to be exploited jointly with the images. Our algorithm was then run with the standard parameters defined in sections 4 and 5. Figure 9 and 10 show that strong shadows were successfully detected by the process. However, some soft shadows located on very bright regions (eg., the shadow of the tree on the white wall on the left) have not been correctly identified as shadows.

Discussion

As explained above, the sharp shadows can be correctly detected and corrected by our process. Unfortunately, in some cases, the relighted areas do not possess the exact same luminance and chromaticity as its original counterpart. This is slightly noticeable in figures 6 and 7 but is very clear on figure 9. Several factors may be responsible for this. First, the illumination model is only an approximation and does not perfectly reflect the illumination of the object (indirect and sky illumination). Second, the light source is supposedly uniform for each point of the cloud. However, illumination power may also vary in the case of a partially clouded sky. These two factors as well as the existence of soft shadows may account for the residual observable color difference. Another limitation lies in the lack of robustness to moving vehicles or pedestrians. They might not be at the same place in the image or in the point cloud which makes the joint exploitation fail.

Conclusion

We introduced a new shadow detection and correction algorithm that relies on the simple but efficient observation that reflectance is only marginally impacted by shadows whereas color information is. Our algorithm makes intensive use of both geometric information and color information working either on the point cloud or in the image plane in each step. Our simplified illumination model may lead however to some remaining artifacts, and in a future work we plan to explore more sophisticated models. Our method is not robust to moving objects, another research direction we want to further explore.

Figure 1 :

 1 Figure 1: Histogram of the different La*b* color channels around a shadow interface.

Figure 2 :

 2 Figure 2: Points detected as potential shadow interfaces (2a), density filtered points (2b), shadow interface points (2c), and shadow mask from the graph cut. The shadow appearing at the bottom left of the graph cut mask (2d) is due to the acquisition vehicle that is visible on the pictures but not on the point cloud.

Figure 3 :

 3 Figure 3: Illumination model of a point. The illumination is decomposed into 3 components: a sky contribution, a sun contribution and an indirect lightening contribution. Each sky ray (θ sky ∈ Ω sky ) contributes an energy E sky , the sun contributes an energy E sun in direction α and the rays corresponding to indirect illumination (θ ind ∈ Ω ind ) contribute an energy E ind . In our simplified model we omit the indirect contribution.

  owed points. It is performed for both the a and b components expressed in the La*b* colorspace. b (p) = b(p) • bS bL and a (p) = a(p) • āS āL (9)

  (a) Shadow border area (b) Binary shadow mask (c) Re-lighted area. (d) Re-lighted area with local median filtering.

Figure 4 :

 4 Figure 4: Small penumbra zones on the boundary of a shadow can have non negligible effect when re-lighting a point cloud.

Figure 5 :

 5 Figure 5: Comparison between the original color and the relighted colors of a fragment of the Pegasus point cloud where the shadows were suppressed.

Figure 6 :Figure 7 :

 67 Figure 6: Comparison between the original color and the relighted colors of a fragment of the Pegasus point cloud

Figure 8 :

 8 Figure 8: Comparison between the original color and the relighted colors of a fragment of the Pegasus point cloud

Figure 9 :

 9 Figure 9: Example of shadow detection and cloud relighting on the KITTI dataset

Figure 10 :

 10 Figure 10: Example of a shadow detection and cloud relighting on the KITTI dataset

Acknowledgment

The authors acknowledge support from ANRT, PhD grant n • 2014/0319.