Data-intensive applications require extreme scaling of their underlying storage systems. Such scaling, together with the fact that storage systems must be implemented in actual data centers, increases the risk of data loss from failures of underlying components. Accurate engineering requires quantitatively predicting reliability, but this remains challenging due to the need to account for extreme scale, redundancy scheme type and strength, distribution architecture, and component dependencies. This article introduces CQS im -R, a tool suite for predicting the reliability of large-scale storage system designs and deployments. CQS im -R includes (a) direct calculations based on an only-drives-fail failure model and (b) an event-based simulator for detailed prediction that handles failures of and failure dependencies among arbitrary (drive or nondrive) components. These are based on a common combinatorial framework for modeling placement strategies. The article demonstrates CQS im -R using models of common storage systems, including replicated and erasure coded designs. New results, such as the poor reliability scaling of spread-placed systems and a quantification of the impact of data center distribution and rack-awareness on reliability, demonstrate the usefulness and generality of the tools. Analysis and empirical studies show the tools’ soundness, performance, and scalability.

Multi-player games played outdoors on smartphones can be designed to improve players' health by requiring vigorous physical activity in an interesting and challenging natural environment, while still providing engaging virtual elements and enabling social interaction. However, to achieve these goals, game elements must not be too screen-oriented, because staring at the device screen degrades one's skill and safety in running, jumping, and climbing. We should instead design game elements in ways that allow them to be experienced with minimal or no screen reading. On the other hand, matching outcomes with user expectations is a major challenge, due to the inaccuracy of device sensors and the realities of communications in outdoor field conditions. This paper describes a design for point-and-shoot weapons that allows the player simply to point the smartphone and tap to shoot. The design includes a computational procedure for engineering implementations to a given accuracy standard and has three variants supporting different types of game experience. We evaluate the design using both Monte Carlo simulations and data gathered from an implemented instance within the iTESS Geocast Game.

An important but relatively less studied class of network layer protocol for sensor networks is geocast. It allows a sensor node to send messages to all nodes in a given geographical area without the sender node having any knowledge about which nodes are present in that area. Developing a robust geocast protocol for practical sensor networks poses several challenges. Geocast messages should be reliably delivered to the destination area in the presence of unreliable wireless links, a typical characteristic of practical sensor network deployments. The protocol should minimize the number of radio transmissions and avoid control traffic to save energy, which is a scarce resource in sensor networks. The protocol should be robust against a wide range of network densities. This paper presents the design, implementation, and evaluation of SGcast - a reliable, robust, and energy-efficient geocast protocol that achieves these goals. For a wide range of experiments conducted using networks of real sensor nodes and simulations, we show that compared to a recent geocast protocol, SGcast achieves up to 11.08x reduction in energy consumption and up to 2.17x improvement in successful delivery of geocast messages to the destination area, while being robust against a wide variability in network densities.

Distributed embedded systems, such as multi-player smartphone games, training instrumentation systems, and “smart” homes, naturally have complex requirements. These are difficult to elicit, represent, validate, and verify. For high confidence, one demands that the represented requirements reflect realistic uses of the system; however, such uses, often representing human actions in complex environments, can have hundreds to thousands of steps and be impractical to elicit and manage using only declarative or intensional (computed) representations. Non-functional requirements like scalability increase this complexity further. In this paper, I show how one can bootstrap requirements using data captured from initial prototypes deployed in small scale real world tests. Using such captures as seeds, I show how a calculus of transformations on captures, from captures to scenarios, among scenarios, and from scenarios back to captures can be used in several requirements engineering tasks. I describe a novel ecosystem of tools and transformations that implement this capture calculus and illustrate its use on data obtained from the domain of multi-player outdoor smartphone games.

Geographic addressing of packets within mobile ad hoc networks enables novel applications, including hard real-time engagement simulation in military training systems, geographic command and control functions in training and emergency communications, and commercial messaging applications as well. The most scalable implementation of geoaddressing is via a geocast protocol, where nodes selectively retransmit packets based on local decision rules. Well-designed retransmission heuristics yield scalable geographic flooding that outperforms alternative geoaddressing approaches. However, previous geocast implementations, while effective, fall into two categories. Approaches based on flooding are unscalable due to the high load they generate. Scalable approaches, on the other hand, have trouble in complex environments, lacking sufficient intelligence about the necessary directionality of packet flow. The present paper defines a novel geocast heuristic, the Center Distance with Priority (CD-P) Heuristic, which both significantly improves on reliability of existing scalable geocasts and yet also remains scalable as scenario complexity increases. This paper describes the new technique as well as an evaluation study comparing it to previous approaches.

Quantum computers can solve a few basic problems, such as factoring an integer and searching a database, much faster than classical computers. However, the complexity of software artifacts, and the types of questions software engineers ask about them, pose significant challenges for applying existing quantum approaches to software engineering search (SES) problems. This paper first describes a new quantum search algorithm, IDGS-FA, whose design is motivated by the characteristics of SES problems. Next, it describes how to apply quantum searching to three SES problems: FSM property checking, software test generation, and library-based software synthesis. Next, the paper gives the main ideas in QSAT, a novel toolkit supporting efficient simulation of the algorithms and applications discussed. Finally, it concludes with a substantial simulation-based study of IDGS-FA, showing that it improves both the reliability and speed of other approaches.

Once a system is built, stakeholders are faced with the task of determining the degree to which the system as a whole and major subsystems meet requirements. However, in real-world embedded distributed systems, it can be impossible, impractical, or too costly to gather enough field test data to make these evaluations in a straight-forward manner using traditional system testing alone. Instead, we need a method of verifying requirements compliance that uses the evidence available while minimizing the chances of wrong or misleading conclusions. This paper introduces the novel forensic system verification (FSV) method, which combines modeling, data mining, analytic extrapolation, and goal modeling. It augments human inferences with automated reasoning about requirement satisfaction and confidence propagation. The FSV Method is evaluated on a case study performed using data from a recent medium-scale field trial of a complex distributed embedded system.

Interrupt-driven real time control software is difficult to design and validate. It does not line up well with traditional state-based, timed-transition specification formalisms, due to the complexity of timers and the pending interrupt queue. The present work takes a new approach to the problem of modeling and tool-supported reasoning about such systems based on infinite-state modeling of the temporal event queue. This approach, RTEQ, can be used in any formalism or tool set supporting function rich modeling. The present paper describes the approach, explores its expressive power and semantics, and describes a significant industrial case study applying it to the design of a novel network medium access controller for wireless communications.

Complex, interrupt-driven hard real time control software is difficult to design and validate. It does not line up well with traditional state-based, timed-transition approaches to real time system specification, due to the complexity of timers and the pending interrupt queue. The present work takes a new approach to the problem of modeling and tool-supported reasoning about such systems based on infinite-state modeling of the temporal event queue. This approach, RTEQ, can be used in any formalism or tool set supporting event queue modeling. This paper briefly overviews the approach and its application to a novel wireless medium access controller

No abstract available.

Today's complex computational and embedded systems compute complex quantities from complex inputs, with behavior dependent upon the (distributed) state of the system and its environment. Describing the intended behavior of such a system is challenging. The most natural and commonly used approach is to give a collection of scenarios, where each scenario is a sequence of inputs and expected outputs. An analyst elicits scenarios from subject matter experts (SMEs) to document functional requirements. Scenarios can be represented in a variety of ways, from informal narratives through (formal) linear event sequences. Formal behavior scenarios are useful in many software engineering tasks, including requirements engineering, specification- and architectural-modeling, and test generation. Uses in modeling include model inference, validation, and measuring resource usage and reliability. Finally, scenarios are useful in discovering and documenting gaps in specifications. Existing scenario-based tools and methodologies break down when scenarios grow large. Elicitation becomes impractical, as it requires the human to specify all the steps. Even assuming one can capture thousands or more of input events, it is problematic for the human to describe the correct expected outputs at each point of interest. Finally, even if one can capture all inputs and outputs, the complexity of such an artifact gives one little confidence that it represents desirable behavior in detail, as the risk of undetected errors grows at least linearly with the size. Finally, the behavior of systems described by large scale scenarios typically requires a large and complex set of them, which creates the added difficulty of assuring oneself of covering a "representative" subset of a huge space

Interface descriptions, while adequate for describing relatively simple or uniform functionality, are too abstract to properly describe entities as complex as e-commerce services or feature rich telecommunications services. The web services community has partially acknowledged this, as description languages like WSCL and OWL-S have enriched interface information with additional fragments of component semantics. In this paper, we naturally extend this progression by proposing that services be described by (abstract) executable specification behavioral models instead of, or in addition to, these other descriptive formalisms. Our argument is based on the observation that at least three capabilities, service discovery, validation, and execution monitoring, are enabled or fundamentally improved by this idea. In addition to overviewing OpenModel, our distributed modeling framework, as one possible basis for this approach, we also describe case studies that support our claims, and review the limitations of existing approaches.

Multi-stakeholder distributed systems (MSDS), such as the Internet email and instant messaging systems, and e-business Web service networks, raise new challenges for users, developers, and systems analysts. Traditional requirements engineering, validation, and debugging approaches cannot handle two primary problems of MSDS: the lack of consistent high level requirements and the ignorance problem caused by lack of communication among stakeholders. OpenModel described by R. Hall (2002) addresses this ignorance problem: each MSDS node publishes a behavioral model of itself so that remote stakeholders can reason about their interactions with it. However, stakeholders will typically wish to hold back private state information, such as user identities and cryptographic keys. An OpenModel-based validation tool must tolerate missing information and yet still give useful analyses where possible. These paper overviews OMV, a novel approach to validation in the face of partial information based upon symbolic simulation of OpenModel models. We briefly illustrate our studies of the OMV tool in the domains of email and instant messaging.

A primary goal of program performance understanding tools is to focus the user's attention directly on optimization opportunities where significant cost savings may be found. Optimization opportunities fall into (at least) three broad categories: the call context of a general component may obviate the need for some of its generality; cross-cutting program aspects may be implemented suboptimally for the particular context of use; and thread dependencies may cause unintended delays. This paper enhances prior work in call path profiling in several ways. First, it provides two different call path oriented views on program performance, a server view and a thread view. The former helps one optimize for throughput, while the latter is useful for optimizing thread latency. The views incorporate a typed time notation for representing different program activities, such as monitor wait and thread preemption times. Second, the new framework allows aspect-oriented program profiling, even when the original program was not designed in an aspect oriented fashion. Finally, the approach is implemented in a tool, CPPROFJ, an aspect-capable call path profiler for Java. It exploits recent developments in the Java APIs to achieve accurate and portable sampling-based profiling. Three case studies illustrate its use.

A high-bandwidth, always-on Internet connection makes computers in homes and small offices attractive targets for network-based attacks. Network security gateways can protect such vulnerable hosts from attackers, but differing sets of customer needs require different feature mixes. The safest way to address this market is to provide a family of products, each member of which requires little or no end-user configuration. Since the products are closely related, the effort to validate n of them should be much less than n times the effort to validate one; however validating the correctness and security of even one such device is notoriously difficult, due to the oft-observed fact that no practical amount of testing can show the absence of security flaws. One would instead like to prove security properties, even when the products are implemented using off-the-shelf technologies that don't lend themselves to formal reasoning. The author describes how the specification modeling and validation tools of the Interactive Specification Acquisition Tools (ISAT) suite are used to help validate members of a particular family of network security gateway products built using widely available open source technologies.

A network security gateway protects the computers of a home or small office from Internet-based attacks by remote adversaries. It allows all the protected machines to share a single connection to the Internet and may allow secure access, via a VPN tunnel, into a remote corporate network. It may provide other services as well. In this presentation, I will demonstrate how I use executable specification modeling and lightweight formal methods tools to help discover, validate, and refine requirements models. This process iteratively constructs a formal, executable model of (an abstraction of) the implementation and validates behaviors and properties, while suggesting experiments to perform on the implementation to reduce ignorance. The tool suite used is the Interactive Specification Acquisition Tools (ISAT) reactive system design suite.

A software product typically goes through many "upgrades" (version changes) over its lifetime. Reactive systems, such as e-mail clients, software agents, proxies, traffic controllers, and telephone switches are no exception. Evolving such stateful systems is made difficult by the fact that new versions of the software must deal correctly with legacy instances. Users of earlier versions have invested significant resources in creating the state of the legacy instance, and usually require that this state be upgraded appropriately when the new system version is activated. However, validating the correctness of this upgrading behavior is particularly difficult, whether through testing or more formal techniques like model checking, because legacy states are typically unreachable to the new version of the software. This paper explores this problem and requirements for its solution; presents a simple conceptual and modeling/programming upgrade framework, based upon the idea of a supermodel that allows upgrade behavior to be validated using mainstream approaches; and gives techniques for simplifying the validation problem.

Reactive systems control many useful and complex real-world devices. Tool-supported specification modelling helps software engineers design such systems correctly. One such tool is a scenario generator, which constructs an input event sequence for the spec model that reaches a state satisfying given criteria. It can uncover counterexamples to desired safety properties, explain feature interactions in concrete terms to requirements analysts, and even provide online help to end users learning how to use a system. However, while exhaustive search algorithms work in limited domains, the problem is highly intractable for the functionally rich models that correspond naturally to complex systems engineers wish to design. This paper describes a novel heuristic approach to the problem that is applicable to a large class of infinite state reactive systems. The key idea is to piece together scenarios that achieve subgoals into a single scenario achieving the conjunction of the subgoals. The scenarios are mined from a library captured independently during requirements acquisition. Explanation-based generalization then abstracts them so they may be coinstantiated and interleaved. The approach is implemented, and I present the results of applying the tool to tasks arising from a case study of telephony feature interactions.

While a user might be able to confidently validate a generalized fragment by inspection, since calling an off-hook user should result in a busy signal (when the system only has one line per user), more complex behavior can be impractical to validate by inspection. This is particularly true when the fragment describes an intermediate protocol step, for example, because correctness is often stated in terms of all possible protocol outcomes. The paper illustrates this problem with a fragment describing a step in the CS-NC protocol used by the personal channel agent (PCA), the paper's primary case study. An example correctness property proved in the paper is Property V: given two properly initialized PCAs, CS-NC correctly transmits the new channel from one to the other, and an eavesdropper's action(s) will be detected by at least one of the PCAs, assuming (1) every protocol message sent is eventually received, and (2) only an eavesdropper can discover keys or channel identifiers (with significant probability).

Focused informationalelectronic mail lists, where end users as well as help staff members read and respond to messages, enable the users of a product or service to get timely answers to questions, while requiring fewer paid staff-hours than customer help desks.However, such lists can be plagued by (a) knowledge loss through user and staff turnover and absences, (b) frequently-asked or RTFM questions, and (c) misdirected administrative messages.This paper describes an approach to building a knowledge-based automated list moderator that partially solves these problems, filtering list traffic so that users with frequently asked or administrative questions can get answers without bothering the rest of the list members.INFO MOD employs an expandable base of question-answering knowledge about the product or service, providing tools to help maintain the knowledge.

In order to effectively optimize complex programs built in a layered or recursive fashion (possibly from reused general components), the programmer has a critical need for performance information connected directly to the design decisions and other optimization opportunities present in the code. Call path refinement profiles are novel tools for guiding the optimization of such programs, that: (1) provide detailed performance information about arbitrarily nested (direct or indirect) function call sequences, and (2) focus the user's attention on performance bottlenecks by limiting and aggregating the information presented. This paper discusses the motivation for such profiles, describes in detail their implementation in the CPPROF profiler, and relates them to previous profilers, showing how most widely available profilers can be expressed simply and efficiently in terms of call path refinements.>

Article Free Access Share on Call path profiling Author: Robert J. Hall View Profile Authors Info & Claims ICSE '92: Proceedings of the 14th international conference on Software engineeringJune 1992 Pages 296–306https://doi.org/10.1145/143062.143147Published:01 June 1992Publication History 35citation516DownloadsMetricsTotal Citations35Total Downloads516Last 12 Months37Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

High-level functional (or behavioral) simulation models are difficult, time-consuming, and expensive to develop. We report on a method for automatically generating the program code for a high-level functional simulation model. The high-level model is produced directly from the program code for the circuit components' functional models and a netlist description of their connectivity. A prototype has been implemented in LISP for the SIMMER functional simulator.