Browsing by Subject "Computer software--Development"
Now showing 1 - 5 of 5
Results Per Page
Sort Options
Item Artifact-based functional comparison of software processes(2004) Podorozhny, Rodion Mikhailovich; Perry, Dewayne E.Item Hybrid domain representation archive (HyDRA) : viewpoint-oriented requirements analysis(2000-08) Jernigan, Stephan Russell; Barber, K. SuzanneThe creation of a requirements model (explicitly representing functional, data, and timing requirements) typically involves accommodating viewpoints from multiple system stakeholders (e.g. multiple end-users and system maintainers). Viewpoint-oriented requirements analysis methods have been proposed by other researchers to ensure the capture of requirements imposed by all user perspectives. However, domain-modeling methodologies and CASE tools poorly address how to construct a single model given input from a variety of sources and how to maintain traceability through the synthesis process. Rather than making incremental changes to a single requirements model in response to new information, this work suggests the creation of independent models to capture the input from each viewpoint. This research provides a semi-automated method of resolving the differences between viewpoints and producing a single, traceable requirements model that embodies the merged viewpoints. Computer assistance includes the detection of consistency and completeness conflicts, the enactment of conflict resolutions, the maintenance of traceability information, and the gathering of statistics regarding the content and resolution of viewpoints. This data can provide previously unavailable insight into the progress of the requirements acquisition process and characteristics of the domain. A case study is presented to demonstrate the method and the usefulness of gathered data to software engineers and software development managers.Item Integration of model checking into software development processes(2004) Xie, Fei; Browne, James C.Testing has been the dominant method for validation of software systems. As software systems become complex, conventional testing methods have become inadequate. Model checking is a powerful formal verification method. It supports systematic exploration of all states or execution paths of the system being verified. There are two major challenges in practical and scalable application of model checking to software systems: (1) the applicability of model checking to software systems and (2) the intrinsic complexity of model checking. In this dissertation, we have developed a comprehensive approach to integration of model checking into two emerging software development processes: ModelDriven Development (MDD) and Component-Based Development (CBD), and a combination of MDD and CBD. This approach addresses the two major challenges under the following framework: (1) bridging applicability gaps through automatic translation of software representations to directly model-checkable formal representations, (2) seamless integration of state space reduction algorithms in the translation through static analysis, and (3) scaling model checking capability and achieving state space reduction by systematically exploring compositional structures of software systems. We have integrated model checking into MDD by applying mature model checking techniques to industrial design-level software representations through automatic translation of these representations to the input formal representations of model checkers. We have developed a translation-based approach to compositional reasoning of software systems, which simplifies the proof, implementation, and application of compositional reasoning rules at the software system level by reusing the proof and implementation of existing compositional reasoning rules for directly model-checkable formal representations. We have developed an integrated state space reduction framework which systematically conducts a top-down decomposition of a large and complex software system into directly model-checkable components by exploring domain-specific knowledge. We have designed, implemented, and applied a bottom-up approach to model checking of component-based software systems, which composes verified systems from verified components and integrates model checking into CBD. We have further scaled model checking of componentbased systems by exploring the synergy between MDD and CBD, i.e., specifying components in executable design languages, and realizing the bottom-up approach based on model checking of software designs through translation.Item Language and compiler support for mixin programming(2002-05) Cardone, Richard Joseph; Lin, Yun CalvinItem Program analysis with boolean logic solvers(2007-12) Zaraket, Fadi A., 1974-; Aziz, AdnanModern computation systems are very complex. As a result they are very challenging to reason about and validate. Validation techniques based on dynamic analysis—testing— are time consuming and offer no guarantees of correctness. Researchers have proposed static verification techniques which require no testing and are complete. Existing static verification techniques that are based on satisfiability of Boolean formulas in conjunctive normal form validate designs by forcing bounds on the range of variables of a design. Their primary drawback is that they are limited to designs of relatively low complexity. They translate a design expressed in an imperative or a declarative high-level description language to a Boolean formula. There are three limiting aspects of translating high-level designs to conjunctive normal form. (1.) A small increase in the bound on variable ranges can cause a large increase in the size of the translated formula. For example, for an undirected seven-node tree the translation produced one million variables and five million clauses. (2.) Boolean satisfiability solvers are restricted to using optimizations that apply at the level of conjunctive normal form formulas. Finally, (3.) the Boolean formulas often need to be regenerated with higher bounds to ensure the correctness of the translation. This dissertation proposes the use of sequential circuits, Boolean formulas with memory elements and hierarchical structures, and sequential circuit solvers to validate highlevel designs. (1.) Sequential circuits are much more succinct than the pure combinational conjunctive normal form formulas and preserve the high-level structure of the design. (2.) Encoding the problem as a sequential circuit enables the use of a number of powerful automated analysis techniques that have no counterparts for conjunctive normal form formulas. This dissertation applies sequential analysis to both declarative and imperative designs. The results show that it can validate designs with bounds that are orders of magnitude larger than those achievable by the state of the art techniques based on conjunctive normal form analysis.