Skip to main content

Horizontal Menu

  • Research
    • Areas
    • Projects
    • Publications
  • Education
    • Grad Student Info
    • Internship Program
  • Team
  • Sponsors
  • Contact
  • Opportunities

Hamburger Menu

  • Home
  • ISIS Calendar
    • Research Projects
    • Research Areas
    • Publications
    • Grad Student Info
    • Internship Program
  • Team
  • Sponsors
  • Contact
  • Opportunities

Breadcrumb

  • Home /
  • Publications
Search by title, author, keywords, etc.

2011

publication

Rapid Property Specification and Checking for Model-Based Formalisms

In model-based development, verification techniques can be used to check whether an abstract model satisfies a set of properties. Ideally, implementation code generated from these models can also be verified against similar properties. However, the distance between the property specification languages and the implementation makes verifying such generated code difficult. Optimizations and renamings can blur the correspondence between the two, further increasing the difficulty of specifying verification properties on the generated code. This paper describes methods for specifying verification properties on abstract models that are then checked on implementation level code. These properties are translated by an extended code generator into implementation code and special annotations that are used by a software model checker.
Authored by Daniel Balasubramanian, Gabor Pap, Harmon Nine, Gabor Karsai, Michael Lowry, Corina Pasareanu, and Tom Pressburger
publication

Transmission Control Policy Design for Decentralized Detection in Sensor Networks

Authored by Ashraf Tantawy, Xenofon Koutsoukos, and Gautam Biswas
publication

Rectifying Orphan Components using Group-Failover in Distributed Real-time and Embedded Systems

Authored by Sumant Tambe and Aniruddha Gokhale
publication

Predictable deployment in component-based enterprise distributed real-time and embedded systems

Component-based middleware, such as the Lightweight CORBA Component Model, are increasingly used to implement large-scale distributed real-time and embedded (DRE) systems. In addition to supporting the quality of service (QoS) requirements of individual DRE systems, component technologies must also support bounded latencies when effecting deployment changes to DRE systems in response to changing environmental conditions and operational requirements. This paper makes three contributions to the study of predictable deployment latencies in DRE systems. First, we describe OMG's Deployment and Configuration (D\&C) specification for component-based systems and discuss how conventional implementations of this standard can significantly degrade deployment latencies. Second, we describe architectural changes and performance optimizations implemented within the Locality-Enhanced Deployment and Configuration Engine (LE-DAnCE) implementation of the D\&C specification. Finally, we analyze the performance of LE-DAnCE in the context of component deployments on 10 nodes for a representative DRE system consisting of 1,000 components. Our results show LE-DAnCE's optimizations provide a bounded deployment latency of less than 2 seconds with 4 percent jitter.
Authored by William Otte, Aniruddha Gokhale, and Douglas Schmidt
publication

PaNeCS: A Modeling Language for Passivity-based Design of Networked Control Systems

The rapidly increasing use of information technology in constructing real-world systems has led to the urgent need for a sound systematic approach in designing networked control systems. Communication delays and other uncertainties complicate the development and analysis of these systems. This paper describes a prototype modeling language for the design of networked control systems using passivity to decouple the control design from network uncertainties. The modeling language includes an integrated analysis tool to check for passivity and code generators for simulation in MATLAB/Simulink using the TrueTime platform modeling toolbox and for running actual experiments. The resulting designs are by construction robust to platform effects and implementation uncertainties.
Authored by Emeka Eyisi, Joseph Porter, Nicholas Kottenstette, Xenofon Koutsoukos, and Janos Sztipanovits
publication

Managing the Quality of Software Product Line Architectures through Reusable Model Transformations

Authored by Amogh Kavimandan, Aniruddha Gokhale, Gabor Karsai, and Jeff Gray
publication

Using Tree Augmented Naive Bayes Classifiers to Improve Engine Fault Models

Authored by Daniel Mack, Gautam Biswas, Xenofon Koutsoukos, and Dinkar Mylaraswamy
publication

Transmission Control Policy Design for Decentralized Detection in Tree Topology Sensor Networks

Authored by Ashraf Tantawy, Xenofon Koutsoukos, and Gautam Biswas
publication

Towards a Generic Cloud-based Modeling Environment

This paper is aimed at presenting a concept of a flexible diagramming framework for building engineering and educational applications. The framework was designed to serve as a platform for online services and collaborative environments where users typically work on remotely stored, shared data through a browser-based user interface. The paper summarizes the common requirements towards such services, overviews related approaches and gives insights into some design challenges through the analysis of use-cases. The design problem is examined from a user-centered view: the key motivation of our research is to find innovative, possibly device-independent solutions that enable seamless user experiences. Finally a generic framework based on a HTML-JavaScript library is proposed, which could be employed for implementing wide range of software solutions from e-learning to cloud-based modeling environments.
Authored by Laszlo Juracz and Larry Howard
publication

Software-defined radio for versatile low-power wireless sensor systems

Traditional wireless sensor network architectures are based on low-power microcontrollers and highly integrated short range radio transceiver chips operating in one of the few ISM bands. This combination provides a convenient and proven approach to design and build inexpensive sensor nodes rapidly. However, the black box nature of these radio chips severely limit experimentation and research with novel and innovative technologies in the wireless infrastructure. Our team previously proposed a revolutionary architecture for wireless nodes based on Flash FPGA devices. This paper shows the rst results of our work through the implementation and evaluation of a simple baseband FSK modem in the SmartFusion FPGA fabric. We also demonstrate how we could leverage existing software radio projects to use the baseband modem in a wide range of radio frequency bands.
Authored by Sandor Szilvasi, Benjamin Babjak, Akos Ledeczi, and Peter Volgyesi
publication

Polyglot: Modeling and Analysis for Multiple Statechart Formalisms

In large programs such as NASA Exploration, multiple systems that interact via safety-critical protocols are already designed with different Statechart variants. To verify these safety-critical systems, a unified framework is needed based on a formal semantics that captures the variants of Statecharts. We describe Polyglot, a unified framework for the analysis of models described using multiple Statechart formalisms. In this framework, Statechart models are translated into Java and analyzed using pluggable semantics for different variants operating in a polymorphic execution environment. The framework has been built on the basis of a parametric formal semantics that captures the common core of Statecharts with extensions for different variants, and addresses previous limitations. Polyglot has been integrated with the Java Jathfinder verification tool-set, providing analysis and test-case generation capabilities. We describe the application of this unified framework to the analysis of NASA/JPL's MER Arbiter whose interacting components were modeled using multiple Statechart formalisms.
Authored by Daniel Balasubramanian, Corina Pasareanu, Michael Whalen, Gabor Karsai, and Michael Lowry
publication

Fusing Distributed Muzzle Blast and Shockwave Detections

The paper presents a novel sensor fusion technique to shooter localization using a wireless network of single-channel acoustic sensors. The unique challenge is that the number of available sensors is very limited. The first contribution of the work is an approach to estimate the miss distance of the shot and the range to the shooter from a single shot using a single sensor. The second contribution is the novel sensor fusion algorithm itself that fuses the miss distance and range estimates of the individual nodes as well as their Time of Arrival observations of the shockwave and the muzzle blast. The performance of both the single sensor method and the network fusion are very promising.
Authored by Janos Sallai, Peter Volgyesi, Ken Pence, and Akos Ledeczi
publication

Efficient Autoscaling in the Cloud using Predictive Models for Workload Forecasting

Authored by Nilabja Roy, Abhishek Dubey, and Aniruddha Gokhale
publication

Prognostic Modeling and Experimental Techniques for Electrolytic Capacitor Health Monitoring

Authored by Chetan Kulkarni, Gautam Biswas, Celaya Jose, and Goebel Kai
publication

Efficiently and transparently automating scalable on-demand activation and deactivation of services with the activator pattern

Authored by Michael Stal, Douglas Schmidt, and William Otte
publication

RFDMon: A Real-Time and Fault-Tolerant Distributed System Monitoring Approach

Authored by Rajat Mehrotra, Abhishek Dubey, Jim Kwalkowski, Marc Paterno, Amitoj Singh, Randolph Herber, and Sherif Abdelwahed
publication

Reasoning about Metamodeling with Formal Specifications and Automatic Proofs

Metamodeling is foundational to many modeling frameworks, and so it is important to formalize and reason about it. Ideally, correctness proofs and test-case generation on the metamodeling framework should be automatic. However, it has yet to be shown that extensive automated reasoning on metamodeling frameworks can be achieved. In this paper we present one approach to this problem: Metamodeling frameworks are specified modularly using algebraic data types and constraint logic programming (CLP). Proofs and test-case generation are encoded as CLP satisfiability problems and automatically solved.
Authored by Ethan Jackson, Tihamer Levendovszky, and Daniel Balasubramanian
publication

Prognostics Health Management and Failure Analysis Modeling techniques for Accelerated Life testing in Electrolytic Capacitors

Authored by Chetan Kulkarni, Gautam Biswas, Celaya Jose, and Goebel Kai
publication

A Model-based Prognostics Methodology for Electrolytic Capacitors Based on Electrical Overstress Accelerated Aging

Authored by Celaya Jose, Chetan Kulkarni, Gautam Biswas, Saha Sankalita, and Goebel Kai
publication

Deriving Bayesian Classifiers from Flight Data to Enhance Aircraft Diagnosis Models

Authored by Daniel Mack, Gautam Biswas, Xenofon Koutsoukos, Dinkar Mylaraswamy, and George Hadden
publication

Weapon Classification and Shooter Localization Using Distributed Multichannel Acoustic Sensors

Authored by Janos Sallai, Will Hedgecock, Peter Volgyesi, Andras Nadas, Gyorgy Balogh, and Akos Ledeczi
publication

Infrastructure for component-based DDS application development

Enterprise distributed real-time and embedded (DRE) systems are increasingly being developed with the use of component-based software techniques. Unfortunately, commonly used component middleware platforms provide limited support for event-based publish/subscribe (pub/sub) mechanisms that meet both quality-of-service (QoS) and configurability requirements of DRE systems. On the other hand, although pub/sub technologies, such as OMG Data Distribution Service (DDS), support a wide range of QoS settings, the level of abstraction they provide make it hard to configure them due to the significant source-level configuration that must be hard-coded at compile time or tailored at run-time using proprietary, ad hoc configuration logic. Moreover, developers of applications using native pub/sub technologies must write large amounts of boilerplate ``glue'' code to support run-time configuration of QoS properties, which is tedious and error-prone. This paper describes a novel, generative approach that combines the strengths of QoS-enabled pub/sub middleware with component-based middleware technologies. In particular, this paper describes the design and implementation of DDS4CIAO which addresses a number of inherent and accidental complexities in the DDS4CCM standard. DDS4CIAO simplifies the development, deployment, and configuration of component-based DRE systems that leverage DDS's powerful QoS capabilities by provisioning DDS QoS policy settings and simplifying the development of DDS applications.
Authored by William Otte, Aniruddha Gokhale, Douglas Schmidt, and Johnny Willemsen
publication

Acoustic Shooter Localization with a Minimal Number of Single-Channel Wireless Sensor Nodes

Acoustic shooter localization systems are being rapidly deployed in the field. However, these are standalone systems—either wearable or vehicle-mounted—that do not have networking capability even though the advantages of widely distributed sensing for locating shooters have been demonstrated before. The reason for this is that certain disadvantages of wireless network-based prototypes made them impractical for the military. The system that utilized stationary single-channel sensors required many sensor nodes, while the multi-channel wearable version needed to track the absolute self-orientation of the nodes continuously, a notoriously hard task. This paper presents an approach that overcomes the shortcomings of past approaches. Specifically, the technique requires as few as five single-channel wireless sensors to provide accurate shooter localization and projectile trajectory estimation. Caliber estimation and weapon classification are also supported. In addition, a single node alone can provide reliable miss distance and range estimates based on a single shot as long as a reasonable assumption holds. The main contribution of the work and the focus of this paper is the novel sensor fusion technique that works well with a limited number of observations. The technique is thoroughly evaluated using an extensive shot library.
Authored by Janos Sallai, Akos Ledeczi, and Peter Volgyesi
publication

External smart microphone for mobile phones

Authored by Peter Volgyesi, Sandor Szilvasi, Janos Sallai, and Akos Ledeczi
publication

Scaffolding to Support Learning of Ecology in Simulation Environments

Authored by Satabdi Basu, Gautam Biswas, and Pratim Sengupta

Pagination

  • First page « First
  • Previous page ‹‹
  • …
  • Page 10
  • Page 11
  • Page 12
  • Page 13
  • Current page 14
  • Page 15
  • Page 16
  • Page 17
  • Page 18
  • …
  • Next page ››
  • Last page Last »
Download CSV

Footer Links A

  • About Us
  • Contact
  • LinkedIn

Footer Links B

  • Work at ISIS
  • Internship Program
  • Grad Student Info

1025 16th Avenue South

Nashville, Tennessee 37212

Phone: (615) 343-7472

Email: contact.isis@vanderbilt.edu