Enabling Requirements Elaboration Through Synthesis, Refinement, and Analysis of Partial Behavior Models

In general, one of the main shortcoming of the existing approaches in the context of incremental requirements elaboration is their focus on synthesizing closed behavioral models. In other words, these approaches overlook the inherent partiality of the input specications thus disabling incremental
specication renement [19]. Problem 2 is closely related to techniques for more scalable analysis of a system's behavior. Today, scalability is mandatory due to the ever growing software complexity. Solutions to behavioral analysis are
typically based on compositional and hierarchical reasoning techniques such as assume-guarantee reasoning [3] and compositional reachability analysis [2].

However, such approaches are primarily designed for model analysis and do
not consider model renement. Hence, they cannot readily solve Problem 2. The last outlined problem above has been considered for dierent types of requirements speci- cations. For example, Letier and van Lamsweerde proposed
tactics for elaboration of goal models [11], and a methodology for analysis and renement of system goals [22]. These and similar approaches are primarily designed for renement and analysis of narrowly scoped requirements.

Conversely, my work is concerned with gradual renement of a system's specication when both the system requirements and the software architecture are available and rened in parallel; this is often the case in modern software development [18].