Synthesizing multi-view models of software systems

Models play a significant role for analyzing requirements and exploring designs of software systems. Good models should focus on key aspects of the target system while abstracting from numerous details. The joint use of multiple modeling languages allows analysts to capture complementary system views in a complete, precise, and consistent way. Such models prove difficult to build in practice. Techniques and tools are therefore required for supporting analysts in this task. Model synthesis techniques may help in building models systematically from various sources of knowledge about the target system. Such techniques may integrate dedicated checks on the models being built. Early errors can thereby be detected and fixed. Model synthesis can also produce missing model fragments, support documentation, or generate code fragments for specific software components. The thesis proposes tool-supported synthesis techniques for multi-view models involving scenarios, state machines, processes, and goals. A formal trace semantics is provided for process models together with algorithms for deriving state machines from them. This enables a variety of checks on processes, including the verification that they satisfy desired properties. An interactive technique is then presented for synthesizing behavior models from scenarios. A grammar induction framework is extended to generalize examples of desired behavior under the control of counterexamples and goals to be met by the system. The induction process interacts with the end-user who needs to classify additional scenarios generated by the synthesizer as positive or negative examples of desired system behavior. The proposed techniques are implemented by a toolset, whose architecture is briefly described. Our inductive synthesizer has been evaluated in depth on various case studies and on synthetic datasets. These evaluations resulted in an online protocol and platform for evaluating inductive synthesis techniques.(FSA 3) -- UCL, 201