Analysis and synthesis for parameterized timed sequence diagrams
Holger Giese · 2004
Today, an increasing demand for high quality real-time software for complex, safety-critical systems results from the fact that more ambitious and complex technical systems are built. In the development of such systems, a crucial step is the design and formal verification of the real-time interaction of the components to ensure the correctness and safe operation of the overall system. We propose to ease this cumbersome design step by supporting the analysis of conflicts between timed scenarios and the scenario-based synthesis of the required component behavior. Such a synthesis procedure, which requires as its input a set of timed scenarios, results in a set of statecharts that realize the given scenarios. By supporting even parameterized timed scenarios, the approach permits to avoid too early decisions on specific values for the time constraints while still being able to check them. We describe the application of the approach and the available prototypical tool support by means of a running example.