dataesr/scientific-paragraphs-categorization huggingface dataset:
Data collectionmodel Different surveillance applications have different data collection model. For instance, water level may be taken into account in the data collection model of a flooding surveillance. However, temperature, humidity, light intensity, wind, hopper density are considered as factors in a BPH surveillance data model. To be simple, the data model consists of 2 entities TData, TSensingData which has relations with TCell and TSensor, respectively. Fields in these 2 entities are almost the same such as: time stamp and other environmental factors. The difference is the TData depicts the data generated from the physical system while TSensingData contains sampling sensing data from surrounding conditions. For example, the data collection model of a BPH surveillance network is as followed (figure  17 ):.
Scenario: physical system and networksystem synchronization This simulation depicts the interaction between the insect physical system and WSN system in the BPH surveillance network. Sampling data from sensor nodes play as inputs for the insect physical system. On the other hands, when the insect physical system occurs, the collected data from sensor nodes the damage level caused by BPHs. In the beginning, the WSN gives environmental conditions at 8 locations of sensor nodes. The temperature is 30 o C (the common temperature in Mekong Delta). The wind direction is 2 (the direction from the center cell to cell 5 in figure  8  with the velocity is 5km/h (approximately 10 hexagonal cells/h). That means BPHs can transmit to the cell distance 10 from the source cell in one hour. Besides, almost rice fields in Cantho are almost young and suffer lightly from hoppers (light infection color of rice fields and sensor nodes as in figure  20 ).
With the ubiquitous usage of mobile devices, most communications are now impacted by the users' mobility. Therefore, applications and services must be designed to cope with network dynamics produced by those mobility patterns. Software research and development would benefit from taking device mobility into account. However, implementing and testing software on real devices is costly and cumbersome to perform. Virtualization is a widely used technique for avoiding these issues. In this paper, we propose three tools for creating and managing networks with mobile devices. Both network devices and user devices are emulated, the latter by using the QEMU system emulator. We implemented a virtual network device that can emulate access points and wireless interfaces, a real-time mobility engine that controls the dynamics of the connections and a control and management tool.
INTRODUCTION Mobile devices' hardware is usually not based around the typical x86/x64 processor architecture commonly found on laptops, desktops and servers. Virtualization is thus a practical and efficient way to help develop software on those MobileSoft  '16, May 16-17 2016 , Austin, TX, USA ACM ISBN 978-1-4503-4178-3/16/05. DOI: http://dx. doi. org/10. 1145/2897073. 2897087 specific platforms. However, mobile devices also have a mobility behavior that was not relevant for regular applications running on laptops or desktops and that should now be taken into account. Setting up a hardware-based network testbed to do this is expensive and cumbersome. In particular, changing the network topology and the network parameters of a hardware testbed is time consuming and error-prone. Virtualizing the device is thus a first step but being able to virtualize the network where the device sits in would be a substantial improvement as network dynamics could then be emulated with ease.
Overall Design The toolset is composed of three different programs: • a C++ program called virtual network device (vnd ), that can emulate links, hubs and switches but also access points and wireless interface cards (WIC), • a C++ program called network mobilizer (nemo), which contains an event processor and a real-time mobility engine that controls the dynamics of the connections between the devices over time, • and a Python program called Network Emulator for Mobile Universes (NEmu), which controls the two programs above as well as manages the virtual devices and the virtual machines running on QEMU. NEmu also provides a Command-Line Interface (CLI) for the users of our toolset and as such, we also call the whole toolset NEmu. NEmu is based on the concept of Network Virtualization Environment (NVE) introduced by Chowdhury and Boutaba in  [12].
Network Emulator for Mobile Universes NEmu as a tool is a Python program consisting of 8000 lines of code which allows users to build dynamic virtual network infrastructures including mobile devices and mobile ad hoc networks. To this end NEmu is based on several building blocks. NEmu uses virtual nodes connected by virtual links in order to create a virtual network topology. A virtual topology can be hosted by one or several physical hosts. The part of the virtual topology laying on a given physical host represents a NEmu session which is configured by the NEmu manager.
Virtual Links A virtual link for NEmu is an emulated network connection between virtual nodes. Many types of virtual links currently exist in NEmu. Here are the most relevant: • A VHub is a virtual hub emulating a physical Ethernet hub and interconnecting several nodes. • A VSwitch is a virtual switch emulating a physical Ethernet switch and interconnecting several nodes. • A VRemote represents a special point-to-point link which inter-connects a virtual element to a distant one (i. e. , residing on another physical host) without breaking the isolation of the whole virtual network. • A VSlirp represents a special point-to-point link which inter-connects a virtual node via a NAT'ed virtual interface to a real network interface card on the physical host. • A VTap represents a special point-to-point link which inter-connects a virtual element to the physical machine through a Linux tap interface.
• A VAirWic represents a wireless interface connector. • A VAirAp is a wireless access point for wireless/wired connections. Virtual links are configured by the user in NEmu commands or scripts. Virtual links carry streams or frames from one virtual node to one or more others. The traffic is tunneled between virtual nodes by using so-called backend connections. NEmu uses our vnd program to emulate network devices. The advantages of using a vnd is that the user can set the bandwidth, delay, jitter and bit error rate on any interface in any mode whereas QEMU offers no control over its hub emulation. In addition, NEmu also provides a Slirp which is a special type of link whose purpose is to provide Internet access to the virtual node. It is an emulation of a NATed access to the real Internet by using the physical host NIC.
Sessions & Manager As already said above, a NEmu session represents a complete configuration of a network topology residing on a physical host (i. e. , storage, virtual nodes' configurations and links). A distributed virtual network on n physical hosts consists in n NEmu sessions at least. A session is represented by an auto-generated directory in order to be saved and re-used. A session can be saved as a sparse archive which compresses all elements and which is compatible with sparse files unlike traditional archives. The NEmu manager is the CLI to manipulate a session. Sessions are independent even if they are part of the same network topology. The manager can be used in three ways: • as a Python module to be integrated in another script or program; • as a dynamic Python interpreter; • as a Python script launcher.
Implementation The vnd is implemented in C++, contains around 6000 lines of code, and uses the following libraries: • Boost libraries  [14] : thread, chrono, system, regex, bind, and the asynchronous input/output library called asio. • SSL libraries (for creating SSL backend connections). • Linux-specific libraries: VDEplug (for connecting to VDE switches). The vnd can be used directly through a rudimentary CLI or can be entirely controlled by NEmu which then acts as the user interface. It is a lightweight program using around 250 KBytes in RAM and it is portable on the majority of UNIX and Windows variants. The code is open source 2 and licensed under the LGPLv3. In the domain of virtualization, the term network backend is often used to designate the software part of an emulator that enables the connection of the emulator to the other emulators either on the same physical machine or on different ones.
Network Mobilizer Our toolset can emulate mobile devices and networks. Thus, it is possible to create a virtual network topology that evolves over time such as a Mobile Ad-hoc Network (MANET). In order to manage mobility, NEmu uses the nemo mobility engine. nemo is a lightweight C++ program which can generate connectivity scenarios for mobile devices and networks. A connectivity scenario is a timestamped list of wireless link connection and disconnection events between wireless devices (e. g. , mobile nodes, access points). In order to emulate device mobility and network dynamics, nemo leverages some features of our vnd software, such as the ability to create or delete virtual links on-thefly and to dynamically modify link characteristics. nemo is able to send orders to NEmu in real time for emulating the connectivity changes between mobile nodes by creating, destroying or changing the characteristics of the links at the appropriate time.
As a rule of thumb, a time precision of 1 ms is probably the best that can be achieved in real time, thus an upper limit for the sampling frequency would be around 1000 computations per second. The code that evaluates the connectivity between all nodes at each time interval has a worst-case computation complexity of O(n 2 × log2(n)), with n being the number of nodes in the scenario. However, as n is usually small and as the processor is written in C++ for performance, the total computation time remains usually below the simulated time duration of the scenario. Plus, this computation is done only by the processor in the first phase of the nemo usage in order to generate the connectivity scenario. It is not done when launching the real-time scheduler. To assess the computation complexity of the connectivity computation, we have generated random scenarios for 5 different network sizes, with a time interval of 10 ms (i.
The real-time scheduler can be paused/resumed at any time by the user. As opposed to NEmu, nemo is not distributed (i. e. , , only one program instance of nemo may be running a given connectivity scenario). Indeed, nemo must know the positions of all the devices at any given time. It is recommended that all the virtual machines emulating mobile devices should reside on the same physical host in order to avoid degrading performance, as sending orders over the physical network may add significant delay. Some network backends, such as sockets, used by the vnd introduce delays and may reduce the temporal precision even on a single physical machine. The latter will be at best of the order of the millisecond as previously mentioned. As our toolset targets the development and testing of non-safety-critical applications, we assume that this precision is enough.
Implementation nemo can be used directly through a rudimentary CLI or can be entirely controlled by NEmu which then acts as the user interface. nemo is implemented in C++, contains around 3000 lines of code, and is using the following Boost libraries: thread, chrono and system. Remote control of nemo also requires the regex, bind and asio libraries. It is a lightweight program using around 1 MByte in RAM and it is portable on the majority of UNIX and Windows variants. The code is open source 3  and licensed under the LGPLv3. In order to emulate wireless communications between ral links, nemo implements the two-ray ground-reflection model and mimics the bitrates vs sensitivity levels of three WICs: Cisco Aironet, 3Com Xjack and Lucent Wavelan. nemo does not yet currently take into account the MAC layer access and contention mechanisms.
In order to avoid, or at least to reduce the effects of this phenomenon, AMiRALE includes several user mechanisms called filters which enable, notably, to limit the re-emission of the same message. We evaluate the output data rates generated by AMi-RALE as a function of the filters' configuration. The application scenario consists in a team of ground robots which has to collect a given number of items of garbage in a park. Garbage and robots are placed randomly in the park at the beginning of the scenario. Mobile ground robots are moving by following the random way-point mobility model  [9]. Each robot is specialized, which means that it can only clean one kind of garbage (e. g. , glass, paper, compost). When a robot finds an item of garbage which it is not able to collect itself, it generates a new mission in order to inform other robots of the existence of this item of garbage.
RELATED WORK Network virtualization has been proposed and studied for quite some time and many tools are currently available. Dynamips  [17]  is a CISCO hardware emulator. Dynagen their inter-connections. However, the network dynamics of the links of the topology are strongly limited (mainly on/off by the user) and adding network services is quite difficult. GNS  [19]  is an open source software which allows to build a virtualized network topology with Dynamips, VirtualBox and QEMU virtual machines. However, it does not provide the possibility to build a community network spread on several physical machines and adding network services is as complicated as in Dynagen. Finally GNS is hardly usable without any graphical interface making difficult the creation and management of a complex network.
Nodes and links are managed inside the operating system kernel which implies strong limitations in terms of flexibility. MobiEmu simulates mobile networks through ns3 for the mobility and LXC containers for nodes. However, it may happen that, due to the processing inherent in the execution of simulation events, the simulator cannot keep up with real-time execution as indicated in the ns3 manual. Furthermore LXC containers cannot emulate mobile devices typically running on different processor types (i. e. , ARM instead of Intel based). NET  [30]  is a powerful hardware-based infrastructure which allows to perform realistic experimentation on mobile networks. However, this solution uses real network inter-connection devices (i. e. , switches, etc. ) in order to build the virtual network. Similarly to our vnd software, some other existing tools enable the creation of emulated customized virtual switches.
VDE  [13]  is a virtual switch which inter-connects virtual machines through the shared memory system inside the Linux kernel. VDE does not include any mechanism in order to manipulate link properties like bandwidth, delay, etc. Open vSwitch  [33]  is an open source project which enables to instantiate virtual switches with a high customization of vir-tual links. However, this software relies on virtual network interfaces inside the Linux kernel thus lacking flexibility in terms of backend connections. Vnet  [37]  is a distributed inter-connection system which enables to link several virtual machines which lay on different physical hosts. Even if the system is distributed, it does not provide any link customization mechanism. In addition, all these virtual switch solutions do not enable access point emulation.
Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring. In this article, we consider a refactoring operation (renaming of global variables in C), and we prove that its core implementation preserves the set of possible behaviors of transformed programs. That proof of correctness relies on the operational semantics of C provided by CompCert C in Coq.
Proving properties of refactoring tool operations Testing and proving are complementary approaches to software validation. Although the need for safe refactoring tools is recognized  [17, 3] , few efforts have been done to prove the correctness of such tools. In many research papers on refactoring, correctness is discussed informally. Some papers give formal arguments, but they either do not cover completely the preservation of behaviors (for instance:  [16] ) or they do not cover a complete programming language (for instance:  [10] ). Also, existing mechanized proofs cover only theoretical languages (for instance:  [22, 21] ). There is a gap between the tools that are available for mainstream languages and the tools that are reliable. Formalized refactoring in CompCert C. Our goal in this paper is to make a step towards a fully formalized refactoring tool for an industrial language.
We choose to work on the language C because it has a mechanized formalization: CompCert C  [2, 9]. We present in section 2 how we use CompCert C to build a refactoring tool. Then we focus on a refactoring operation: renaming global variables. Renaming seems to be inoffensive at first sight, but we will see that there are some pitfalls to be avoided 1 The author reported several bugs in the Haskell Refactorer  (2010, 2011). (Sec. 3. 1). We show how our implementation handles several situations of shadowing (Sec. 3. 2) and that it preserves the behavior of programs (Sec. 3. 4. 1). We also give a sufficient precondition for the operation (Sec. 3. 4. 2). All the properties we give are proved in Coq. The full code with the proofs is available from the author or the project web-page.
Refactoring in CompCert C To be able to prove properties on the behavior of transformed programs, we need a formal definition of the semantics of programs. We rely on the semantics of C programs formalized in Coq by CompCert C, which takes into account a subset of ISO C 99 larger than MISRA C 2004  2. That semantics (module Csem in CompCert) is defined on abstract syntax trees (AST). For this reason, we focus on AST transformations in this paper. This allows to verify the logic of the transformation, but it also has some limits as described below (Sec. 2. 4). Programs (AST. program) are represented by a list of definitions (or declarations) of global variables and functions. A definition is represented by a pair (i, d) where i is the defined identifier and d is the content of that definition.
Program Transformations Our prototype follows the data-flow given in Fig 1. We use CompCert lexer, parser and pretty-printer. The core refactoring is performed on parsed syntax trees. Then the transformed AST are pretty-printed to recover a source file. Most refactoring tools transform simultaneously the syntax tree and the token stream in order to recover the layout in the source file, but this is out of the scope of this paper. A program transformation may fail and return an error (Error constructor with a message) or succeed and return the transformed AST (OK constructor with the resulting program, see the module Errors of CompCert).
External Functions The problem. In C, linked libraries have access to global variables of the program as in the following example (consider the source code of the library is not available): We generally cannot or do not want to propagate the renaming in libraries. Here, renaming a into b only in the main program would change the behavior (it introduces an error). 3 ufficient Condition as an Hypothesis. Analysis of the compiled code of libraries is out of the scope of our prototype. So we have to assume that the renamed variable is not accessed from external code. We also assume that the new name is not used for a global variable or function in the library. Those assumptions are formalized by a predicate, extcall additional properties (see module ExtCall in the distributed source code). That predicate is used as a precondition for our result on behavior preservation, (hypothesis EXT1 in Fig.
Implementation of the transformation We now describe our implementation. In the following, we consider x is the name to be changed, y is the new name, and x = y. Pre-operations. Before calling the transformation defined in Coq we perform the following operations (coded in OCaml): 1. Check that y is not a C keyword. This cannot be done in the Coq part because identifiers are represented by numbers in syntax trees. 2. Trigger parsing. We use the CompCert parser, but we must not use the feature of the CompCert compiler that changes the names of the variables to have a unique name for each variable. Otherwise, we would have no way to detect shadowings in the AST. Top-level checks and transformation. When the AST is available from parsing, the transformation defined in Coq (function rename globvar hard in module Programs) makes the following verifications: 1.
Hypothesis EXT1 : ∀ name sig, ExtCall. extcall additional properties (Events. external functions sem name sig) x y. Hypothesis EXT2 : ∀ text, ExtCall. extcall additional properties (Events. inline assembly sem text) x y. Variable p : program. Hypothesis RG : RawGlobals. rawglobals p. Theorem behavior preserved 1 :   Structure of the Proof. The key point to prove the result of forward simulation above is the preservation of transitions (lemma step commut of Fig. 4 ). x = y → ∀ ( To prove this, we build a correspondence between states coming from the execution of the initial program with states in the execution of the transformed program (function change ident in module State). That correspondence relies on correspondences we build on continuations, on contexts, and on global environments. Some aspects of the proof are further discussed in App.
The scale is then used to construct a table summarizing the evaluation of approaches according to the criteria. CLEMENTS  [6]  makes a taxonomic study of ADLs. He characterizes these languages in terms of: class of systems they support, properties inherent to languages themselves, processes and technological supports that they provide to represent, refine, analyze and build systems from an architecture. He based himself on the results of a questionnaire produced and distributed to the owners of ADL, and which has allowed to characterize each ADL in terms of type of systems and architectures it supports, types of analysis that it facilitates or offer and of intrinsic qualities. The results of this survey are summarized in a table containing all the ADL considered. The works presented above deal with the comparison of approaches to design real-time systems, but some of them (  [2]   [6] ) do not take into account recent languages such as SysML, AADL, MARTE, others ([3]-  [6] ) focus on languages and do not address methods.
Some of the works presented (  [2] ) have a scoring method based on the authors' experience. Although this scoring method has the advantage of allowing to benefit from the experience of the authors, their disadvantage is to be quite subjective. Indeed, the scores based on authors' experience can quickly vary from one experiment to another. Furthermore, dependability that is an important property in the majority of real time and embedded systems, is not taken into account in almost all of these works (  [2]  [4]  [5] ). The goal of our work is to provide an objective comparison of approaches dedicated to the design of real-time and embedded systems, taking into account both modelling languages and design methods, including recent modelling languages (SysML, AADL, MARTE), and incorporating the criterion of dependability.