Navegar

Colección

Datos Estadísticas

Artículo

La versión final de este artículo es de uso interno de la institución.
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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 ModalTransition 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. © 2009 IEEE.

Registro:

Documento: Artículo
Título:Synthesis of partial behavior models from properties and scenarios
Autor:Uchitel, S.; Brunet, G.; Chechik, M.
Filiación:Department of Computing, FCEN, University of Buenos Aires, Buenos Aires C1428EGA, Argentina
Department of Computing, Imperial College London, London SW7 2RH, United Kingdom
Secure Enterprise Search Group, Oracle Corp., Redwood Shores, CA 94065, United States
Department of Computer Science, University of Toronto, 10 King's College Road, Toronto, ON M5S 3G4, Canada
Palabras clave:Merge; Modal transition systems; Partial behavior models; Synthesis; Behavior model; Merge; Modal transition systems; Model construction; Partial behavior models; Requirements specifications; Safety property; Software development; Synthesis; Synthesis techniques
Año:2009
Volumen:35
Número:3
Página de inicio:384
Página de fin:406
DOI: http://dx.doi.org/10.1109/TSE.2008.107
Título revista:IEEE Transactions on Software Engineering
Título revista abreviado:IEEE Trans Software Eng
ISSN:00985589
CODEN:IESED
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v35_n3_p384_Uchitel

Referencias:

  • Abadi, M., Lamport, L., The Existence of Refinement Mappings (1991) Theoretical Computer Science, 82 (2), pp. 253-284
  • Bontemps, Y., Heymans, P., From Live Sequence Charts to State Machines and Back: A Guided Tour (2005) IEEE Trans. Software Eng, 31 (12), pp. 999-1014. , Dec
  • Brunet, G., A Characterization of Merging Partial Behavioural Models, (2006), master's thesis, Univ. of Toronto; Bruns, G., Godefroid, P., Generalized Model Checking: Reasoning about Partial State Spaces (2000) Proc. Int'l Conf. Concurrency Theory, pp. 168-182
  • Castro, J., Kolp, M., Mylopoulos, J., Towards Requirements-Driven Information Systems Engineering: The Tropos Project (2002) J. Information Systems, 27 (6), pp. 365-389
  • Damas, C., Lambeau, B., van Lamsweerde, A., Scenarios, Goals, and State Machines: A Win-Win Partnership for Model Synthesis (2006) Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng, pp. 197-207
  • Dams, D., Abstract Interpretation and Partition Refinement for Model Checking, (1996), PhD thesis, Eindhoven Univ. of Technology, July; D'Ippolito, N., MTSA: A Model Checker for Modal Transition Systems, (2007), master's thesis, Univ. of Buenos Aires, Computing Dept, Dec; D'Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S., MTSA: The Modal Transition System Analyzer (2008) Proc. Tools Track of Int'l Conf. Automated Software Eng, , Sept
  • Dwyer, M., Avrunin, G., Corbett, J., Patterns in Property Specifications for Finite-State Verification (1999) Proc. Int'l Conf. Software Eng, pp. 411-420
  • Fischbein, D., Uchitel, S., On Correct and Complete Strong Merging of Partial Behaviour Models (2008) Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng, , Nov
  • 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; Giannakopoulou, D., Magee, J., Fluent Model Checking for Event-Based Systems (2003) Proc. Joint European Software Eng. Conf. and ACM SIGSOFT Int'l Symp. Foundations of Software Eng
  • Gurfinkel, A., Chechik, M., How Thorough Is Thorough Enough (2005) Proc. 13th Advanced Research Working Conf. Correct Hardware Design and Verification Methods, pp. 65-80
  • Harel, D., StateCharts: A Visual Formalism for Complex Systems (1987) Science of Computer Programming, 8, pp. 231-274
  • Harel, D., Marelly, R., (2003) Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine, , Springer
  • Havelund, K., Rosu, G., Monitoring Programs Using Rewriting (2001) Proc. Int'l Conf. on Automated Software Eng, pp. 135-143
  • Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G., Automated Consistency Checking of Requirements Specifications (1996) ACM Trans. Software Eng. and Methodology, 5 (3), pp. 231-261. , July
  • Holzmann, G.J., The Model Checker SPIN (1997) IEEE Trans. Software Eng, 23 (5), pp. 279-295. , May
  • Hussain, A., Huth, M., On Model Checking Multiple Hybrid Views (2004) Proc. First Int'l Symp. Leveraging Applications of Formal Methods, pp. 235-242
  • Hussain, A., Huth, M., Automata Games for Multiple-Model Checking (2006) Electronic Notes in Theoretical Computer Science, 115, pp. 401-421
  • Huth, M., Jagadeesan, R., Schmidt, D., A Domain Equation for Refinement of Partial Systems (2004) Math. Structures in Computer Science, 14 (4), pp. 469-505
  • Huth, M., Jagadeesan, R., Schmidt, D.A., Modal Transition Systems: A Foundation for Three-Valued Program Analysis (2001) Proc. European Symp. Programming, pp. 155-169
  • (2000) Recommendation z.120: Message Sequence Charts, , ITU, ITU
  • Kazhamiakin, R., Pistore, M., Roveri, M., Formal Verification of Requirements Using SPIN: A Case Study on Web Services (2004) Proc. Int'l Conf. Software Eng. and Formal Methods, pp. 406-415
  • Kleene, S.C., (1952) Introduction to Metamathematics, , Van Nostrand
  • Koskimies, K., MLkinen, E., Automatic Synthesis of State Machines from Trace Diagrams (1994) Software Practice and Experience, 24 (7), pp. 643-658
  • Kramer, J., Magee, J., Sloman, M., CONIC: An Integrated Approach to Distributed Computer Control Systems (1983) Proc. IEE, 130 (1), pp. 1-10
  • Krüger, I., Grosu, R., Scholz, P., Broy, M., From MSCs to Statecharts (1999) Distributed and Parallel Embedded Systems, , Kluwer Academic Publishers
  • De Landtsheer, R., Letier, E., van Lamsweerde, A., Deriving Tabular Event-Based Specifications from Goal-Oriented Requirements Models (2003) Proc. IEEE Int'l Symp. Requirements Eng, pp. 200-212
  • Larsen, K., Steffen, B., Weise, C., The Methodology of Modal Constraints (1996) Formal Systems Specification, pp. 405-435. , Springer
  • Larsen, K., Xinxin, L., Equation Solving Using Modal Transition Systems (1990) Proc. Fifth Ann. Symp. Logic in Computer Science, pp. 108-117. , July
  • Larsen, K.G., Nyman, U., Wasowski, A., Modal I/O Automata for Interface and Product Line Theories (2007) Proc. European Symp. Programming
  • Larsen, K.G., Steffen, B., Weise, C., A Constraint Oriented Proof Methodology based on Modal Transition Systems (1995) Proc. First Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems, pp. 17-40
  • Larsen, K.G., Thomsen, B., A Modal Process Logic (1988) Proc. IEEE Symp. Logic in Computer Science, pp. 203-210
  • Letier, E., Kramer, J., Magee, J., Uchitel, S., Fluent Temporal Logic for Discrete-Time Event-Based Models (2005) Proc. ACM SIGSOFT Symp. Foundations of Software Eng, pp. 70-79
  • Letier, E., Kramer, J., Magee, J., Uchitel, S., Deriving Event-Based Transition Systems from Goal-Oriented Requirements Models, (2006), Technical Report 02/2006, Imperial College; Letier, E., van Lamsweerde, A., Deriving Operational Software Specifications from System Goals (2002) Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng, pp. 119-128
  • Lichtenstein, O., Pnueli, A., Checking that Finite State Concurrent Programs Satisfy Their Linear Specification (1985) Proc. 12th Ann. ACM Symp. Principles of Programming Languages, pp. 97-107
  • Magee, J., Kramer, J., (1999) Concurrency - State Models and Java Programs, , John Wiley
  • Magee, J., Pryce, N., Giannakopoulou, D., Kramer, J., Graphical Animation of Behavior Models (2000) Proc. Int'l Conf. Software Eng, pp. 499-508
  • Manna, Z., Pnueli, A., Verification of Concurrent Programs: A Temporal Proof System, (1983) technical report, , Dept. of Computer Science, Stanford Univ
  • Ponsard, C., Massonet, P., Rifaut, A., Molderez, J.F., van Lamsweerde, A., Tran Van, H., Early Verification and Validation of Mission-Critical Systems (2004) Proc. Workshop Formal Methods in Critical Systems
  • Roscoe, A.W., Hoare, C.A.R., Bird, R., (1997) The Theory and Practice of Concurrency, , Prentice-Hall
  • Sun, J., Song Dong, J., Design Synthesis from Interaction and State-Based Specifications (2006) IEEE Trans. Software Eng, 32 (6), pp. 349-364. , June
  • Sutcliffe, A.G., Maiden, N.A.M., Minocha, S., Manuel, D., Supporting Scenario-Based Requirements Engineering (1998) IEEE Trans. Software Eng, 24 (12), pp. 1072-1088. , Dec
  • Uchitel, S., Brunet, G., Chechik, M., Behaviour Model Synthesis from Properties and Scenarios (2007) Proc. Int'l Conf. Software Eng, pp. 34-43
  • Uchitel, S., Chechik, M., Merging Partial Behavioural Models (2004) Proc. ACM SIGSOFT Int'l Symp. Foundations of Software Eng, pp. 43-52
  • Uchitel, S., Kramer, J., Magee, J., Incremental Elaboration of Scenario-Based Specifications and Behaviour Models using Implied Scenarios (2004) ACM Trans. Software Eng. and Methodology, 13 (1)
  • Tran Van, H., van Lamsweerde, A., Massonet, P., Ponsard, C.H., Goal-Oriented Requirements Animation (2004) Proc. IEEE Int'l Symp. Requirements Eng, pp. 218-228
  • van Lamsweerde, A., Tutorial: Goal-Oriented Requirements Engineering: From System Objectives to UML Models to Precise Software Specifications (2003) Proc. Int'l Conf. Software Eng, pp. 744-745
  • van Lamsweerde, A., Letier, E., Handling Obstacles in Goal-Oriented Requirements Engineering (2000) IEEE Trans. Software Eng, 26 (10), pp. 978-1005. , Oct
  • Vardi, M.Y., Wolper, P., An Automata-Theoretic Approach to Automatic Program Verification (1986) Proc. First Symp. Logic in Computer Science, pp. 322-331

Citas:

---------- APA ----------
Uchitel, S., Brunet, G. & Chechik, M. (2009) . Synthesis of partial behavior models from properties and scenarios. IEEE Transactions on Software Engineering, 35(3), 384-406.
http://dx.doi.org/10.1109/TSE.2008.107
---------- CHICAGO ----------
Uchitel, S., Brunet, G., Chechik, M. "Synthesis of partial behavior models from properties and scenarios" . IEEE Transactions on Software Engineering 35, no. 3 (2009) : 384-406.
http://dx.doi.org/10.1109/TSE.2008.107
---------- MLA ----------
Uchitel, S., Brunet, G., Chechik, M. "Synthesis of partial behavior models from properties and scenarios" . IEEE Transactions on Software Engineering, vol. 35, no. 3, 2009, pp. 384-406.
http://dx.doi.org/10.1109/TSE.2008.107
---------- VANCOUVER ----------
Uchitel, S., Brunet, G., Chechik, M. Synthesis of partial behavior models from properties and scenarios. IEEE Trans Software Eng. 2009;35(3):384-406.
http://dx.doi.org/10.1109/TSE.2008.107