The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - May/June (2009 vol.35)
pp: 384-406
Greg Brunet , University of Toronto, Toronto
Sebastian Uchitel , Imperial College London and FCEN-University of Buenos Aires
ABSTRACT
Synthesis of behavior models from software development artifacts such as scenario-based descriptions or requirements specifications helps reduce the effort of model construction. However, the models favored by existing synthesis approaches are not sufficiently expressive to describe both universal constraints provided by requirements and existential statements provided by scenarios. In this paper, we propose a novel synthesis technique that constructs behavior models in the form of Modal Transition Systems (MTS) from a combination of safety properties and scenarios. MTSs distinguish required, possible, and proscribed behavior, and their elaboration not only guarantees the preservation of the properties and scenarios used for synthesis but also supports further elicitation of new requirements.
INDEX TERMS
Modal transition systems, merge, synthesis, partial behavior models.
CITATION
Greg Brunet, Sebastian Uchitel, "Synthesis of Partial Behavior Models from Properties and Scenarios", IEEE Transactions on Software Engineering, vol.35, no. 3, pp. 384-406, May/June 2009, doi:10.1109/TSE.2008.107
REFERENCES
[1] M. Abadi and L. Lamport, “The Existence of Refinement Mappings,” Theoretical Computer Science, vol. 82, no. 2, pp. 253-284, 1991.
[2] Y. Bontemps and P. Heymans, “From Live Sequence Charts to State Machines and Back: A Guided Tour,” IEEE Trans. Software Eng., vol. 31, no. 12, pp. 999-1014, Dec. 2005.
[3] G. Brunet, “A Characterization of Merging Partial Behavioural Models,” master's thesis, Univ. of Toronto, 2006.
[4] G. Bruns and P. Godefroid, “Generalized Model Checking: Reasoning about Partial State Spaces,” Proc. Int'l Conf. Concurrency Theory, pp. 168-182, 2000.
[5] J. Castro, M. Kolp, and J. Mylopoulos, “Towards Requirements-Driven Information Systems Engineering: The Tropos Project,” J.Information Systems, vol. 27, no. 6, pp. 365-389, 2002.
[6] C. Damas, B. Lambeau, and A. van Lamsweerde, “Scenarios, Goals, and State Machines: A Win-Win Partnership for Model Synthesis,” Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 197-207, 2006.
[7] D. Dams, “Abstract Interpretation and Partition Refinement for Model Checking,” PhD thesis, Eindhoven Univ. of Tech nology, July 1996.
[8] N. D'Ippolito, “MTSA: A Model Checker for Modal Transition Systems,” master's thesis, Univ. of Buenos Aires, Computing Dept., Dec. 2007.
[9] N. D'Ippolito, D. Fischbein, M. Chechik, and S. Uchitel, “MTSA: The Modal Transition System Analyzer,” Proc. Tools Track of Int'l Conf. Automated Software Eng., Sept. 2008.
[10] M. Dwyer, G. Avrunin, and J. Corbett, “Patterns in Property Specifications for Finite-State Verification,” Proc. Int'l Conf. Software Eng., pp. 411-420, 1999.
[11] D. Fischbein and S. Uchitel, “On Correct and Complete Strong Merging of Partial Behaviour Models,” Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng., Nov. 2008.
[12] D. Fischbein, S. Uchitel, and V. Braberman, “A Foundation for Behavioural Conformance in Software Product Line Architectures,” Proc. ISSTA '06 Workshop Role of Software Architecture for Testing, pp. 39-48, 2006.
[13] D. Giannakopoulou and J. Magee, “Fluent Model Checking for Event-Based Systems,” Proc. Joint European Software Eng. Conf. and ACM SIGSOFT Int'l Symp. Foundations of Software Eng., 2003.
[14] A. Gurfinkel and M. Chechik, “How Thorough Is Thorough Enough,” Proc. 13th Advanced Research Working Conf. Correct Hardware Design and Verification Methods, pp. 65-80, 2005.
[15] D. Harel, “StateCharts: A Visual Formalism for Complex Systems,” Science of Computer Programming, vol. 8, pp. 231-274, 1987.
[16] D. Harel and R. Marelly, Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, 2003.
[17] K. Havelund and G. Rosu, “Monitoring Programs Using Rewriting,” Proc. Int'l Conf. on Automated Software Eng., pp. 135-143, 2001.
[18] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, “Automated Consistency Checking of Requirements Specifications,” ACM Trans. Software Eng. and Methodology, vol. 5, no. 3, pp. 231-261, July 1996.
[19] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[20] A. Hussain and M. Huth, “On Model Checking Multiple Hybrid Views,” Proc. First Int'l Symp. Leveraging Applications of Formal Methods, pp. 235-242, 2004.
[21] A. Hussain and M. Huth, “Automata Games for Multiple-Model Checking,” Electronic Notes in Theoretical Computer Science, vol. 115, pp. 401-421, 2006.
[22] M. Huth, R. Jagadeesan, and D. Schmidt, “A Domain Equation for Refinement of Partial Systems,” Math. Structures in Computer Science, vol. 14, no. 4, pp. 469-505, 2004.
[23] M. Huth, R. Jagadeesan, and D.A. Schmidt, “Modal Transition Systems: A Foundation for Three-Valued Program Analysis,” Proc. European Symp. Programming, pp. 155-169, 2001.
[24] ITU, Recommendation z.120: Message Sequence Charts, ITU, 2000.
[25] R. Kazhamiakin, M. Pistore, and M. Roveri, “Formal Verification of Requirements Using SPIN: A Case Study on Web Services,” Proc. Int'l Conf. Software Eng. and Formal Methods, pp.406-415, 2004.
[26] S.C. Kleene, Introduction to Metamathematics. Van Nostrand, 1952.
[27] K. Koskimies and E. MLkinen, “Automatic Synthesis of State Machines from Trace Diagrams,” Software Practice and Experience, vol. 24, no. 7, pp. 643-658, 1994.
[28] J. Kramer, J. Magee, and M. Sloman, “CONIC: An Integrated Approach to Distributed Computer Control Systems,” Proc. IEE, vol. 130, no. 1, pp. 1-10, 1983.
[29] I. Krüger, R. Grosu, P. Scholz, and M. Broy, “From MSCs to Statecharts,” Distributed and Parallel Embedded Systems, Kluwer Academic Publishers, 1999.
[30] R. De Landtsheer, E. Letier, and A. van Lamsweerde, “Deriving Tabular Event-Based Specifications from Goal-Oriented Requirements Models,” Proc. IEEE Int'l Symp. Requirements Eng., pp. 200-212, 2003.
[31] K. Larsen, B. Steffen, and C. Weise, “The Methodology of Modal Constraints,” Formal Systems Specification, pp. 405-435, Springer, 1996.
[32] K. Larsen and L. Xinxin, “Equation Solving Using Modal Transition Systems,” Proc. Fifth Ann. Symp. Logic in Computer Science, pp. 108-117, July 1990.
[33] K.G. Larsen, U. Nyman, and A. Wasowski, “Modal I/O Automata for Interface and Product Line Theories,” Proc. European Symp. Programming, 2007.
[34] K.G. Larsen, B. Steffen, and C. Weise, “A Constraint Oriented Proof Methodology based on Modal Transition Systems,” Proc. First Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems, pp. 17-40, 1995.
[35] K.G. Larsen and B. Thomsen, “A Modal Process Logic,” Proc. IEEE Symp. Logic in Computer Science, pp. 203-210, 1988.
[36] E. Letier, J. Kramer, J. Magee, and S. Uchitel, “Fluent Temporal Logic for Discrete-Time Event-Based Models,” Proc. ACM SIGSOFTSymp. Foundations of Software Eng., pp. 70-79, 2005.
[37] E. Letier, J. Kramer, J. Magee, and S. Uchitel, “Deriving Event-Based Transition Systems from Goal-Oriented Requirements Models,” Technical Report 02/2006, Imperial College, 2006.
[38] E. Letier and A. van Lamsweerde, “Deriving Operational Software Specifications from System Goals,” Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 119-128, 2002.
[39] O. Lichtenstein and A. Pnueli, “Checking that Finite State Concurrent Programs Satisfy Their Linear Specification,” Proc. 12th Ann. ACM Symp. Principles of Programming Languages, pp. 97-107, 1985.
[40] J. Magee and J. Kramer, Concurrency—State Models and Java Programs, John Wiley, 1999.
[41] J. Magee, N. Pryce, D. Giannakopoulou, and J. Kramer, “Graphical Animation of Behavior Models,” Proc. Int'l Conf. Software Eng., pp.499-508, 2000.
[42] Z. Manna and A. Pnueli, “Verification of Concurrent Programs: A Temporal Proof System,” technical report, Dept. of Computer Science, Stanford Univ., 1983.
[43] C. Ponsard, P. Massonet, A. Rifaut, J.F. Molderez, A. van Lamsweerde, and H. Tran Van, “Early Verification and Validation of Mission-Critical Systems,” Proc. Workshop Formal Methods in Critical Systems, 2004.
[44] A.W. Roscoe, C.A.R. Hoare, and R. Bird, The Theory and Practice of Concurrency. Prentice-Hall, 1997.
[45] J. Sun and J. Song Dong, “Design Synthesis from Interaction and State-Based Specifications,” IEEE Trans. Software Eng., vol. 32, no. 6, pp. 349-364, June 2006.
[46] A.G. Sutcliffe, N.A.M. Maiden, S. Minocha, and D. Manuel, “Supporting Scenario-Based Requirements Engineering,” IEEE Trans. Software Eng., vol. 24, no. 12, pp. 1072-1088, Dec. 1998.
[47] S. Uchitel, G. Brunet, and M. Chechik, “Behaviour Model Synthesis from Properties and Scenarios,” Proc. Int'l Conf. Software Eng., pp. 34-43, 2007.
[48] S. Uchitel and M. Chechik, “Merging Partial Behavioural Models,” Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp.43-52, 2004.
[49] S. Uchitel, J. Kramer, and J. Magee, “Incremental Elaboration of Scenario-Based Specifications and Behaviour Models using Implied Scenarios,” ACM Trans. Software Eng. and Methodology, vol. 13, no. 1, 2004.
[50] H. Tran Van, A. van Lamsweerde, P. Massonet, and C.H. Ponsard, “Goal-Oriented Requirements Animation,” Proc. IEEE Int'l Symp. Requirements Eng., pp. 218-228, 2004.
[51] A. van Lamsweerde, “Tutorial: Goal-Oriented Requirements Engineering: From System Objectives to UML Models to Precise Software Specifications,” Proc. Int'l Conf. Software Eng., pp. 744-745, 2003.
[52] A. van Lamsweerde and E. Letier, “Handling Obstacles in Goal-Oriented Requirements Engineering,” IEEE Trans. Software Eng., vol. 26, no. 10, pp. 978-1005, Oct. 2000.
[53] M.Y. Vardi and P. Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” Proc. First Symp. Logic in Computer Science, pp. 322-331, 1986.
34 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool