|
|
ProjectsPorting .NET Micro Framework to Imote2The .NET Micro Framework (MF) makes in possible to program a mote application using a significant subset of C#. The development environment is Visual Studio, and the usual debugging tools are available for single-step execution and state interrogation. This ease of development, combined with the familiarity of C# for many programmers, offers advantages to sensor network programmers. The porting kit for MF has been released to the public. It's a work in progress and we're making an effort to fill in some of the holes. We're working with Crossbow's Imote2, which supports MF and TinyOS. Since we're in a testbed environment, we need to be able to run either OS on a mote at any time; hence we've developed a two-step boot loader: First Step is resident on the mote and it loads either the MF or the TinyOs boot loader as a second step. The USB communication for programs was only from the mote to the host and we've made it two-way. Although MF offers advantages in programming applications, C# is interpreted and therefore slow; and the large body of sensor network protocols that have been developed are almost entirely in NesC for TinyOS. For any of them to be used, they would have to be reimplemented for C#; in many cases, this would be a large undertaking. In consequence, we are looking into whether a NesC-based protocol can be incorporated into MF, exposing appropriate interfaces to user code written in C#. This would let the application be developed in C#, with key protocols executed in NesC code. Fair SchedulingUnifying Share and Weight. Most fair resource schedulers are in the family of Proportional Shared Schedulers (PSS), where the amount of resource a task receives over time is the proportion of its assigned weight as the ratio of the sum of the weights of all tasks. Hence the amount of resource a task gets varies according to the other tasks that are present. We developed MRM, a multimode resource manager in which each task specifies a required share (as a percent) or a weight or both [see 2008icesa]. Share-only tasks receive that amount; weight-only tasks share proportionally in the balance remaining after share values have been satisfied; share and weight tasks receive their share as well as a proportion of the balance. If the sum of shares specified reaches or exceeds 100% then weight-based tasks receive no resource and the share-based tasks receive in proportion to the sum of the shares, providing graceful degradation. We implemented MRM based on the EEVDF (Earliest Eligible Deadline First) scheduler in the Linux 2.6 kernel. We chose EEVDF because it is the fairest of available PSS schedulers. Our implementation, incidentally, constitutes the first PSS scheduler implemented in a modern operating system kernel with preemptive scheduling. We are completing work on a decentralized load balancer that takes into account the relative computing power of asymmetric multiprocessors and achieves an allocation that is close to optimal. DESAL Sensor Network LanguageProgramming sensor networks is notoriously hard. Folklore suggests that a new project requires one PhD and two graduate students working for a year. We developed DESAL, a language whose goal was to hide the complexities of sensor network programming and let domain experts (such as environmentalists) easily develop and deploy new applications [see 2007wsna, 2008icccn]. DESAL is based on Dijkstra's guarded command language using a shared state model. State maintenance via radio or other links is handled by the runtime, hiding the complexity from users. Given the availability of C# on platforms from motes upwards, I'm planning to develop a multi-platform compiler for DESAL. Compositional Frameworks for StabilizationA set of components that are in bad states may individually stabilize to good states but it is possible that the composition does not, since, if one component's state depends in some way on another, the first can corrupt the second. If the components are mutually dependent on each other's state (say, exchanging messages back and forth), then this can lead to a cycle. I've developed two compositional frameworks. My thesis dealt with the "use" relation in a system: an implementation L of some component uses the spec of another component, CSpec, with the understanding that some implementation C of CSpec will be deployed [2001hesis]. This is commonly used in system development. The components involved may each be fault tolerant but in composition they might not be. To avoid global reasoning over the whole system, which could be complex, I provided sufficient conditions under which local reasoning is possible. Briefly, we verify that if C in the presence of faults implements some tolerance spec, CTolSpec, and if L using CTolSpec implements its tolerance spec, LTolSpec, then L using C will implement LTolSpec in the presence of faults affecting C. The thesis also addressed verification of the refinement of a spec.
Two approaches involve a mapping from concrete to abstract states, or
from concrete to abstract variable values. The latter is simpler and was
believed to be relatively complete. In a simple example I showed that in
fact it is not. In addition, refinement is usually viewed as subsetting
of executions. I showed, in the case of components, that this is not so;
see also [ The second framework generalizes to the case that any pair of components in a system can interact [2004icdcs]. Systems are categorized according to flow of corruption and flow of correction between components. An example is stabilization by layers. In this case, A depends on B; if B stabilizes then A does too. Here the flow of corruption is from B to A, since if B is corrupted, A can be corrupted as well. The flow of correction is also from B to A: after B stabilizes, then so does A. Correction relations are classified as acyclic, tree or arbitrary/unknown. Corruption relations are classified as the same or opposite to correction relations, or arbitrary/unknown. The combinations give a hierarchy of system stabilization with increasing levels of complexity. ChowkidarOur group's Kansei wireless sensor network testbed is one of the largest in the world. Since many of the components are commodity items, failures are common. Knowing network health is important to interpreting experiment results and to necessary maintenance. We needed a health monitor that was lightweight, accurate. It had to be suitable for non-IP heterogeneous networks, since Kansei uses Ethernet, Wi-Fi, USB and serial links. Our solution, Chowkidar [2006sss, 2007tridentcom, 2009taas], uses a snap-stabilization PIF (propagation of information with feedback) scheme with low message complexity. Each deployed Chowkidar component knows the available networks at the node and their priority (we might prefer Ethernet to Wi-Fi). A novel 3-way handshake between nodes enforces tree structure and eliminates false negatives. Ohio Coal Research Center (OCRC) Safety SystemOCRC conducts research on fuel cells using gasified high-sulphur coal. The lab uses several toxic and/or explosive gasses and vents into an office building containing offices and classrooms. To mitigate the safety hazard, we designed, implemented and verified a safety monitoring and control system [2006ccc]. In the presence of hazards and equipment failures, the system self-stabilizes to the safest available state, issuing alerts and sounding alarms as appropriate. The system was designed as a composition of self-stabilizing components. By keeping them small, we were able to verify the properties of each component and then separately verify the composition. A somewhat unusual design feature is that the system was specified using the Guarded Command language and was implemented by expanding each command into a decision table. The decision table is interpreted directly by the safety system, so changes in logic, such as alerting options, can be made by an administrator by changing the table rather than recompiling the control program. Despite issues with sensor sensitivity, the system has functioned continuously for several years without missing hazards or causing needless disruption.
|
|