Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Computer Engineering
Formal Modeling And Analysis Of A Family Of Surgical Robots, Niloofar Mansoor
Formal Modeling And Analysis Of A Family Of Surgical Robots, Niloofar Mansoor
Department of Computer Science and Engineering: Dissertations, Theses, and Student Research
Safety-critical applications often use dependability cases to validate that specified properties are invariant, or to demonstrate a counterexample showing how that property might be violated. However, most dependability cases are written with a single product in mind. At the same time, software product lines (families of related software products) have been studied with the goal of modeling variability and commonality and building family-based techniques for both modeling and analysis. This thesis presents a novel approach for building an end to end dependability case for a software product line, where a property is formally modeled, a counterexample is found and then …
Variable Bounds Analysis Of A Climate Model Using Software Verification Techniques, Peter Revesz, Robert Woodward
Variable Bounds Analysis Of A Climate Model Using Software Verification Techniques, Peter Revesz, Robert Woodward
CSE Conference and Workshop Papers
Software verification techniques often use some approximation method that identifies the limits of the possible range of values that variables in a computer program can take during execution. Current climate models are complex computer programs that are typically iterated time-step by time-step to predict the next value of the climate-related variables. Because these iterative methods are necessarily computed only for a fixed number of iterations, they are unable to answer many long-range questions that may be posed regarding climate change, for example, whether there are natural fluctuations or whether a tipping point is reached after which there is no return …