Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in 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 …
Evoalloy: An Evolutionary Approach For Analyzing Alloy Specifications, Jianghao Wang
Evoalloy: An Evolutionary Approach For Analyzing Alloy Specifications, Jianghao Wang
Department of Computer Science and Engineering: Dissertations, Theses, and Student Research
Using mathematical notations and logical reasoning, formal methods precisely define a program’s specifications, from which we can instantiate valid instances of a system. With these techniques, we can perform a variety of analysis tasks to verify system dependability and rigorously prove the correctness of system properties. While there exist well-designed automated verification tools including ones considered lightweight, they still lack a strong adoption in practice. The essence of the problem is that when applied to large real world applications, they are not scalable and applicable due to the expense of thorough verification process. In this thesis, I present a new …