This paper demonstrates that composition and refinement techniques are a promising solution for performing rigorous, security architecture trade-off analysis. Such analysis typically occurs in one of two forms: comparing two architectures for implementation and determining the impact of change to an implemented architecture. Composition and refinement techniques reduce the overhead of such analysis significantly over traditional formal methods by facilitating specification and proof reuse and by providing powerful reasoning tools. In this paper, we propose an approach for applying composition and refinement techniques to trade-off analysis. Our approach relies on a formal composition and refinement framework, which is not described here. We describe the approach and apply it to a simple example. We conclude with lessons learned and future work.

This paper argues that Napoleon, a flexible, role-based access control (RBAC) modeling environment, is also a practical solution for enforcing business process control,or workflow, policies. Napoleon provides two important benefits for workflow: simplified policy management and support for heterogeneous, distributed systems. We discuss our strategy for modeling workflow in Napoleon, and we present an architecture that incorporates Napoleon into a workflow management system.

Complex systems must be analyzed in smaller pieces.Analysis must support both bottom-up (composition) and top-down (refinement) development, and it must support the consideration of several critical properties, e.g., functional correctness, fault tolerance and security, as appropriate. We describe a mathematical framework for performing com-position and refinement analysis and discuss some lessons learned from its application. The framework is written and verified in PVS.

Linear hybrid automata are finite state automata augmented with real-valued variables. Transitions between discrete states may be conditional on the values of these variables and may assign new values to variables. These variables can be used to model real time and accumulated task compute time as well as program variables. Although it is possible to encode preemptive fixed priority scheduling using existing linear hybrid automata models, we found it more general and efficient to extend the model slightly to include resource allocation and scheduling semantics.
Under reasonable pragmatic restrictions for this problem domain, the reachability problem is decidable. The proof of this establishes an equivalence between dense time and discrete time models given these restrictions. We next developed a new reachability algorithm that significantly increased the size of problem we could analyze, based on benchmarking exercises we carried out using randomly generated real-time uniprocessor workloads.

Finally, we assessed the practical applicability of these new methods by generating and analyzing hybrid automata models for the core scheduling modules of an existing real-time executive. This exercise demonstrated the applicability of the technology to real-world problems, detecting several errors in the executive code in the process. We discuss some of the strengths and limitations of these methods and possible future developments that might address some of the limitations.

Methods for modeling real-time periodic and aperiodic task scheduling and message passing within multitask systems. The methods utilize undelayed and single sample delayed message connections among software task objects and hardware objects. Task priorities are assigned inversely with period or deadline, so that tasks with shorter periods or deadlines have higher scheduling priorities. Periods of high-criticality tasks are decomposed into smaller pieces that are sequentially dispatched at higher rates where the initial assignment of priority is inconsistent with task criticality. The methods provide for deterministic communication among periodic processes.

This paper discusses a model-based architectural approach for improving predictability of performance in embedded real-time systems. This approach utilizes automated analysis of task and communication architectures to provide insight into schedulability and reliability during design. Automatic generation of a runtime executive that performs task dispatching and inter-task communication eliminates manual coding errors and results in a system that satisfies the specified execution behavior. The MetaH language and toolset supports this model-based approach. MetaH has been used by the U.S. Army in a pilot project applied to missile guidance systems. Reduced time and cost benefits that have been observed will be discussed as a case study.
The paper closes by outlining the current state of commercial availability of such technology and efforts to develop standards, such as those put forth by the Society of Automotive Engineers (SAE); Avionics Systems Division (ASD); working group on Avionics Architecture Description Language (AADL); and the Object Management Group (OMG) Unified Modeling Language (UML) working group on real-time and performance
support in UML.

US Patent Number 6,188,753
A method and apparatus for detection and prevention of calling card fraud is disclosed. The invention provides enhanced intelligence and efficiency in part applying by a fraud analysis associated with a calling card bill type or service provider as identified by originating partitions in network switches. Additionally, the invention incorporates a case-subcase arrangement of fraud analysis information and conducts fraud analysis on a case-by-case basis, thereby providing streamlined handling of suspected fraud. Still additionally, the invention includes an administrative monitor that continuously collects and reviews fraud system status information to detect abnormalities in the system.

This abstract discusses a model-based architectural approach for improving predictability of performance in embedded real-time systems. This approach utilizes automated analysis of task and communication architectures to provide insight into schedulability and reliability during design. Automatic generation of a runtime executive that performs task dispatching and inter-task communication eliminates manual coding errors and results in a system that satisfies the specified execution behavior. The MetaH language and toolset supports this model-based approach. MetaH has been used in a demo projects applied to missile guidance systems and spacecraft attitude control. Reduced time and cost benefits observed will be discussed as a case study.

The distributed firewall is an important new line of network defense. It provides fine-grained access control to augment the protections afforded by the traditional perimeter firewall. To be effective, though, a distributed firewall must satisfy two critical requirements. First, it must embrace a protection model that acknowledges that everything behind the firewall may not be trustworthy. The malicious insider with unobstructed access the network can still mount limited attacks. Second, the firewall must be tamper-resistant. Any firewall that executes on the same untrusted operating system that it is charged to protect begs the question: who is protecting whom? This paper presents a new distributed, embedded firewall that satisfies both requirements. The firewall filters Internet Protocol traffic to and from the host. The firewall is tamper-resistant because it is independent of the host’s operating system. It is implemented on the host’s network interface card and managed by a protected, central policy server located elsewhere on the network. This paper describes the firewall’s architecture and associated assurance claims and discusses unique applications for it.

Planning and scheduling is an important capability for a wide variety of NASA missions, serving either as an enabler without which the mission cannot be done at all, or serving to improve mission operations through making those operations more robust, more predictable, or more efficient.
The objective of this study was to provide input to strategic planning for planning and scheduling research and development within NASA. The rationale for employing an outside agent in this work was precisely to get that outside perspective, with no agenda or axe to grind regarding research priorities. The output of the study is the current report.

This report is intended to serve several purposes:

To provide a taxonomy of planning and scheduling functions relevant to NASA missions.
To provide an analysis of NASA missions currently planned or under study, with regard to the needs of those missions for planning and scheduling, in terms of that taxonomy.
To identify current or planned research and development within NASA or funded by NASA, addressing those identified needs.
To identify remaining unmet needs.