Publications

Abstract not provided.

Abstract not provided.

In this paper we present Maestro, a model-based systems engineering (MBSE) environment for design and simulation of complex electronic systems using Orchestra-a simulation tool developed at Sandia National Laboratories. Maestro is deployed as a plugin for MagicDraw and uses Orchestra domain-specific language (DSL) which is based on SysML. Maestro enables a model-based design and analysis approach that replaces the traditional document-based systems engineering process. It provides a unified graphical modeling environment to domain experts who have had to depend on drawing tools for defining system architecture and manual transcription of system topology in creating complex simulation models.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Maturing embeddable real-time concepts into deployable high consequence systems faces numerous challenges. Although overcoming these challenges can be aided by commercially available processes, toolsets, and components, they often fall short of meeting the needs at hand. This paper will review the development of a framework being assembled to address many of the shortcomings while attempting to leverage commercial capabilities as appropriate. © 2007 The authors and IOS Press. All rights reserved.

Abstract not provided.

The SSP is a hardware implementation of a subset of the JVM for use in high consequence embedded applications. In this context, a majority of the activities belonging to class loading, as it is defined in the specification of the JVM, can be performed statically. Static class loading has the net result of dramatically simplifying the design of the SSP as well as increasing its performance. Due to the high consequence nature of its applications, strong evidence must be provided that all aspects of the SSP have been implemented correctly. This includes the class loader. This article explores the possibility of formally verifying a class loader for the SSP implemented in the strategic programming language TL. Specifically, an implementation of the core activities of an abstract class loader is presented and its verification in ACL2 is considered.

Program transformation is a restricted form of software construction that can be amenable to formal verification. When successful, the nature of the evidence provided by such a verification is considered strong and can constitute a major component of an argument that a high-consequence or safety-critical system meets its dependability requirements. This article explores the application of novel higher-order strategic programming techniques to the development of a portion of a class loader for a restricted implementation of the Java Virtual Machine (JVM). The implementation is called the SSP and is intended for use in high-consequence safety-critical embedded systems. Verification of the strategic program using ACL2 is also discussed.

In many strategic systems, the choice combinator provides a powerful mechanism for controlling the application of rules and strategies to terms. The ability of the choice combinator to exercise control over rewriting is based on the premise that the success and failure of strategy application can be observed. In this paper we present a higher-order strategic framework with the ability to dynamically construct strategies containing the choice combinator. To this framework, a combinator called hide is introduced that prevents the successful application of a strategy from being observed by the choice combinator. We then explore the impact of this new combinator on a real-world problem involving a restricted implementation of the Java Virtual Machine.

The distributed data problem, is characterized by the desire to bring together semantically related data from syntactically unrelated portions of a term. Two strategic combinators, dynamic and transient, are introduced in the context of a classical strategic programming framework. The impact of the resulting system on instances of the distributed data problem is then explored.

The Sandia Secure Processor (SSP) is a new native Java processor that has been specifically designed for embedded applications. The SSP's design is a system composed of a core Java processor that directly executes Java bytecodes, on-chip intelligent IO modules, and a suite of software tools for simulation and compiling executable binary files. The SSP is unique in that it provides a way to control real-time IO modules for embedded applications. The system software for the SSP is a 'class loader' that takes Java .class files (created with your favorite Java compiler), links them together, and compiles a binary. The complete SSP system provides very powerful functionality with very light hardware requirements with the potential to be used in a wide variety of small-system embedded applications. This paper gives a detail description of the Sandia Secure Processor and its unique features.

Assuring hard real-time characteristics of I/O associated with embedded software is often a difficult task. Input-Output related statements are often intermixed with the computational code, resulting in I/O timing that is dependent on the execution path and computational load. One way to mitigate this problem is through the use of interrupts. However, the non-determinism that is introduced by interrupt driven I/O may be so difficult to analyze that it is prohibited in some high consequence systems. This paper describes a balanced hardware/software solution to obtain consistent interrupt-free I/O timing, and results in software that is much more amenable to analysis.