Browsing by Author "Stewart, Danielle"
Now showing 1 - 6 of 6
- Results Per Page
- Sort Options
Item Architecture Modeling and Analysis for Safety Engineering(Springer, 2017) Stewart, Danielle; Whalen, Michael; Cofer, Darren; Heimdahl, MatsArchitecture description languages such as AADL allow systems engineers to specify the structure of system architectures and perform several analyses over them, including schedulability, resource analysis, and information flow. In addition, they permit system-level requirements to be specified and analyzed early in the development process of airborne and ground-based systems. These tools can also be used to perform safety analysis based on the system architecture and initial functional decomposition. Using AADL-based system architecture modeling and analysis tools as an exemplar, we extend existing analysis methods to support system safety objectives of ARP4754A and ARP4761. This includes extensions to existing modeling languages to better describe failure conditions, interactions, and mitigations, and improvements to compositional reasoning approaches focused on the specific needs of system safety analysis. We develop example systems based on the Wheel Braking System in SAE AIR6110 to evaluate the effectiveness and practicality of our approach.Item Compositional Behavioral Fault Analysis(2021-02) Stewart, DanielleModel-based development tools are increasingly being used for system-level development of safety-critical systems. Architectural and behavioral models provide important information that can be leveraged to improve the system safety analysis process. Model-based design artifacts produced in early stage development activities can be used to perform system safety analysis, reducing costs and providing accurate results throughout the system life-cycle. Safety analysis is used to ensure that critical systems operate within some level of safety when failures are present. As critical systems become more dependent on software components, it becomes more challenging for safety analysts to comprehensively enumerate all possible failure causation paths. Any automated analyses should be sound to sufficiently prove that the system operates within the designated level of safety. This paper presents a compositional approach to the generation of fault forests (sets of fault trees) and minimal cut sets. We use a behavioral fault model to explore how errors may lead to a failure condition. The analysis is performed per layer of the architecture and the results are automatically composed. A complete formalization is given. We implement this by leveraging minimal inductive validity cores produced by an infinite state model checker. This research provides a sound alternative to a monolithic framework. This enables safety analysts to get a comprehensive enumeration of all applicable fault combinations using a compositional approach while generating artifacts required for certification.Item Even Harmonious Labelings of Disconnected Graphs(2015-05) Stewart, DanielleA graph $G$ with $q$ edges is called \textit{graceful} if there is an injection from the vertices of $G$ to the set $\{0,1,\ldots,q\}$ such that when each edge $xy$ is assigned the label $|f(x)-f(y)|$, the resulting edge labels are distinct. This notion as well as a number of other functions from a graph to a set of non-negative integers were studied as tools for decomposing the complete graph into isomorphic subgraphs. A graph $G$ with $q$ edges is said to be harmonious if there is an injection $f$ from the vertices of $G$ to the group of integers modulo $q$ such that when each edge $xy$ is assigned the label $f(x)+f(y)$ $($mod $q)$, the resulting edge labels are distinct. If $G$ is a tree, exactly one label may be used on two vertices. Over the years, many variations of these two concepts have been studied and hundreds of articles have been written on these topics. We study a variant of harmonious labeling. A function $f$ is said to be an even harmonious labeling of a graph $G$ with $q$ edges if $f$ is an injection from the vertices of $G$ to the integers from $0$ to $2q$ and the induced function $f^*$ from the edges of $G$ to ${0,2,\ldots,2(q-1)}$ defined by $f^*(xy)=f(x)+f(y) ($mod $2q)$ is bijective. Only a few papers have been written on even harmonious labeling. This paper focuses on finding even harmonious labelings for disjoint graphs. Among the families we investigate are: the disjoint union of cycles and stars, unions of cycles with paths, and unions of squares of paths.Item Generation of Pseudoprimes(2012) Stewart, DanielleItem Generation of Pseudoprimes(2014) Stewart, Danielle; Greene, John R.Item Safety Annex for the Architecture Analysis and Design Language(2018-03-09) Stewart, Danielle; Liu, Jing (Janet); Heimdahl, Mats; Cofer, Darren; Peterson, MichaelModel-based development techniques are increasingly being used in the development of critical systems software. Leveraging the artifacts from model based development in the safety analysis process would be highly desirable to provide accurate analysis and enable cost savings. In particular, architectural and behavioral models provide rich information about the system's operation. In this paper we describe an extension to the Architecture Analysis and Design Language (AADL) developed to allow a rich modeling of a system under failure conditions. This emph{Safety Annex} allows the independent modeling of component failure modes and allows safety engineers to weave various types of faults into the nominal system model. The accompanying tool support allows investigation of the propagation of errors from their source to their effect on top level safety properties without the need to add separate propagation specifications; it also supports describing dependent faults that are not captured through the behavioral models, e.g., failures correlated due to the physical structure of the system. We describe the Safety Annex, illustrate its use with a representative example, and discuss and demonstrate the tool support enabling an analyst to investigate the system behavior under failure conditions.