Nobody's perfect: interactive synthesis from parametrized real-time scenarios

ABSTRACT

As technical systems keep growing more complex and sophisticated, designing software for the safety-critical coordination between their components becomes increasingly difficult. Verifying and correcting these components already represents a significant part of the development process both with respect to time and cost. Scenario-based synthesis has been put forward as an approach to accelerate the transition from requirements to a correct, verified model. In (8), we have presented a synthesis technique for deriving pattern behavior from a set of timed scenarios with parametrized time constraints. The derived patterns can then be verified using our technique for the compositional formal verification of Mechatronic UML models as introduced in (10). In this paper, we argue that the practical relevance of a synthesis technique predominantly depends rather on its ability to identify and point to specification errors than the complexity of the scenarios it could, in theory, process, provided with a correct specification. By means of a case study, we introduce the different types of specification errors that may arise during synthesis. Using our tools for modeling, synthesis, and verification, we then show how we can identify and resolve these errors in the successive phases of an interactive development process.

References

1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 414--425, Philadelphia, PA, 1990.
2. R. Alur, T. A. Henzinger, and M. Y. Vardi. Parametric real-time reasoning. In Proceedings of the twenty-fifth annual ACM symposium on Theory of computing, pages 592--601. ACM Press, 1993.
3. B. Becker, D. Beyer, H. Giese, F. Klein, and D. Schilling. Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation. In Proc. of the 28th International Conference on Software Engineering (ICSE), Shanghai, China. ACM Press, 2006. (accepted).
4. G. Behrmann, A. David, and K. G. Larsen. A tutorial on sc uppaal. In M. Bernardo and F. Corradini, editors, Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, number 3185 in LNCS, pages 200--236. Springer--Verlag, September 2004.
5. Y. Bontemps and P. Heymans. As fast as sound (lightweight formal scenario synthesis and verification). In H. Giese and I. Krüger, editors, Proc. of the 3rd Int. Workshop on "Scenarios and State Machines: Models, Algorithms and Tools" (SCESM'04), pages 27--34, Edinburgh, May 2004. IEE.
6. S. Burmester and H. Giese. The Fujaba Real-Time Statechart PlugIn. In Proc. of the Fujaba Days 2003, Kassel, Germany, October 2003.
7. S. Burmester, H. Giese, M. Hirsch, D. Schilling, and M. Tichy. The Fujaba Real-Time Tool Suite: Model-Driven Development of Safety-Critical, Real-Time Systems. In Proc. of the 27th International Conference on Software Engineering (ICSE), St. Louis, Missouri, USA, pages 670--671. ACM Press, May 2005.
8. S. Burmester, H. Giese, and F. Klein. Synthesis of Parameterized UML Real-Time Patterns from Multiple Parameterized Real-Timed Scenarios. In F. Bordeleau, S. Leue, and T. Systä, editors, Scenarios: Models, Algorithms and Tools, volume 3371 of Lecture Notes in Computer Science, pages 193--211. Springer Verlag, April 2005.
9. H. Giese and M. Hirsch. Checking and Automatic Abstraction for Timed and Hybrid Refinement in Mechtronic UML. Technical Report tr-ri-03-266, University of Paderborn, Paderborn, Germany, December 2005. (to appear).
10. H. Giese, M. Tichy, S. Burmester, W. Schäfer, and S. Flake. Towards the Compositional Verification of Real-Time UML Designs. In Proc. of the European Software Engineering Conference (ESEC), Helsinki, Finland, pages 38--47. ACM Press, September 2003.
11. D. Harel and R. Marelly. Playing with Time: On the Specification and Execution of Time-Enriched LSCs. In Proc. 10th IEEE/ACM Int. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2002), Fort Worth, Texas, USA, 2002. (invited paper).
12. T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. In Proc. of IEEE Symposium on Logic in Computer Science. IEEE Computer Press, 1992.
13. M. Hirsch and H. Giese. Towards the Incremental Model Checking of Complex RealTime UML Models. In Proc. of the Fujaba Days 2003, Kassel, Germany, October 2003.
14. I. Krüger, R. Grosu, P. Scholz, and M. Broy. From MSCs to Statecharts. In F. J. Rammig, editor, Distributed and Parallel Embedded Systems, pages 61--71. Kluwer Academic Publishers, 1999.
15. X. Li and J. Lilius. Timing Analysis of UML Sequence Diagrams. In R. France and B. Rumpe, editors, UML'99 - The Second International Conference on The Unified Modeling Language Fort Collins, Colorado, USA, volume 1723 of Lecture Notes in Computer Science, October 1999.
16. E. Mäkinen and T. Systä. MAS - an interactive synthesizer to support behavioral modeling in UML. In Proceedings of the 23rd International Conference on Software Engineering (ICSE 2001), Toronto, Canada, pages 15--24, May 2001.
17. Object Management Group. UML 2.0 Superstructure Specification, 2003. Document ptc/03-08-02.
18. A. Salah, R. Dssouli, and G. Lapalme. Implicit integration of scenarios into a reduced timed automaton. Information and Software Technology, 45:715--725, August 2003.
19. B. Sengupta and R. Cleaveland. Triggered Message Sequence Charts. In W. G. Griswold, editor, Proceedings of the Tenth ACM SIGSOFT Symposium on the Foundations of Softare Engineering (FSE-10), Charleston, South Carolina, USA, November 2002. ACM Press.
20. S. Somé, R. Dssouli, and J. Vaucher. From Scenarios to Timed Automata: Building Specifications from Users Requirements. In Proceedings of the 1995 Asia Pacific Software Engineering Conference (APSEC '95), 1995.
21. S. Uchitel and J. Kramer. A Workbench for Synthesising Behviour models from Scenarios. In Proceedings of the 23rd International Conference on Software Engineering (ICSE 2001), Toronto, Canada, pages 188--197, May 2001.
22. W. Vickrey. Counterspeculation and Competitive Sealed tenders. Journal of Finance, 16:8--37, March 1961.
23. M. Walicki and S. Meldal. Algebraic Approaches to Nondeterminism - an Overview. ACM Computing Surveys, 29(1):30--81, March 1997.
24. J. Whittle and J. Schumann. Generating statechart designs from scenarios. In Proceedings of the 22nd international conference on on Software engineering June 4 - 11, 2000, Limerick Ireland, 2000.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Designing software

      • Requirements analysis

      • Software implementation planning

        • Software design techniques

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification