FormlSlicer: A Model Slicing Tool for Feature-rich State-machine Models

software requirements;feature interactions;state machines;model-based engineering;model slicing;Computer Science

Lai, Xiaoni

University of Waterloo

关键词: software requirements;    feature interactions;    state machines;    model-based engineering;    model slicing;    Computer Science;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/9413/3/Lai_Xiaoni.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

A model of the feature-oriented requirements of a software system usually contains a large number of non-trivial features; each feature may have unintended interactions with other features. It may be difficult to comprehend or verify such a model. Model slicing is a useful approach to overcome such a challenge by enabling views of models of individual features that preserve feature interactions. Model slicing evolves from traditional program slicing; it is a technique to extract a sub-model from the original model with respect to a slicing criterion. In this thesis we focus on one type of model: state-based models (SBMs). Because of the difference in granularity between programs and SBMs, as well as the difficulty of maintaining well-formedness of a sliced SBM, SBM slicing is much more challenging than program slicing. Among a diverse range of slicing approaches, dependence-based slicing is the most popular; it relies on the computation of dependence relations among states and transitions in order to determine which model elements of the original model must be in the slice and which can be omitted.We present a workflow and tool for automatically constructing a feature-based slice from a feature-oriented state-machine model of the requirements of a software system. Each feature in the model is modeled as a complete state-transition machine called a feature-oriented state machine (FOSM). The workflow consists of two tasks—a preprocessing task and a slicing task. The preprocessing task mainly computes three types of dependences: hierarchy dependence (HD), which represents the state hierarchy relation among states in the original model; data dependence (DD), which captures the define-use relationship among transitions with respect to a variable; and control dependence (CD), which captures the notion of whether one state can affect the execution of another state or transition. The slicing task forks off multiple slicing processes; each process considers one of the FOSMs as the feature of interest (FOI)—which is the slicing criterion—and the rest of FOSMs as the rest of the system (ROS)—which is to be sliced. Each slicing process constructs a sliced model to preserve the portion of the ROS that interacts with the FOI. The construction process is multi-staged; it firstly identifies an initial set of transitions in the ROS that directly affect the FOI; it then finds more states and transitions in the transitive closure of dependences; and it eventually restructures the model to further reduce the model size and maintain its well-formedness property.We provide a correctness proof that shows that the resulting sliced models simulate the original model, by proving that an execution step of a given execution trace in the original model can always be projected to an execution step of at least one execution trace in the sliced model.Our proposed slicing workflow has been implemented in a tool called FormlSlicer. We conducted an empirical evaluation that demonstrates that, on average, the ROS of a sliced model has 23.0% of states, 15.7% of transitions, 32.8% of regions and 19.3% of variables of the ROS of the original model.