COMPARING AND IMPROVING THE SYNTHESIS OF STATE-BASED SPECIFICATIONS FROM SCENARIO-BASED SPECIFICATIONS

摘要

The scenario-based specifications are popularly used to capture user requirements. The state-based specifications are very appropriate to capture system design. Recently, there has been increased research interest in connecting these two kinds of specifications, called synthesis. Synthesis is a way to automatically construct the state-based specifications from the scenario-based specifications. There are two kinds of synthesis methods: global synthesis and local synthesis. Global synthesis means constructing a state-based specification for the whole system from the scenario-based specifications, while local synthesis means constructing a state-based specification for each object in the system. The two different synthesis methods have different uses and need to be systematically compared. The contributions of this paper are twofold. Firstly, we propose an improved method supporting the global and the local synthesis of state machines (a kind of state-based specifications) by using a novel algorithm for state machine execution and an algorithm similar to operator priority analysis method, which can fully automate the process of synthesis. Our synthesis method also satisfies two important properties: completeness and soundness. Secondly, to the best of our knowledge, our work does the first attempt to systematically compare global synthesis with local synthesis, and shows some insightful results of the experimental comparison between the two kinds of synthesis methods, which are valuable for the practitioners to choose an appropriate synthesis method for the analysis and verification of the system.