Open Access. Powered by Scholars. Published by Universities.®

Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 3 of 3

Full-Text Articles in Computer Engineering

Formal Modeling And Analysis Of A Family Of Surgical Robots, Niloofar Mansoor Dec 2019

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 Nov 2018

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 …


Secure Access Control In Multidomain Environments And Formal Analysis Of Model Specifications, Fatemeh Nazerian, Homayun Motameni, Hossein Nematzadeh Jan 2018

Secure Access Control In Multidomain Environments And Formal Analysis Of Model Specifications, Fatemeh Nazerian, Homayun Motameni, Hossein Nematzadeh

Turkish Journal of Electrical Engineering and Computer Sciences

Distributed multiple organizations interact with each other. If the domains employ role-based access control, one method for interaction between domains is role-mapping. However, it may violate constraints in the domains such as role hierarchy, separation of duty, and cardinality. Therefore, autonomy of the domains is lost. This paper proposes secure interoperation in multidomain environments. For this purpose, a cross-domain is created by foreign permission assignment. In an effort to maintain the autonomy of every domain, several rules are defined formally. Then, a decentralized scheme is used to provide permission mapping between domains. At the next stage, the proposed cross-domain is …