WSC 2003 Final Abstracts

Distributed Simulation with COTS Simulation Packages
Csaba Attila Boer (Erasmus University of Rotterdam) and Alexander Verbraeck (Delft University of Technology)

Abstract:
Connecting COTS (Commercial-off-the-Self) simulation packages entails various difficulties. First of all, commercially available simulation packages hide the access to some internal data that is needed to connect to other simulation models in the distributed simulation study. Next, the data sharing between simulation models is complicated. In order to carry out distributed simulation studies applying COTS simulation packages, we have to exactly define the interfacing and data transfer mechanisms. In this paper we present a theoretical description of different solutions for interfacing and transferring data between various simulation models. These mechanisms have been implemented and tested, and applied in a project in order to prove their practical usage.

Time Management Issues in COTS Distributed Simulation: A Case Study
Simon J.E. Taylor (Brunel University ), Jon Sharpe (Brunel University) and John Ladbrook (Ford Motor Company)

Abstract:
Commercial off-the-shelf (COTS) simulation packages are widely used in industry. Several international groups are currently investigating techniques to integrate distributed simulation facilities in these packages. Through the use of a case study developed with the Ford Motor Company, this paper investigates time management issues in COTS simulation packages. Time management is classified on the basis of the ordering of events that are externally produced to a federate and the ordering of these with events that occur within a COTS simulation package federate. Several approaches to the latter are discussed and one approach is presented as the most effective. Finally the paper presents a bounded buffer problem and proposes the classification of information sharing with respect to the certification of solution.

Synchronization and Management of Shared State in HLA-Based Distributed Simulation
Boon Ping Gan and Malcolm Yoke Hean Low (Singapore Institute of Manufacturing Technology) and Junhu Wei, Xiaoguang Wang, Stephen John Turner, and Wentong Cai (Nanyang Technological University)

Abstract:
The HLA Runtime Infrastructure can support a conservative simulation protocol for its time management service. However, the performance of conservative simulation protocols is very much dependent on lookahead that one can extract out of a simulation model. The most conservative value has to be taken in order to ensure the causality constraint. In this paper, we propose two algorithms, pullRO and pushRO, that allow one to replace some of the timestamp order (TSO) messages (possibly those causing zero lookahead values) with receive order (RO) messages. This removes the time constraint that these messages impose on the lower bound timestamp calculation, which in turn will improve the time advancement rate of federates. The algorithms still ensure the causality constraint and a middleware approach is used to preserve the semantics of the RTI APIs. The performance of the two algorithms is compared against a baseline model where no TSO messages are replaced.

Causal Order based Time Warp: A Tradeoff of Optimism
Yi Zeng, Wentong Cai, and Stephen J. Turner (Nanyang Technological University)

Abstract:
The optimistic synchronization paradigm, Time Warp, allows logical processes to advance aggressively. In the circumstances where the violation of the local causality constraint (LCC) is prone to occurring, this optimism may introduce substantial rollbacks and, as a consequence, significant overhead in recovering from erroneous computations. In this paper, a new approach, COBTW, is proposed, where the happen before relation is employed to capture the potential violations of LCC and causal order is applied to regulate the advancement of logical processes. Due to the difference between causal order and time-stamp order, there are discrepancies between them. Solutions to remove the discrepancies are proposed. Experiments conducted in a cluster and an emulated WAN suggest that COBTW reduces rollbacks caused by violations of LCC and empirically results in better performance, in comparison with the Time Warp protocol.

An Algorithm for Fully-Reversible Optimistic Parallel Simulation
Michael D. Peters and Christopher D. Carothers (Rensselaer Polytechnic Institute)

Abstract:
Typically, large-scale optimistic parallel simulations will spend 90% or more of the total execution time forward processing events and very little time executing rollbacks. In fact, it was recently shown that a large-scale TCP model consisting of over 1 million nodes will execute without generating any rollbacks (i.e., perfect optimistic execution is achieved). The major cost involved in forward execution is the preparation for a rollback in the form of state-saving. Using a technique called "reverse computation", state-saving overheads can be greatly reduced. Here, the rollback operation is realized by executing previously processed events in reverse. However, events are retained until GVT sweeps past. In this paper, we define a new algorithm for realizing a continuum of reverse computation-based parallel simulation systems, which enables us to relax the computing of GVT and potentially further reduces the amount of memory required to execute an optimistic simulation.

SyncSim: A Synchronous Simple Optimistic Simulation Technique based on a Global Parallel Heap Event Queue
Sushil K. Prasad and Zhiyong Cao (Georgia State University)

Abstract:
We developed and implemented two highly optimized optimistic discrete event simulation techniques based on an efficient and scalable Parallel Heap data structure as a global event queue. The primary results are (i) the design of an optimistic simulation algorithm, namely SyncSim, which does not rely on traditional state and message saving data structures, but employs only one backup state per state variable, (ii) a demonstration, through implementation of SyncSim, of an optimistic technique which overcomes the two main mutually conflicting and unbounded overheads of the existing optimistic simulation algorithms: SyncSim bounds the additional space requirements to just one copy per state variable and drastically limits the number of rollbacks encountered. Furthermore, SyncSim beats the highly optimized traditional simulator simglobal on a wide variety of large networks on an Origin-2000 computer. The algorithm SyncSim could form a basis for a good parallelizing engine attachable relatively easily to an existing serial simulator.

HLA-CSPIF Panel on Commercial Off-the-Shelf Distributed Simulation
Simon J.E. Taylor (Brunel University), Boon Ping Gan (Singapore Institute of Manufacturing Technology), Steffen Straßburger (Fraunhofer Inst. for Factory Operation & Automation) and Alexander Verbraeck (Technical University Delft)

Abstract:
Commercial-off-the-shelf (COTS) simulation packages are widely used in many areas of industry. Several research groups are attempting to integrate distributed simulation principles and techniques with these packages to potentially give us COTS distributed simulation. The High Level Architecture – COTS Simulation Package Interoperation Forum (HLA-CSPIF) is a group of researchers and practitioners that are studying methodological and technological issues in this area. This panel paper presents the views of four members of this forum on the technical problems that must be overcome for this emerging field to be realized.

From Simulation to Verification (and Back)
Harald Rueß and Leonardo de Moura (SRI International)

Abstract:
Symbolic evaluation is the execution of software and software designs on inputs given as symbolic or explicit constants along with constraints on these inputs. Efficient symbolic evaluation is now feasible due to recent advances in efficient decision procedures and symbolic model checking. Symbolic evaluation can be applied to partially implemented descriptions and provides wider coverage and greater assurance than testing and traditional simulation alone. Unlike full formal verification, symbolic evaluation can be used in a partial manner that is more likely to succeed and yield some degree of assurance. Its main advantage is that it can be used within a smooth spectrum of analyses ranging from refutation based on explicit-state simulation to full-blown verification.

Design Environments for Complex Systems
Corrado Priami (University of Trento)

Abstract:
The paper describes an approach for modeling complex systems by hiding as much formal details as possible from the user, still allowing verification and simulation of the model. The interface is based on UML to make the environment available to the largest audience. To carry out analysis, verification and simulation we automatically extract process algebras specifications from UML models. The results of the analysis is then reflected back in the UML model by annotating diagrams. The formal model includes stochastic information to handle quantitative parameters. We present here the stochastic pi-calculus and we discuss the implementation of its probabilistic support that allows simulation of processes. We exploit the benefits of our approach in two applicative domains: global computing and systems biology.

Formal Analysis of Air Traffic Management Systems: The Case of Conflict Resolution and Recovery
Ricky Butler (National Aeronautics & Space Administration), Jeffrey Maddalon (NASA) and Alfons Geser and César Muñoz (National Institute of Aerospace)

Abstract:
New air traffic management concepts distribute the responsibility for traffic separation among the several actors of the aerospace system. As a consequence, these concepts move the safety risk from human controllers to the on-board software and hardware systems. One example of the new kind of distributed systems is air traffic conflict detection and resolution. Traditional methods for safety analysis such as human-in-the-loop simulations, testing, and flight experiments may not be sufficient in this highly distributed system: the set of possible scenarios is too large to have a reasonable coverage. This paper proposes a paradigm shift for the safety analysis of avionics systems where formal methods drive the development of critical systems. As a case study of this approach, we report the mechanical verification of an algorithm for air traffic conflict resolution and recovery.

Event-Triggered Environments for Verification of Real-Time Systems
Darren Cofer (Honeywell Laboratories) and Murali Rangarajan (Honeywell)

Abstract:
The growing complexity and the safety-critical requirements of the embedded software in avionics systems present many challenges to current test-based verification technology. The use of formal verification methods can increase design assurance by exploring a larger range of system behaviors and fault conditions than can feasibly be covered by testing or simulation. However, one of the most challenging tasks faced in any formal verification activity is the construction of an adequate model for the environment with which the analyzed system interacts. For real-time systems where the timing characteristics are critical to correct performance this task is even more difficult. In this paper we discuss how an event-triggered model of time (as found in discrete event simulations) can be used as the basis for the environment needed to verify real-time avionics software.

From Timed Automata to DEVS Models
Norbert Giambiasi, Jean-Luc Paillet, and Frédéric Châne (Université Aix-Marseille III)

Abstract:
In this paper, we present the formal transformation of Timed Input/Output Automata into simulation models, expressed in the DEVS formalism. This transformation takes place in an approach of a validation of high-level specifications by simulation. The validation is based on the simulation of a coupled model built with the system to be controlled and the control specifications. An example of this approach is given in the paper.

Simulating Quantum Computing: Quantum eXpress
Kareem S. Aggour (GE Global Research), Michael J. Simon (Lockheed Martin Space Systems Company) and Renee Guhde and Melvin K. Simmons (GE Global Research)

Abstract:
Quantum Computing (QC) research has gained a lot of momentum recently due to several theoretical analyses that indicate that QC is significantly more efficient at solving certain classes of problems than classical computing. While experimental validation will ultimately be required, the primitive nature of current QC hardware leaves practical testing limited to trivial examples. Thus, a robust simulator is needed to study complex QC issues. Most QC simulators model ideal operations, and thus cannot predict the actual time required to execute an algorithm or quantify the effects of errors in the calculation. We have developed a novel QC simulator that models physical hardware implementations. This simulator not only allows the accurate simulation of quantum algorithms on various hardware implementations, but also takes an important step towards providing a framework to determine their true performance and vulnerability to errors.