Link to Colorado State University Home Page




Lightweight Analysis of Software Models

Contents

People

Current Project Members:

Funding

Project Summary

Publications

The documents contained in these area are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Abstract

Developing adequate system operation contracts at the requirements level can be challenging. A specifier needs to ensure that a contract allows an operation to be invoked in different usage contexts without putting the system in an invalid state. Specifiers need usable rigorous analysis techniques that can help them develop more robust contracts, that is, contracts that are neither too restrictive nor too permissive. In this paper we describe an iterative approach to developing robust operation contracts. The approach supports rigorous robustness analysis of operation contracts against a set of scenarios that provide usage contexts for the operation. We illustrate the approach by developing a robust operation contract for a functional feature in a Location-aware Role-Based Access Control (LRBAC) model.

Abstract

The use of the Unified Modeling Language (UML) for specifying security policies is attractive because it is expressive and has a wide user base in the software industry. However, there are very few mature tools that support rigorous analysis of UML models. Alloy is a formal specification language that has been used to rigorously analyze security policies, but few practitioners have the background needed to develop good Alloy models. We propose a new approach to policy analysis in which designers use UML at the front-end to describe their security policies and the Alloy Analyzer is used at the backend to analyze the modeled properties. The UML-to-Alloy and Alloy-to-UML transformations obviate the need for security designers to understand the Alloy specification language. The proposed approach supports the analysis of both functional and structural aspects of security policies.

Abstract

Identifying and resolving design problems in the early software development phases can help ensure software quality and save costs. In this research we will develop a lightweight approach to uncovering errors in UML design models consisting of class diagrams with invariants and operation specifications expressed in the OCL. In this analysis method a set of scenarios created by a verifier is used to check the functionality specified by operations in the design class diagrams. The scenario generation technique utilizes use cases, misuse cases and activity diagrams describing allowed and disallowed functionality. The method is lightweight in that it analyzes behavior of UML design class model within the scope of a set of scenarios. It is static in that it does not animate or execute the UML design. Empirical studies will be done to evaluate the effectiveness of the method.

Abstract

There is a need for rigorous analysis techniques that developers can use to uncover security policy violations in their UML designs. There are a few UML analysis tools that can be used for this purpose, but they either rely on theorem-proving mechanisms that require sophisticated mathematical skill to use effectively, or they are based on model-checking techniques that require a .closed-world. view of the system (i.e., a system in which there are no inputs from external sources). In this paper we show how a lightweight, scenario-based UML design analysis approach we developed can be used to rigorously analyze a UML design to uncover security policy violations. In the method, a UML design class model, in which security policies and operation specifications are expressed in the Object Constraint Language (OCL), is analyzed against a set of scenarios describing behaviors that adhere to and that violate security policies. The method includes a technique for generating scenarios. We illustrate how the method can be applied through an example involving rolebased access control policies

Abstract

Static analysis tools, such as OCLE and USE, can be used to analyze structural properties of class models. The USE tool also provides support for analyzing specified operations through interactive simulations in which users provide operation parameters, and manually assign values to state elements to reflect the effect of an operation. In this paper we describe an approach to statically analyzing behavior that does not require a user to manually simulate behavior. The approach involves transforming a class model into a static model of behavior, called a Snapshot Model. A Snapshot Model characterizes sequences of snapshots, where a snapshot describes an application state. A scenario describing a sequence of operation invocations can be verified against a Snapshot Model using tools such as USE and OCLE. We illustrate our approach by verifying a scenario against a Snapshot Model that describes the behavior of some operations in a role-based access control (RBAC) application.

Abstract

Identifying and resolving design problems in the early design phase can help ensure software quality and save costs. There are currently few tools for analyzing designs expressed using the Unified Modeling Language (UML). Tools such as OCLE and USE support analysis of static structural properties. These tools provide mechanisms for checking instance models against invariant properties expressed using the Object Constraint Language (OCL). In this paper we propose an approach to analyzing behavioral properties of UML models that can utilize static analysis tools. The approach includes a technique for generating a class model of behavior from operation specifications expressed in a restricted form of OCL Behavioral properties are expressed as invariants defined in the class model of behavior. Static analysis tools such as USE and OCLE can be used to check object models describing series of snapshots. Most of the analysis can be automated. We illustrate our approach by analyzing static separation of duty and dynamic separation of duty properties of a hierarchical role-based access control model (HRBAC).

Last Updated 12/20/2011