Search

Modern railway stations are controlled by computerized systems called interlockings. In fact the middle size and large size stations usually require to use several interlockings, then forming a network of interlockings. Much research propose to verify the safety properties of such systems by means of model checking. Our approach goes a step further and proposes a method to extend the verification process to a network of interlockings. This process is known as compositional verification. Each interlocking is seen as the component of a larger system (i.e., station) and interacts with its neighbours by means of interfaces. Our first contribution comes in the form of a catalogue of elements that constitute the interfaces (as used in the Belgian railways) and associated contracts. Each interface can then be bound to a formal contract allowing its verification by the ocra tool. Our second contribution comes in the form of an algorithm designed to split the topology controlled by a single interlocking into components. The verification of a large station can therefore be achieved by verifying its constituting components and their interaction thereby tackling the state space explosion problem while providing guarantees on the whole interlocking.

Scheduling consists in deciding when a set of activities must be executed under different constraints, in order to optimize a given objective. The two main types of constraints are precedences between activities, and the availability of finite resources. Common objectives are to minimize the total duration, or to minimize the weighted sum of the tardiness of activities with respect to given due-dates. Scheduling problems are very varied, both in application domains and in featured constraints. They have been a large area of research for decades. A lot of work has been undertaken to express, classify, and solve scheduling problems. Most of these problems are computationally hard to solve (in the sense of being NP-complete) and need complex algorithms (using techniques in the domains of Operations Research and Artificial Intelligence, such as e.g. Constraint Programming, Local and Heuristic Search, Mathematical Programming). But the difficulty lies also in the modeling of the problems, and the mapping between high-level, declarative models and low-level, procedural search techniques. The problem we are tackling is the gap between the high-level modeling of scheduling problems and their efficient resolution. This gap has several causes. First, most search techniques deal with more or less pure problems, and may not be easily adapted to solve problems with side constraints. Second, it requires a strong background in operations research to cast the problem to the right representation. Our goal is to facilitate the work of the user, such that no particular expertise is needed to solve a problem of scheduling. Our contributions in this direction are listed next: * Strong separation between modeling and solving. * Structural analysis and classification of problems. * Synthesis techniques to automatically generate search algorithms for a model. * Simple combination of several search algorithms, to create loosely coupled hybrid algorithms (in particular using Constraint Progr, (FSA 3) -- UCL, 2010

Constrained Optimum Path (COP) problems arise in many real-life applications and are ubiquitous in communication networks. They have been traditionally approached by dedicated algorithms, which are often hard to extend with side constraints and to apply widely. This paper proposes a constraint-based local search (CBLS) framework for COP applications, bringing the compositionality, reuse, and extensibil- ity at the core of CBLS and CP systems. The modeling contribution is the ability to express compositional models for various COP applications at a high level of abstraction, while cleanly separating the model and the search procedure. The main technical contribution is a connected neigh- borhood based on rooted spanning trees to find high-quality solutions to COP problems. The framework, implemented in COMET, is applied to Re- source Constrained Shortest Path (RCSP) problems (with and without side constraints) and to the edge-disjoint paths problem (EDP). Com- putational results show the potential significance of the approach.

Standard state-merging DFA induction algorithms, such as RPNI or Blue-Fringe, aim at inferring a regular language from positive and negative strings. In particular, the negative information prevents merging incompatible states: merging those states would lead to produce an inconsistent DFA. Whenever available, domain knowledge can also be used to extend the set of incompatible states. We introduce here mandatory merge constraints, which form the logical counterpart to the usual incompatibility constraints. We show how state-merging algorithms can benefit from these new constraints. Experiments following the Abbadingo contest protocol illustrate the interest of using mandatory merge constraints. As a side effect, this paper also points out an interesting property of state-merging techniques: they can be extended to take any pair of DFAs as inputs rather than simple strings., Anglais

Forkhead box O (FOXO) transcription factors induce cell growth arrest and apoptosis, which can be prevented by FOXO phosphorylation by AKT in response to growth factors such as platelet-derived growth factors (PDGF). Beside this well-characterized post-translational modification, we showed that FOXO1, FOXO3 and FOXO4 were also regulated at the transcriptional level. PDGF, FGF and IGF-I repressed the expression of FOXO genes in human fibroblasts. This process was sensitive to phosphatidylinositol-3 kinase inhibition by LY294002. FOXO1-specific shRNA decreased FOXO1 mRNA expression and enhanced fibroblast proliferation, mimicking the effects of growth factors. Conversely, ectopic FOXO3 activation blocked the proliferation of fibroblasts, and induced the expression of FOXO1, FOXO4 and p27-KIP1. Using luciferase reporter assays and chromatin immunoprecipitations, we identified a conserved FOXO-binding site in the promoter of the FOXO1 gene, which was required for regulation by PDGF, and mediated the upregulation of FOXO1 by itself and by FOXO3. Altogether, our results suggest that the expression of FOXO1 and FOXO4 genes is stimulated by FOXO3 and possibly by other FOXO factors in a positive feedback loop, which is disrupted by growth factors.

Software engineering requires adequate tool support. Software engineering research is no different. Many researchers in this field build and use advanced tools and prototypes to either validate their own research ideas or advance the state-of-the-art in software engineering tools and techniques. The 2008 European Conference on Object-Oriented Programming introduced the International Workshop on Advanced Software Development Tools and Techniques, the first workshop dedicated to academic tool building. At that workshop, researchers shared their experiences and discussed how to build tools more effectively and efficiently. The 15 tools we looked at covered a broad range of topics, including refactoring, modeling, behavioral specification, static and dynamic program checking, user interface composition, and program understanding. In this column, we identify four emerging trends in academic tool development.

The gene expression profile of metastasizing serotonin-producing neuroendocrine carcinomas, which arise from enterochromaffin cells in the jejunum and ileum, is still largely unknown. The aim of this study was to identify genes and proteins, which are preferentially expressed by neuroendocrine carcinoma and enterochromaffin cells and therefore potential novel biomarkers and/or therapeutic targets. Six carcinoma specimens and six normal ileal mucosas were profiled by Affymetrix microarrays. Advanced bioinformatics identified differentially and specifically expressed genes, which were validated by quantitative real-time-PCR on tumor cells extracted by laser capture microdissection and normal enterochromaffin cells extracted by immunolaser capture microdissection. We identified six novel marker genes for neuroendocrine carcinoma cells: paraneoplastic antigen Ma2 (PNMA2), testican-1 precursor (SPOCK1), serpin A10 (SERPINA10), glutamate receptor ionotropic AMPA 2 (GRIA2), G protein-coupled receptor 112 (GPR112) and olfactory receptor family 51 subfamily E member 1 (OR51E1). GRIA2 is specifically expressed by neuroendocrine carcinoma cells whereas the others are also expressed by normal enterochromaffin cells. GPR112 and OR51E1 encode proteins associated with the plasma membrane and may therefore become targets for antibody-based diagnosis and therapy. Hierarchical clustering shows high similarity between primary lesions and liver metastases. However, chemokine C-X-C motif ligand 14 (CXCL14) and NK2 transcription factor related locus 3 Drosophila (NKX2-3) are expressed to a lower level in liver metastases than in primary tumors and normal enterochromaffin cells, which implies a role in neuroendocrine carcinoma differentiation. In conclusion, this study provides a list of genes, which possess relatively specific expression to enterochromaffin and neuroendocrine carcinoma cells and genes with differential expression between primary tumors and metastases. We verified six nov

This mini-tutorial overviews a blend of complementary techniques for constructing multi-view models for RE. Requirements engineering techniques are faced with a recurring problem of focus and structure. Elicitation techniques raise the problem of focussing and structuring elicitation sessions and artefacts. Evaluation techniques raise the problem of identifying and comparing items at a common level of abstraction and granularity for risk analysis, conflict management, option selection, or prioritization. Specification techniques offer mechanisms for structuring specifications but do not tell us much on how a complex structure should be built through such mechanisms. For quality assurance, inspection techniques are more effective if inspections can be focussed on structured specifications. Validation and verification techniques require the availability of structured specifications as well. Likewise, evolution techniques are more effective when a rich structure is available for defining change units, granularities of traceable items, built-in derivation links, and satisfaction arguments to be replayed in case of change., Anglais

The Feedback with Carry Shift Registers (FCSRs) have been proposed as an alternative to Linear Feedback Shift Registers (LFSRs) for the design of stream ciphers. FCSRs have good statistical properties and they provide a built-in non-linearity. However, two attacks have shown that the current representations of FCSRs can introduce weaknesses in the cipher. We propose a new "ring" representation of FCSRs based upon matrix definition which generalizes the Galois and Fibonacci representations. Our approach preserves the statistical properties and circumvents the weaknesses of the Fibonacci and Galois representations. Moreover, the ring representation leads to automata with a quicker diffusion characteristic and better implementation results. As an application, we describe' a new version of F-FCSR stream ciphers., Anglais

Distance bounding protocols aim at avoiding relay attacks during an authentication process. Such protocols are especially important in RFID, where mounting a relay attack between a low-capability prover and a remote verifier is a realistic threat. Several distance bounding protocols suitable for RFID have been recently suggested, all of which aim to reduce the adversary's success probability and the number of rounds executed within the protocol. Peinado et al. introduced an efficient distance bounding protocol that uses the concept of void challenges. We present in this paper a generic technique called MUltiState Enhancement that is based on a more efficient use of void challenges. MUSE significantly improves the performances of the already-published distance bounding protocols and extends the void challenges to p-symbols., Anglais

Radio Frequency Identification (RFID) allows to identify and authenticate objects or subjects without any physical nor optical contact, using transponders - micro-circuits with an antenna - queried by readers through a radio frequency channel. This technology is one of the most promising of this decade and is already widely used in applications such as access cards, public transportation, payment cards, and passports. This success is partly due to the steadily decrease in both size and cost of passive transponders called tags. The shared enthusiasm for RFID makes people think that everything is do-able with any kind of RFID, especially with low-cost tags. Reality is a bit different. In particular, the characteristics of this technology - ubiquity, low-resource, wireless - open a security breach that should be seriously considered. After a brief introduction about the technology, we will focus in this talk on the security threats. We will propose a classification and show that victims are not only the end-users but they can also be the systems' owners. We will see what is possible today in terms of security and what are the future challenges we will have to address. Among others, we will consider the following topics: privacy, denial of service, relay attacks., Anglais

Energy efficiency is one of the most important issue to be tackled in wireless sensor networks. Activity scheduling protocols aim at prolonging the network lifetime by reducing the proportion of nodes that participate in the application. Among the vast range of criteria existing to schedule nodes activities, area coverage by connected sets is one of the most studied. Active nodes must ensure area coverage while remaining connected in order to guarantee proper data collection to the sink stations. As wireless communications stand for the main source of energy consumption, we investigated the communication redundancy of the active nodes set. We define a path diversity based metric that allows to characterize the communication redundancy of a given set of nodes. We show that one of the most used connectivity criterion is far from building minimal connected sets in terms of communicating nodes involved. Our results open new directions to design localized connected sets solutions., Anglais

RFID-based access control solutions for mobile environments, e.g. ticketing systems for sport events, commonly rely on readers that are not continuously connected to the back-end system. The readers must so be able to perform their tasks even in offline mode, what commonly requires the management by the readers of sensitive data. We stress in this paper the problem of compromised readers and its impact in practice. We provide a thorough review of the existing authentication protocols faced to this constraint, and extend our analysis with the privacy property. We show that none of the reviewed protocols fits the required properties in case of compromised readers. We then design a sporadically-online solution that meets our expectations in terms of both security and privacy., Anglais

Measuring graph similarity is a key issue in many applications. We propose a new constraint-based modeling language for defining graph similarity measures by means of constraints. It covers measures based on univalent matchings, such that each node is matched with at most one node, as well as multivalent matchings, such that a node may be matched with a set of nodes. This language is designed on top of Comet, a programming language supporting both Constraint Programming (CP) and Constraint-Based Local Search (CBLS). Starting from the constraint-based description of the measure, we automatically generate a Comet program for computing the measure. Depending on the measure characteristics, this program either uses CP -which is better suited for computing exact measures such as (sub)graph isomorphism- or CBLS -which is better suited for computing error-tolerant measures such as graph edit distances. First experimental results show the feasibility of our approach., Anglais

This paper presents a novel feature selection method for classification of high dimensional data, such as those produced by microarrays. It includes a partial supervision to smoothly favor the selection of some dimensions (genes) on a new dataset to be classified. The dimensions to be favored are previously selected from similar datasets in large microarray databases, hence performing inductive transfer learning at the feature level. This technique relies on a feature selection method embedded within a regularized linear model estimation. A practical approximation of this technique reduces to linear SVM learning with iterative input rescaling. The scaling factors depend on the selected dimensions from the related datasets. The final selection may depart from those whenever necessary to optimize the classification objective. Experiments on several microarray datasets show that the proposed method both improves the selected gene lists stability, with respect to sampling variation, as well as the classification performances., Anglais

A new generation of widely distributed systems to measure the Internet topology at the interface level is currently being deployed. Cooperation between monitors in these systems is required in order to avoid over-consumption of network resources. This paper proposes an architecture for a distributed topology measurement (DTM) system that, for the first time, decentralizes probing information. The key idea of our proposal is that, by utilizing a shared database as a communication method among monitors and taking advantage of the characteristics of the Doubletree algorithm, we can get rid of a specific control point, and a DTM system can be constructed in a decentralized manner. In this paper, we describe our implementation of a DTM, called Decentralized Tracing System (DTS). Decentralization within DTS is achieved using various distributed hash tables (DHTs), each one being dedicated to a particular plane (i.e., control or data). We also provide preliminary evaluation results., Anglais

Internet topology discovery has been an attractive research field during the past decade. In particular, the research community was interested in modeling the network as well as providing efficient tools, mostly based on traceroute, for collecting data. In this paper, we follow this track of rendering traceroute-based exploration more efficient. We discuss incentives for coupling passive monitoring and active measurements. In particular, we show that high-level information, such as BGP updates, might be used to trigger targeted traceroutes. As a result, the network dynamics might be better capture. We also provide a freely available tool for listening to BGP feeds and triggering dedicated traceroutes., Anglais

Network researchers often need to evaluate newly proposed algorithms and protocols over realistic topologies. Many researchers use random networks for such evaluations. Unfortunately, random networks do not accurately model real networks and important parameters such as link metrics or iBGP configurations are often ignored. We propose IGen, a freely available topology generator that uses network design heuristics to generate realistic IP network topologies. We explain the objectives of IGen and describe the topology generation process in details., Anglais

The objective of the 1st International Workshop on Advanced Software Development Tools and Techniques (WASDeTT-1) was to provide interested researchers with a forum to share their tool building experiences and to explore how tools can be built more effectively and efficiently. The theme for this workshop did focus on tools that target object-oriented languages and that are implemented with object-oriented languages. This workshop report provides a brief overview of the presented tools and of the discussions that took place. The presented tools, 15 in total, covered a broad range of functionalities, among them: refactoring, modeling, behavioral specification, static and dynamic program checking, user interface composition, and program understanding. The discussion during the workshop centered around the following topics: language independent tools, tool building in an industrial context, tool building methodology, tool implementation language, and building tools with external code., Anglais

LS(Graph & Tree) is a local search framework which aims at simplifying the modeling of Constraint Satisfaction Opti- mization Problems on graphs (CSOP on graphs or GCSOP). Optimum Constrained Trees (OCT) problems (a subclass of CSOP on graphs) in which we need to find an optimum sub- tree with additional constraints of a given weighted graph arise in many real-life applications. This paper introduces the LS(Graph & Tree) framework and local search abstrac- tions for OCT problems. These abstractions are applied to model and solve the edge weighted k-Cardinality Tree (KCT) problem. The modeling as well as experimental re- sults show the significance of the abstractions.

Many organizations and many home users have deployed WiFi networks permitting external users to connect to the Internet through their networks. Such WiFi sharing poses many security risks for the visited network as well as for the visiting user. In this paper, we focus on the recently introduced concept for tunneled WiFi roaming in which the infrastructure of the visited network is considered as part of the security architecture. A secure layer-2 tunneling between the user's device and his home network is performed by the visited network only after the successful authentication of all three parties. The authentication protocol provides the mobile device and its home network with a secret key that protects their end-to-end communication. Additionally, it provides another tunnel key, shared with the visited network, that protects the actual traffic exchanged between the visited and home networks and prevents diverse resource consumption attacks against the latter. This concept encourages users to provide roaming service in a more secure and privacy-friendly way. We show how to implement this concept using the IEEE802.11i/EAP framework, based on existing infrastructures and standard tunneling protocols.

Three-party tunnel-based roaming infrastructures may become a future trend to permit mobile users to connect to the Internet when they are not at home. Those solutions takle security issues for both visited networks and mobile users, but require an efficient and scalable accounting protocol. In this paper, we present a lightweight accounting protocol in which the quantity of data that the mobile is allowed to send is gradually increased when cryptographically signed receipts are received.

Redundant connectivity (or multiconnectivity) between autonomous systems (ASes) is important for interdomain traffic engineering and fast recovery in case of failures. However, the redundancy of ASes peering links has not been quantitatively studied, mainly due to the difficulty of obtaining relevant data.

Using quality-of-service (QoS) metrics for Internet traf- fic is expected to improve greatly the performance of many network enabled applications, such as Voice-over-IP(VoIP) and video conferencing. However, it is not possible to con- stantly measure path performance metrics (PPMs) such as delay and throughput without interfering with the network. In this work, we focus on PPMs measurement scalabil- ity by considering machine learning techniques to estimate predictive models from past PPMs observations. Using real data collected from PlanetLab, we provide a comparison be- tween three different predictors: AR(MA) models, Kalman filters and support vector machines (SVMs). Some predic- tors use delay and throughput jointly to take advantage of the possible relationship between PPMs, while other pre- dictors consider PPMs individually. Our current results illustrate that the best performing model is an individual SVM specific to each time series. Overall, delay can be pre- dicted with very good accuracy while accurate forecasting of throughput remains an open problem.

Model checking is an efficient technique for verifying properties on reactive systems. Partial-order reduction (POR) and symbolic model checking are two com- mon approaches to deal with the state space explosion problem in model checking. Traditionally, symbolic model checking uses BDDs which can suffer from space blow- up. More recently bounded model checking (BMC) using SAT-based procedures has been used as a very successful alternative to BDDs. However, this approach gives poor results when it is applied to models with a lot of asynchronism. This paper presents an algorithm which combines partial order reduction methods and bounded model check- ing techniques in an original way that allows efficient verification of temporal logic properties (LT LX ) on models featuring asynchronous processes. The encoding to a SAT problem strongly reduces the complexity and non-determinism of each transition step, allowing efficient analysis even with longer execution traces. The starting-point of our work is the Two-Phase algorithm (Namalesu and Gopalakrishnan) which per- forms partial-order reduction on process-based models. At first, we adapt this algo- rithm to the bounded model checking method. Then, we describe our approach for- mally and demonstrate its validity. Finally, we present a prototypal implementation and report encouraging experimental results on a small example

BGP routing policies are mainly used by network operators to enforce business relationships between Autonomous Systems (AS), and to prefer some routes over others. In this paper, we propose a hierarchical policy model to express each policy at the most appropriate level of abstraction. The model is structured around chains of filters that apply at a specific level of abstraction. To validate our approach, we implemented the model in a Java prototype and used it to reproduce several network-wide routing policies. In all studied networks, the model produced a high-level view of routing policies while preserving their semantics. Our model offers numerous advantages to network operators including, but not limited to, a better network documentation, an improved understanding of routing policies, redundancy suppression, and an easier way of managing their network.

A large ISP typically learns many routes to remote destinations, and these routes differ in terms of their performance, cost, stability, and security properties. An ISP's customers may also have different preferences for the paths that would carry their traffic. For example, financial institutions may prefer the most secure paths (e.g., paths that circumvent untrusted ASes, such as ASes known to censor traffic), while providers of interactive applications like online gaming and VoIP may prefer short paths with low latency. If such options were available, customers might be willing to pay a higher price to have the paths they want. Yet some other customers may be perfectly happy with whatever path the ISP provides for a relatively low price. Yet, today's BGP requires each router to select a single best route, making it difficult for an ISP to select different routes for different customers. In this talk, we describe how an ISP can offer customized route selection using existing router mechanisms. Such a service requires to disseminate multiple BGP routes within the AS, perform customized route selection at each AS border router, and direct data traffic on the chosen interdomain paths. As a proof of concept, we present a configuration supporting customized BGP route selection based on the BGP/MPLS VPN machinery. We evaluate the overhead of our solution, and discuss how new BGP/MPLS VPN router features and protocol enhancements could improve its scalability.

In wireless roaming a mobile device obtains a service from some foreign network while being registered for the similar service at its own home network. However, recent proposals try to keep the service provider role behind the home network and let the foreign network create a tunnel connection through which all service requests of the mobile device are sent to and answered directly by the home network. Such Wireless Roaming via Tunnels (WRT) others several (security) benefits but states also new security challenges on authentication and key establishment, as the goal is not only to protect the end-to-end communication between the tunnel peers but also the tunnel itself. In this paper we formally specify mutual authentication and key establishment goals for WRT and propose an efficient and provably secure protocol that can be used to secure such roaming session. Additionally, we describe some modular protocol extensions to address resistance against DoS attacks, anonymity of the mobile device and unlinkability of its roaming sessions, as well as the accounting claims of the foreign network in commercial scenarios.

To date, mobility and multihoming support in IPv6 have been considered independently of each other, which lead to the publication of the standards Mobile IPv6 and Shim6, respectively. Nevertheless, several use cases that we show prove that there is a strong interest for simultaneous use of these two protocols. In particular, the combined solution allows for replacing the routing optimization mechanism of Mobile IPv6 with a lighter technique, equivalent in functionality, without needing to extend the already defined protocols. We also provide an evaluation of our architecture, based on our publicly available implementation for Linux.

LISP is a map-and-encap solution where the inner header addresses are identifiers and outer header ad- dresses are locators. A set of locators is associate to each identifier via a mapping. Mappings are obtained by querying a mapping system like in DNS where the DNS is queried to resolve a name. Unfortunately, with on-demand mappings, some delay is observed between the reception of a packet by the border router and the time it can effectively be sent when the router sees for the first time the destination identifier. To reduce the impact of such mapping resolution delay, the gleaning functionalityhas been proposed. However, in it original form, the gleaning, introduces a cache poisoning threat. This paper presents an extended gleaning approach that limits the risk of cache poisoning and mitigates the impact of port scanning on the mapping system load

With Intradomain Routing Protocols, by optimizing the configuration (Trafic Engineering -TE) of link weights, operators can significantly improve the load of their links, which is known to be an NP-hard problem. Another emerging issue for ISP networks is the fast restoration of IP services in the case of failures. Recently, Fast Reroute techniques have been proposed for pure IP networks. The Loop Free Alternates (LFA) is one of the most promising technique. An LFA for a router A, for a destination d, is a neighbor C of A which does not use A to reach d, so that A can prepare itself to directly reroute the traffic destined to d along its link with C upon the failure of the link that A is using to reach d. Our objective is to provide a TE technique that takes the coverage of LFAs into account during the network resource usage optimization. Constraint Programming and Constraint-Based Local Search are well suited for solving such complex combinatorial problems. Especially in COMET, some classical problems can be modeled in only about a dozen lines of code. So, we have chosen a local search algorithm implemented in COMET for solving our traffic engineering problem.

This paper addresses the problem of integrating information about user tasks and about the operating environment to the model of a system. Following a modelling based on labelled transition systems, this integration can be done with elementary operations: models synchronization and graph operations. Integration of user tasks and information about operating environment allows to get operational model which represents the knowledge the user should have about the system to perform a set of tasks, given information provided by the operating environment, through user interface for example. The paper draws up a formal way to do the integration to get an operational model which can be used to evaluate and compare different system=s design, to do verification or to generate training material.

This paper discusses the use of formal methods for analysing human-computer interaction. We focus on the mode confusion problem that arises whenever the user thinks that the system is doing something while it is in fact doing another thing. We consider two kinds of models: the system model describes the actual behaviour of the system and the mental model represents the user's knowledge of the system. The user interface is modelled as a subset of system transitions that the user can control or observe. We formalize a full-control property which holds when a mental model and associated user interface are complete enough to allow proper control of the system. This property can be verified using model-checking techniques on the parallel composition of the two models. We propose a bisimulation-based equivalence relation on the states of the system and show that, if the system satisfies a determinism condition with respect to that equivalence, then minimization modulo that equivalence produces a minimal mental model that allows full-control of the system. We enrich our approach to take operating modes into account. We give experimental results obtained by applying a prototype implementation of the proposed techniques to a simple model of an air-conditioner

LISP, the Locator/ID Separation Protocol, proposed by Cisco is an incremental, network-based protocol implementing the separation of the Internet addresses into identifiers and locators spaces. This separation aims at solving some scalability issues the current Internet Architecture is facing. LISP is currently under development within Cisco and our Click implantation can be seen as a laboratory for testing potential new features in the protocol.

We present a methodology and a tool for the problem of testing and verifying that a PDDL planning domain satisfies a set of requirements, a need that arises for instance in space missions. We first review and analyse coverage conditions for requirement-based testing, and present how test cases can be derived automatically from requirements. Additionally, we show how test cases can be translated into additional planning goals. To automate this process, we introduce PDVer, an Eclipse plug-in for the automatic generation of PDDL code from requirements expressed in LTL. We evaluate the effectiveness of our approach and the usability of our tool against the Rovers domain from the fifth International Planning Competition (IPC-5).

The aim of requirements-based testing is to generate test cases from a set of requirements for a given system or piece of software. In this paper we propose a formal semantics for the generation of test cases from requirements by revising and extending the results presented in previous works (e.g. [21, 20, 13]). We give a syntactic characterisation of our method, defined inductively over the syntax of LTL formulae, and prove that this characterisation is sound and complete, given some restrictions on the formulae that can be used to encode requirements. We provide various examples to show the applicability of our approach.

Il est aujourd’hui difficile de parler d’identification par radiofréquence (RFID) sans que ne viennent à l’esprit les termes de "sécurtié de l’information" et de "protection des données personnelles". Nous présentons ici les grandes familles de menaces auxquelles doit faire face la RFID, ainsi que leur impact dans notre vie de tous les jours.

We present a generalization of a class of characteristic polynomials used for linear feedback shift registers (LFSRs). In previous works, several restrictions have been demonstrated for the windmill polynomials. Most notably, no irreducible windmill polynomial was found for a degree d = 3 mod 8. We show how to modify the original definition to overcome those restrictions. We also assess the security of our extended windmill generator considering the case of a filtered LFSR. This paper concerns LFSRs but it can be extended to any kind of shift registers including feedback with carry shift registers (FCSRs) and non-linear feedback shift registers (NLFSRs). We also establish the number of extended windmill polynomials for v = 4,8,16,32 and 64 vanes up to the degree 160.

Aggregation is a very important issue to reduce the energy consumption in Wireless Sensors Networks (WSNs). There is currently a lack of cryptographic primitives for authentication of aggregated data. The theoretical background for Aggregated Message Authentication Codes (AMACs) has been proposed by Chan and Castelluccia at ISIT 08. In this paper, we propose a MAC design based on universal hash functions and more precisely on the Krawczyk’s constructions. We show how those designs can be used for aggregation and how it can be easily adapted for WSNs. Our two AMAC constructions offer a small memory footprint and a signification speed to fit into a sensor. Moreover, when compared with scenarios without aggregation, the method proposed here induces a simulated energy gain between 3 and 9.

In this paper, we study the problem of aggregation of message authentication codes (MACs) in Wireless Sensor Networks (WSNs). We propose to use some of the well known universal hash functions and to modify some of them to define a scheme allowing both data and MACs aggregation

LS(Graph & Tree) is a local search framework which aims at simplifying the modeling of Constraint Satisfaction Optimization Problems on graphs (CSOP on graphs or GCSOP). Optimum Constrained Trees (OCT) problems (a subclass of CSOP on graphs) in which we need to find an optimum subtree with additional constraints of a given weighted graph arise in many real-life applications. This paper introduces the LS(Graph & Tree) framework and local search abstractions for OCT problems. These abstractions are applied to model and solve the edge weighted k-Cardinality Tree (KCT) problem. The modeling as well as experimental results show the significance of the abstractions.

Motivation: Biomarker discovery is an important topic in biomedical applications of computational biology, including applications such as gene and SNP selection from high dimensional data. Surprisingly, the stability with respect to sampling variation or robustness of such selection processes has received attention only recently. However, robustness of biomarkers is an important issue, as it may greatly influence subsequent biological validations. In addition, a more robust set of markers may strengthen the confidence of an expert in the results of a selection method. Results: Our first contribution is a general framework for the analysis of the robustness of a biomarker selection algorithm. Secondly, we conducted a large-scale analysis of the recently introduced concept of ensemble feature selection, where multiple feature selections are combined in order to increase the robustness of the final set of selected features. We focus on selection methods that are embedded in the estimation of support vector machines (SVMs). SVMs are powerful classification models that have shown state-ofthe-art performance on several diagnosis and prognosis tasks on biological data. Their feature selection extensions also offered good results for gene selection tasks. We show that the robustness of SVMs for biomarker discovery can be substantially increased by using ensemble feature selection techniques, while at the same time improving upon classification performances. The proposed methodology is evaluated on four microarray data sets showing increases of up to almost 30% in robustness of the selected biomarkers, along with an improvement of about 15% in classification performance. The stability improvement with ensemble methods is particularly noticeable for small signature sizes (a few tens of genes), which is most relevant for the design of a diagnosis or prognosis model from a gene signature.

This paper addresses feature selection techniques for classification of high dimensional data, such as those produced by microarray experiments. Some prior knowledge may be available in this context to bias the selection towards some dimensions (genes) a priori assumed to be more relevant. We propose a feature selection method making use of this partial supervision. It extends previous works on embedded feature selection with linear models including regularization to enforce sparsity. A practical approximation of this technique reduces to standard SVM learning with iterative rescaling of the inputs. The scaling factors depend here on the prior knowledge but the final selection may depart from it. Practical results on several microarray data sets show the benefits of the proposed approach in terms of the stability of the selected gene lists with improved classification performances.

This paper elaborates on some of the fundamental contributions made by John Mylopoulos in the area of Requirements Engineering. We specifically focus on the use of goal models and their soft goals for reasoning about alternative options arising in the requirements engineering process. A personal account of John=s qualitative reasoning technique for comparing alternatives is provided first. A quantitative but lightweight technique for evaluating alternative options is then presented. This technique builds on mechanisms introduced by the qualitative scheme while overcoming some problems raised by it. A meeting scheduling system is used as a running example to illustrate the main ideas

Process models capture tasks performed by agents together with their control flow. Building and analyzing such models is important but difficult in certain areas such as safety-critical healthcare processes. Tool-supported techniques are needed to find and correct flaws in such processes. On another hand, event-based formalisms such as Labeled Transition Systems (LTS) prove effective for analyzing agent behaviors. The paper describes a blend of state-based and event-based techniques for analyzing task models involving decisions. The input models are specified as guarded high-level message sequence charts, a language allowing us to integrate material provided by stakeholders such as multi-agent scenarios, decision trees, and flowchart fragments. The input models are compiled into guarded LTS, where transition guards on fluents support the integration of state-based and event-based analysis. The techniques supported by our tool include model checking against process-specific properties, invariant generation, and the detection of incompleteness, unreachability, and undesirable non-determinism in process decisions. They are based on a trace semantics of process models, defined in terms of guarded LTS, which are in turn defined in terms of pure LTS. The techniques complement our previous palette for synthesizing behavior models from scenarios and goals. The paper also describes our preliminary experience in analyzing cancer treatment processes using these techniques.

Equivalences, partitions and (bi)simulations are usually tackled using concrete relations. There are only few treatments by abstract relation algebra or category theory.We give an approach based on the theory of semirings and quantales. This allows applying the results directly to structures such as path and tree algebras which is not as straightforward in the other approaches mentioned. Also, the amount of higher-order formulations used is low and only a one-sorted algebra is used. This makes the theory suitable for fully automated first-order proof systems. As a small application we show how to use the algebra to construct a simple control policy for infinite-state transition systems.