Addressing off-nominal behaviors in requirements for embedded systems

System requirements are typically specified on the assumption that the system's operating environment will behave in what is considered to be an expected and nominal manner. When gathering requirements, one concern is whether the requirements are too ambiguous to account for every possible, unintended, Off-Nominal Behavior (ONB) that the operating environment can create, which results in an undesired system state. In this dissertation, we present two automated approaches which can expose, within a set of embedded requirements, whether an ONB can result in an undesired system state. Both approaches employ a modeling technique developed as part of this dissertation called the Causal Component Model (CCM).;The first approach described, uses model checking as the means of property checking requirements using temporal logic properties specifically created to oppose ONBs. To facilitate the use of model checking by requirements engineers and non-technical stakeholders who are the system domain experts, a framework for the model checker interface was developed using the CCM. The CCM serves as both a cognitive friendly input and output to the model checker. The second approach extends the CCM into a dedicated ONB property checker, which overcomes the limitations of the model checker, by not only exposing ONBs but also facilitating the correction of those ONBs. We demonstrate how both approaches can expose and help correct potential Off-Nominal Behavior problems using requirements that represent real-world products. Our case studies show that both approaches can expose a system's susceptibility to ONBs and provide enough information to correct the potential problems that can be caused by those ONBs.