Synthesis of Open Reactive Systems from Scenario-Based Specifications

• Autorzy: Bontemps Y. , Schobbens P-Y. , Löding Ch.
• Konferencja: Third International Conference on Application of Concurrency to System Design (ACSD'03) (18-20 June, 2003, Guimaraes, Portugal)
• Języki publikacji: EN

Abstrakty

EN

We propose here Live Sequence Charts with a new, game-based semantics to model interactions between the system and its environment. For constructing programs automatically, we give an algorithm to synthesize either a strategy for the system ensuring that the specification is respected, or, if the specification is unimplementable, a strategy for the environment forcing the system to fail. We introduce the concept of mercifulness, a desirable property of the synthesized program. We give a polynomial time algorithm for synthesizing merciful winning strategies.

Słowa kluczowe

EN

Live Sequence Charts; safety; consistency; synthesis; mercifulness

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 62, nr 2
• Strony: 139--169
• Opis fizyczny: Bibliogr. 60 poz., tab., wykr.

Twórcy

autor

Bontemps Y.

• Computer Science Depariment, Universily of Namur Namur, Belgium

autor

Schobbens P-Y.

• Computer Science Depariment, Universily of Namur Namur, Belgium

autor

Löding Ch.

• Lehrstuhl für Informatik VII. RWTH Aachen, Aachen. Germany

Bibliografia

• [1] Abadi. M., Lamport, L.: Composing Specifications, ACM Transactions on Programming Languages and Systems, 15(1). January 1993. 73-132.
• [2] Abadi, M., Lamport, L., Wolper, P.: Realizable and Unrealizable Specifications of Reactive Systems, Automata. Languages and Programming, I6th International Colloquium. ICALP89. Stresa. Italy. July 11-15, 1999, Proceedings (G. Ausiello, M. Dezani-Ciancaglini, S. R. D. Rocca, Eds.), 372, Springer, 1989. ISBN 3-540-51371-X.
• [3] de Alfaro, L., Henzinger, T, A., Stoelinga, M.: Timed Interfaces, Proc. of EMSOFT 2002, Second International Workshop on Embedded Software (A, Sangiovanni-VincenteUi. J. Sifakis, Eds.), 2491, Springer, Grenoble, France, October 2002.
• [4] Alprn, B., Schneider, F. B.: Defining Liveness, Information Processing Letters, 21(4), October 1985,181-185, ISSN 0020-0190.
• [5] Alur, R., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts, Proceedings of 22nd International Conference on Software Engineering, 2000.
• [6] Alur, R., Henzinger, T. A., Kupferman, C: Alternating-time temporal logic. Journal of the ACM (JACM), 49(5), 2002,672-713, ISSN 0004-5411.
• [7] Amyot. D., Eberiein, A.: An Evaluation of Scenario Notations for Telecommunication Systems Development, Proc. of 9th Int. Conference on Telecommunication Systems (9ICTS), Dallas, USA, March 2001.
• [8] Antoniotti, M.: Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the Control-D system, Ph.D. Thesis, New York University, New York, 1995.
• [9] Berry, G.: The Foundations of ESTEREL, in; Proof Language and Interaction: Essays in Honour of Robin Milner (G. Plotkin, C. Stirling, M. Tofte, Eds.), MIT Press, 1998.
• [10] Biermann, A. W., Krishnaswamy, R.; Constructing Programs from Example Computations. IEEE Transactions on Software Engineering (TSE), SE-2(3), September 1976, 141-153.
• [11] Bontemps, Y.: Automated Verification of State-based Specifications Against Scenarios (A Step towards Relating Inter-Object to Intra-Object Specifications), Master Thesis, University of Namur, rue Grandgagnage, 21-5000 Namur(Belgium), June 2001.
• [12] Bontemps, Y.: Realizability of Scenario-based Specifications. Diplôme d'études approfondies, Eacultes Universitaires Notre-Dame de la Paix, Institut d'Informatique (University of Namur, Computer Science Dept), rue Grandgagnage, 21. B5000 - Namur (Belgium), September 2003.
• [13] Blichi, J., Landweber, L. H.: Solving sequential conditions finite-state strategies, Trans. Ameri. Math. Soc, 138,1969.295-311.
• [14] Church, A.: Logic, arithmetic and automata, Proc. of Intern. Cong. Math, 1963.
• [15] Cobben. J., Engels. A., Mauw. S., Reniers, A., M.: Formal Semantics of Message Sequence Charts (ITU-T Recommendation Z.120 Annex B), International Telecommunication Union, Eindhoven, The Netherlands, April 1998. http://www.itu.int.
• [16] Damm, W., Harel. D.: LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System , 19(1). 2001.45-80.
• [17] Desforges, P.: Industrialisation of the B method. La lettre B, 1(1), Nov 1996.
• [18] Desharnais, J., Frappier, M., Khedri, R., Mili, A.: Integration of Sequential Scenarios, IFEE Transactions on Software Engineering. 24(9), September 1998, 695-708.
• [19] Diethelm. I., Geiger, L., Maier, T., Zundorf. A.: Turning Collaboration Diagram Strips into Storycharts, Proc. of "Scenarios and State-Machines: models, algorithms and tools" (SCESM) workshop of the 24th Int. Conf on Software Engineering (ICSE 2002). ACM, Orlando, FL, May 2002, http : //www.cs.tut.fi/ ~tsysta/ICSE/papers/.
• [20] Dwyer, M. B., Avrunin, G, S., Corbett, J. C: Patterns in Property Specifications for Finite-State Verification, Proceedings of the 21st International Conference on Software Engineering, ACM, May 1999.
• [21] Emerson, E. A., Clarke, E. M.: Using branching time temporal logic to synthesize synchronization skeletons, Science of Computer Programming, 2(3), December 1982, 241-266, ISSN 0167-6423.
• [22] Finkbeiner, B., Kruger, I. H.: Using Message Sequence Charts for Component-based Formal Verification, Proc. of OOPSLA 2001 Workshop on Specification and Verification of Component-Based Systems, Tampa Bay, FL, USA, October 2001.
• [23] Gradel. E., Thomas. W., Wilke, T., Eds.: Automata Logics, and Infinite Games: A Guide to Current Research, vol. 2500 of Lect. Notes in Comp. Sci., Springer, November 2002, ISBN 3-540-00388-6.
• [24] Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications, International Journal of Foundations of Computer Science, 13(1), February 2(X)2, 5-51, (Preliminary version appeared in, Proc. Fifth Int. Conf on Implementation and Application of Automata (CIAA 2000), LNCS 2088, July 2000.).
• [25] Harel. D., Kugler, H., Marelly, R., Pnueli, A.: Smart Play-Out of Behavioral Requirements, Proc. 4th Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD'O2), Portland, Oregon, 2002, To appear. Also available as Tech. Report MCS02-08, The Weizmann Institute of Science.
• [26] Harel, D., Marelly, R.: Come, let's play! Scenario-based programming using LSCs and the Play-engine, Springer, 2003, ISBN 3-540-00787-3.
• [27] Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: the STATEMATE Approach, McGraw-Hill, 1998, ISBN 0-070-26205-5.
• [28] Hsia, P., Samuel, J., Gao, J., Kund, D., Toyoshima, Y., Chen, C: Formal Approach to Scenario Analysis, IEEE Journal, March 1994, 33-41.
• [29] Huber, F., Schatz, B., Einert, G.: Consistent Graphical Specification of Distributed Systems, EME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 4th International Symposium of Formal Methods Europe, Graz. Austria, September 15-19. 1997, Proceedings (J. S. Fitzgerald, C. B. Jones, P Lucas, Eds.), 1313, Springer, 1997, ISBN 3-540-63533-5.
• [30] MSC-2000: ITU-T Recommendation Z.120: Message Sequence Chart (MSC), 2000, http://www.itu.int/.
• [31] Jacobson, I.: Object Oriented Software Engineering: a Use-Case Driven Approach, ACM Press/Addison-Wesley, 1992.
• [32] Klose, J., Wittke. H.: An Automata Based Interpretation of Live Sequence Charts, Proc. of TACAS (Tools and Algorithms for the Construction and Analysis of Systems) 2001 (T. Margaria, W. Yi. Eds.), 2031, Springer-Verlag, Genova, Italy, April 2001.
• [33] Koskimies, K., Mannisto, T, Systa, T., Tuomi, J.: SCED: A Tool for Dynamic Modelling of Object Systems, Technical Report Report A-1996-4, Department of Computer Science, University of Tampere, University of Tampere, Department of Computer Science, PO. Box 607, FIN-33101 Tampere, Finland, July 1996, ISBN 951.44-4003-X, ISSN 0783-6910.
• [34] Kruger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to Statecharts, Kluwer Academic Publishers, 1999, Franz J. Rammig (ed).
• [35] Kupferman, O., Vardi, M. Y: Synthesizing distributed Systems, Proc. 16th IEEE Symp. on Logic in Computer Science, July.2001.
• [36] Kupferman, O., Vardi, M. Y, Wolper, P: Module Checking, Information and Computation. 164, 2001, 322-344.
• [37] Lamouchi, H. M., Thistle, J. G.: Effective control synthesis for DES under partial observations. Proc. 39th IEEE Conference on Decision and Control (Session on Discrete Event Systems), IEEE, Sidney, Australia, December 2000.
• [38] Li, Y. Wonham. W.: On supervisory control of real-time discrete-event systems, Information Sciences, 46(3), 1988, 159-183.
• [39] Madhusudhan, P., Thiagarajan, P.: A Decidable Class of Asynchronous Distributed Controllers. Proc. of CONCUR '02, 2421, Springer. Brno, Czech Republic, 2002.
• [40] Manna, Z., Wolper. P.: Synthesis of Communicating Processes from Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 6(1), 1984, 68-93, ISSN 0164-0925.
• [41] Martin, D. A.: Borel Determinacy, Annals of Mathematics, 102, 1975, 363-371.
• [42] Object Management Group (UML Revision Task Force): OMG UML Specification (2.0), September 2003, http://www.omg.org/uml.
• [43] Pnueli. A., Rosner, R.: On the Synthesis of a Reactive Module, Proceedings of the sixteenth annual ACM symposium on Principles of programming languages, 1989, ISBN 0-89791-294-2.
• [44] Puri. A., Tripakis, S., Varaiya, P.: Problems and Examples of Decentralized Observation and Control for Discrete Event Systems, in: Synthesis and Control of Discrete Event Systems (B. Caillaud, P. Darondeau, L. Lavagno, X. Xie, Eds.), Kluwer Academic Publisher, January 2002, ISBN 0-7923-7639-0.
• [45] Ramadge, P. J. G., Wonham, W. M.: The Control of Discrete Event Systems. Proceedings of the IEEE; Special issue on Dynamics of Discrete Event Systems, 77, 1. 1989. 81-98.
• [46] Rosner, R.: Modular Synthesis of Reactive Systems, Ph.D. Thesis, The Weizmann Institute of Science, Rehovot, Israel, April 1992.
• [47] Safra, S.: On the complexity of w-automata, 29th annual Symposium on Foundations of Computer Science, October 24-26. 1988, White Plains. New York (IEEE. Ed.). IEEE Computer Society Press. 1109 Spring Street. Suite 300, Silver Spring. MD 20910. USA, 1988. ISBN 0-8186-0877-3 (paperback). 0-8186-4877-5 (microfiche). 0-8186-8877-7 (hard).
• [48] Thistle, J. G.: Supervisory Control of Discrete Event Systems, Mathl Comput. Modelling, 23(11/12), 1996, 25-53.
• [49] Thistle, J. G., Malhame. R. P.: Control of ω-automata under state fairness assumptions. Systems and Controls Letters, 33, 1998.265-274.
• [50] Thistle. J. G., Wonham, W. M.: Control of infinite behavior of finite automata, SIAM J. Control and Optimization, 31(A), My 1994,1075-1097.
• [51] Thistle, J. G., Wonham, W. M.: Supervision of infinite behavior of discrete-event systems. SIAM J. Control and Optimization, 32(4), July 1994. 1098-1113.
• [52] Thomas, W.: Infinite games and verification. Proceedings of the International Conference on Computer Aided Verification (CAV'02l 2404. Springer. 2002.
• [53] Tripakis, S.: Undecidable problems of decentralized observation and control on regular languages. Information Processing Letters, 90, 2004. 21-28.
• [54] Uchitel, S., Kramer. J.: A Workbench for Synthesizing Behaviour Models from Scenarios, Proc. of the 23rd IEEE International Conference on Software Engineering (ICSE'OI), ACM, 2001.
• [55] Uchitel, S., Kramer, J., Magee, J.: Detecting Implied Scenarios in Message Sequence Chart Specifications. Proceedings of the Joint 8th European Software Engeneering Conference und 9th ACM SIGSO FT Symposium on the Foundation of Software Engeneering (ESEC/FSE-01) (V. Gruhn, Ed.), 26, 5, ACM Press, New York, September 10-14 2001, ISSN 0163-5948.
• [56] Vardi, M. Y.: An automata-theoretic approach to fair realizability and synthesis, Proceedings of the 7th International Conference On Computer Aided Verification (P. Wolper, Ed.), 939, Springer Verlag, Liege, Belgium, 1995.
• [57] Voge, J., Jurdziński, M.: A Discrete Strategy Improvement Algorithm for Solving Parity Games (Extended Abstract), Computer Aided Verification, 12th International Conference, CAV2000, Proceedings (E. A. Emerson, A. P. Sistla, Eds.), !855, Springer, Chicago, IL, USA, July 2000.
• [58] Weidenhaupt, K., Pohl, K., Jarke, M., Haumer, P.: Scenario Usage in System Development: A Report on Current Practice, IEEE Software, 15(2). March 1998,34-45.
• [59] Whittle, J., Schumann, J.: Generating Statechart Designs from Scenarios, 22nd International Conference on Software Engineering (ICSE 2000), ACM, Limerick, Ireland, June 2000.
• [60] Wong-Toi, H., Dill, D. L.: Synthesizing Processes and Schedulers from Temporal Specifications, Computer-Aided Verification '90: Proceedings of a DIMACS Workshop (E. M. Clarke, R. P. Kurshan, Eds.), 3, American Mathematical Society, 1991.