Requirements Elicitation And Formalization Modeling Based On Scenarios And Properties

The scenarios are widely recognized as an effective ways for requirements elicitation, documentation and certification. The scenarios provide examples of the intended system behaviour,i.e., sequences of interactions that the system is expected to exhibit. A scenario does not describe universal requirement for all system behaviours completely, so the behaviour model based on the single scenario only provides a lower bound of the intended system. Properties are statements which characterize the behaviours that must be satisfied, The behaviour model from properties contains the possible traces which do not violate properties. Thus, the behaviour modeling provides a upper bound for the intended system. The research emphasis of the thesis is how to construct the lower bound of the intended system based-on scenarios, how to construct the upper bound of the intended system based-on properties,and how to get the final intended system between the lower behaviour model and the upper behaviour model.The first solution is how to do the requirement elicitation based-on the scenarios and properties. MSC, a representation of scenarios, is used to describe the communication, interaction between the components in the scenarios, thus, the thesis first introduces the main concept of MSC.3-FLTL is an effective way to describe the system properties, so, after introducing the 3-value Kleen logic and fluent,3-FLTL is introduced.Then, by the examples of the forum post,the requirement is elicited based on the description of scenarios, generates the MSC, formalizes the requirement as the properties description.LTS synthesis based on the scenarios only describe the behaviours provided by scenarios, and do not describe the possible behaviours which is not provided by scenarios. LTS synthesis based on the properties blurs the distinction between the behaviours that may occur as they will not violate properties and the behaviours that must occur in order to avoid a violation of properties. With regard to the existed synthesis algorithm, we present the MTS synthesis algorithm on the base of the existed synthesis algorithm. We present a algorithm to turn LTS into MTS on the base of existed LTS synthesis algorithm scenarios-based, and get a lower bound of requisite behaviours of the intended system. The synthesis MTS model can distinguish the requisite behaviours and possible behaviours. Then we merge the two MTSs to one MTS by the merging operator, the model preserves the requisite behaviours of the lower bound and the possible behavours of the upper bound. After merging,the system behavour can further refine, The MTS refinement can not preserve the initial properties and scenarios, but support the elicitation of the new scenarios and properties.