Events Calendar

PhD Defense - Ivo Krka

Title: Deriving Component-Level Behavior Models from Scenario-Based Requirements

PhD Candidate: Ivo Krka

Committee:
Nenad Medvidovic (Chair)
Leana Golubchik
Sandeep Gupta
Sebastian Uchitel (University of Buenos Aires)

Use-case scenarios, with notations such as UML sequence diagrams, are widely used, often in combination with formalized system goals and event invariants, to specify the desired behavior of a software system. These intuitive requirement specification notations only partially specify the system-to-be by prohibiting or requiring certain behaviors, while leaving other behaviors uncategorized into either of those. Engineers iteratively refine and elaborate the requirements specification by eliciting more requirements to finally arrive at a complete behavior description. Partial-behavior models, such as modal transition systems (MTS), have been utilized as a formal foundation for capturing partial system specifications. Mapping the requirements to partial behavior models enables automated analyses (e.g., requirements consistency checking) and helps to elicit new requirements, thus assisting the requirements specification practices.

Although intuitive, the existing requirements notations allow engineers to specify behaviors with unintended semantic side-effects. In particular, the current practices support reasoning about and specification of a system's behavior exclusively at the system level, disregarding the fact that a system typically consists of interacting components. This runs the risk of arriving at an inconsistent specification (i.e. one that is not realizable as a composition of the system's components), which can prove costly if left unresolved.

To address the shortcomings of the current practices, this dissertation explores three strategies to enable transitioning from a scenario-based requirements specification to a set of component-level MTSs: (1) heuristically creating component MTSs from a system-level scenario-based specifications, (2) enhancing the way scenarios are specified, and (3) mapping the refinements performed on a system MTS to refinements to-be-performed on component-level MTSs. These strategies have been implemented with the following suite of techniques:
1. A heuristic algorithm that synthesizes a set of component-level MTSs from a set of existential scenarios and system operation invariants.
2. Component-aware Triggered Scenarios (caTS), a triggered-scenario language that enables expressing reactive behaviors of system components.
3. A framework that, given a system MTS refinement based on a new requirement, propagates that refinement to a set of component MTSs.

As they work with different inputs, selecting the appropriate technique depends on the context such as restrictions on adopting new notations and the required level of formality. In addition, the heuristic synthesis algorithm has been adapted and modified into Trace-Enhanced MTS Inference (TEMI) algorithm to work with information about the observed implementation-level system executions.

The proposed techniques have been theoretically evaluated to assess their complexity, correctness, and completeness. The techniques have also been applied on a number of real-world and automatically generated case studies. The results suggest that the generated MTSs accurately capture those component implementations that (1) necessarily provide the behavior required by the scenarios, (2) restrict behavior forbidden by the requirements specification, and (3) leave the behavior that is neither explicitly required nor forbidden as undefined. Furthermore, the proposed techniques help to detect potential specification flaws as they are specified, correct the existing errors, and prevent future inconsistencies. In case of heuristic MTS synthesis, the algorithm has been proven applicable to very large system specifications. The performed quantitative evaluations also confirmed significant savings in specification effort when caTS scenarios are used in place of existing notations. Finally, based on evaluations performed on nine off-the-shelf libraries, the TEMI algorithm has improved significantly upon the state-of-the-art in dynamic model inference, producing models of higher quality in terms of precision and recall.

Location: Hughes Aircraft Electrical Engineering Center (EEB) - 248

Audiences: Everyone Is Invited

Contact: Lizsl De Leon