922 resultados para Static verification
Resumo:
Consider the problem of scheduling sporadic messages with deadlines on a wireless channel. We propose a collision-free medium access control (MAC) protocol which implements static-priority scheduling and present a schedulability analysis technique for the protocol. The MAC protocol allows multiple masters and is fully distributed; it is an adaptation to a wireless channel of the dominance protocol used in the CAN bus. But unlike that protocol, our protocol does not require a node having the ability to receive an incoming bit from the channel while transmitting to the channel.
Resumo:
We propose a wireless medium access control (MAC) protocol that provides static-priority scheduling of messages in a guaranteed collision-free manner. Our protocol supports multiple broadcast domains, resolves the wireless hidden terminal problem and allows for parallel transmissions across a mesh network. Arbitration of messages is achieved without the notion of a master coordinating node, global clock synchronization or out-of-band signaling. The protocol relies on bit-dominance similar to what is used in the CAN bus except that in order to operate on a wireless physical layer, nodes are not required to receive incoming bits while transmitting. The use of bit-dominance efficiently allows for a much larger number of priorities than would be possible using existing wireless solutions. A MAC protocol with these properties enables schedulability analysis of sporadic message streams in wireless multihop networks.
Resumo:
Consider the problem of scheduling a set of sporadically arriving tasks on a uniform multiprocessor with the goal of meeting deadlines. A processor p has the speed Sp. Tasks can be preempted but they cannot migrate between processors. On each processor, tasks are scheduled according to rate-monotonic. We propose an algorithm that can schedule all task sets that any other possible algorithm can schedule assuming that our algorithm is given processors that are √2 / √2−1 ≈ 3.41 times faster. No such guarantees are previously known for partitioned static-priority scheduling on uniform multiprocessors.
Resumo:
Consider the problem of scheduling real-time tasks on a multiprocessor with the goal of meeting deadlines. Tasks arrive sporadically and have implicit deadlines, that is, the deadline of a task is equal to its minimum inter-arrival time. Consider this problem to be solved with global static-priority scheduling. We present a priority-assignment scheme with the property that if at most 38% of the processing capacity is requested then all deadlines are met.
Resumo:
This paper studies static-priority preemptive scheduling on a multiprocessor using partitioned scheduling. We propose a new scheduling algorithm and prove that if the proposed algorithm is used and if less than 50% of the capacity is requested then all deadlines are met. It is known that for every static-priority multiprocessor scheduling algorithm, there is a task set that misses a deadline although the requested capacity is arbitrary close to 50%.
Resumo:
The three-dimensional (3D) exact solutions developed in the early 1970s by Pagano for simply supported multilayered orthotropic composite plates and later in the 1990s extended to piezoelectric plates by Heyliger have been extremely useful in the assessment and development of advanced laminated plate theories and related finite element models. In fact, the well-known test cases provided by Pagano and by Heyliger in those earlier works are still used today as benchmark solutions. However, the limited number of test cases whose 3D exact solutions have been published has somewhat restricted the assessment of recent advanced models to the same few test cases. This work aims to provide additional test cases to serve as benchmark exact solutions for the static analysis of multilayered piezoelectric composite plates. The method introduced by Heyliger to derive the 3D exact solutions has been successfully implemented using symbolic computing and a number of new test cases are here presented thoroughly. Specifically, two multilayered plates using PVDF piezoelectric material are selected as test cases under two different loading conditions and considering three plate aspect ratios for thick, moderately thick and thin plate, in a total of 12 distinct test cases. (C) 2013 Elsevier Ltd. All rights reserved.
Resumo:
Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do grau de Mestre em Engenharia Informática.
Resumo:
A good verification strategy should bring near the simulation and real functioning environments. In this paper we describe a system-level co-verification strategy that uses a common flow for functional simulation, timing simulation and functional debug. This last step requires using a BST infrastructure, now widely available on commercial devices, specially on FPGAs with medium/large pin-counts.
Resumo:
Thesis for the Degree of Master of Science in Biotechnology Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia
Resumo:
The container loading problem (CLP) is a combinatorial optimization problem for the spatial arrangement of cargo inside containers so as to maximize the usage of space. The algorithms for this problem are of limited practical applicability if real-world constraints are not considered, one of the most important of which is deemed to be stability. This paper addresses static stability, as opposed to dynamic stability, looking at the stability of the cargo during container loading. This paper proposes two algorithms. The first is a static stability algorithm based on static mechanical equilibrium conditions that can be used as a stability evaluation function embedded in CLP algorithms (e.g. constructive heuristics, metaheuristics). The second proposed algorithm is a physical packing sequence algorithm that, given a container loading arrangement, generates the actual sequence by which each box is placed inside the container, considering static stability and loading operation efficiency constraints.
Resumo:
Trabalho final de Mestrado para a obtenção do grau de mestre em Engenharia Civil
Resumo:
Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do Grau de Mestre em Engenharia Informática
Resumo:
Proceedings of the First International Conference on Coastal Conservation and Management in the Atlantic and Mediterranean, p. 193-200
Resumo:
Over the past decades several approaches for schedulability analysis have been proposed for both uni-processor and multi-processor real-time systems. Although different techniques are employed, very little has been put forward in using formal specifications, with the consequent possibility for mis-interpretations or ambiguities in the problem statement. Using a logic based approach to schedulability analysis in the design of hard real-time systems eases the synthesis of correct-by-construction procedures for both static and dynamic verification processes. In this paper we propose a novel approach to schedulability analysis based on a timed temporal logic with time durations. Our approach subsumes classical methods for uni-processor scheduling analysis over compositional resource models by providing the developer with counter-examples, and by ruling out schedules that cause unsafe violations on the system. We also provide an example showing the effectiveness of our proposal.
Resumo:
The Internet of Things (IoT) has emerged as a paradigm over the last few years as a result of the tight integration of the computing and the physical world. The requirement of remote sensing makes low-power wireless sensor networks one of the key enabling technologies of IoT. These networks encompass several challenges, especially in communication and networking, due to their inherent constraints of low-power features, deployment in harsh and lossy environments, and limited computing and storage resources. The IPv6 Routing Protocol for Low Power and Lossy Networks (RPL) [1] was proposed by the IETF ROLL (Routing Over Low-power Lossy links) working group and is currently adopted as an IETF standard in the RFC 6550 since March 2012. Although RPL greatly satisfied the requirements of low-power and lossy sensor networks, several issues remain open for improvement and specification, in particular with respect to Quality of Service (QoS) guarantees and support for mobility. In this paper, we focus mainly on the RPL routing protocol. We propose some enhancements to the standard specification in order to provide QoS guarantees for static as well as mobile LLNs. For this purpose, we propose OF-FL (Objective Function based on Fuzzy Logic), a new objective function that overcomes the limitations of the standardized objective functions that were designed for RPL by considering important link and node metrics, namely end-to-end delay, number of hops, ETX (Expected transmission count) and LQL (Link Quality Level). In addition, we present the design of Co-RPL, an extension to RPL based on the corona mechanism that supports mobility in order to overcome the problem of slow reactivity to frequent topology changes and thus providing a better quality of service mainly in dynamic networks application. Performance evaluation results show that both OF-FL and Co-RPL allow a great improvement when compared to the standard specification, mainly in terms of packet loss ratio and average network latency. 2015 Elsevier B.V. Al