Engineering PapersSearch

Engineering topics

Owens, David

Publications and source records attributed to Owens, David.

Integrated Intermodal Passenger Transportation System

Modern transportation consists of many unique modes of travel. Each of these modes and their respective industries has evolved independently over time, forming a largely incoherent and inefficient overall transportation system. Travelers today are forced to spend unnecessary time and efforts planning a trip through varying modes of travel each with their own scheduling, pricing, and services; causing many travelers to simply rely on their relatively inefficient and expensive personal automobile. This paper presents a demonstration program system to not only collect and format many different sources of trip planning information, but also combine these independent modes of travel in order to form optimal routes and itineraries of travel. The results of this system show a mean decrease in inter-city travel time of 10 percent and a 25 percent reduction in carbon dioxide emissions over personal automobiles. Additionally, a 55 percent reduction in carbon dioxide emissions is observed for intra-city travel. A conclusion is that current resources are available, if somewhat hidden, to drastically improve point to point transportation in terms of time spent traveling, the cost of travel, and the ecological impact of a trip. Finally, future concepts are considered which could dramatically improve the interoperability and efficiency of the transportation infrastructure.

Klock, Ryan

SPIN or LURCH : a Comparative Assessment of Model Checking and Stochastic Search for Temporal Properties in Procedural Code

The difficulty of how to test large systems, such as the one on board a NASA robotic remote explorer (RRE) vehicle, is fundamentally a search issue: the global state space representing all possible has yet to be solved, even after many decades of work. Randomized algorithms have been known to outperform their deterministic counterparts for search problems representing a wide range of applications. In the case study presented here, the LURCH randomized algorithm proved to be adequate to the task of testing a NASA RRE vehicle. LURCH found all the errors found by an earlier analysis of a more complete method (SPIN). Our empirical results are that LURCH can scale to much larger models than standard model checkers like SMV and SPIN. Further, the LURCH analysis was simpler than the SPIN analysis. The simplicity and scalability of LURCH are two compelling reasons for experimenting further with this tool.

verification