Artículo

Uchitel, S.; Alrajeh, D.; Ben-David, S.; Braberman, V.; Chechik, M.; De Caso, G.; D'Ippolito, N.; Fischbein, D.; Garbervetsky, D.; Kramer, J.; Russo, A.; Sibay, G. "Supporting incremental behaviour model elaboration" (2013) Computer Science - Research and Development. 28(4):279-293
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Behaviour model construction remains a difficult and labour intensive task which hinders the adoption of model-based methods by practitioners. We believe one reason for this is the mismatch between traditional approaches and current software development process best practices which include iterative development, adoption of use-case and scenario-based techniques and viewpoint- or stakeholder-based analysis; practices which require modelling and analysis in the presence of partial information about system behaviour. Our objective is to address the limitations of behaviour modelling and analysis by shifting the focus from traditional behaviour models and verification techniques that require full behaviour information to partial behaviour models and analysis techniques, that drive model elaboration rather than asserting adequacy. We aim to develop sound theory, techniques and tools that facilitate the construction of partial behaviour models through model synthesis, enable partial behaviour model analysis and provide feedback that prompts incremental elaboration of partial models. In this paper we present how the different research threads that we have and currently are developing help pursue this vision as part of the "Partial Behaviour Modelling - Foundations for Iterative Model Based Software Engineering" Starting Grant funded by the ERC. We cover partial behaviour modelling theory and construction, controller synthesis, automated diagnosis and refinement, and behaviour validation. © 2012 Springer-Verlag Berlin Heidelberg.

Registro:

Documento: Artículo
Título:Supporting incremental behaviour model elaboration
Autor:Uchitel, S.; Alrajeh, D.; Ben-David, S.; Braberman, V.; Chechik, M.; De Caso, G.; D'Ippolito, N.; Fischbein, D.; Garbervetsky, D.; Kramer, J.; Russo, A.; Sibay, G.
Filiación:Imperial College London, London, United Kingdom
FCEN, Universidad de Buenos Aires, Buenos Aires, Argentina
University of Toronto, Toronto, Canada
Palabras clave:Partial behaviour modelling; Behaviour modelling; Controller synthesis; Iterative development; Modelling and analysis; Software development process; Techniques and tools; Traditional approaches; Verification techniques; Software engineering; Iterative methods
Año:2013
Volumen:28
Número:4
Página de inicio:279
Página de fin:293
DOI: http://dx.doi.org/10.1007/s00450-012-0233-1
Título revista:Computer Science - Research and Development
Título revista abreviado:Comput. Sci. Res. Devel. Dev.
ISSN:18652034
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_18652034_v28_n4_p279_Uchitel

Referencias:

  • Alexander, I., Maiden, N., (2004) Scenarios, Stories, Use Cases: Through the Systems Development Life-cycle, , Wiley New York
  • Alrajeh, D., Russo, A., Uchitel, S., Deriving non-zeno behavior models from goal models using ilp (2008) FASE, pp. 1-15. , J.L. Fiadeiro Inverardi (eds) Lecture notes in computer science 4961 Springer Berlin
  • Alrajeh, D., Kramer, J., Russo, A., Uchitel, S., Learning operational requirements from goal models (2009) Proc of 31st Intl Conf on Softw Eng, pp. 265-275
  • Alrajeh, D., Ray, O., Russo, A., Uchitel, S., Using abduction and induction for operational requirements elaboration (2009) J Appl Log, 7 (3), pp. 275-288. , 2528926 10.1016/j.jal.2008.10.002
  • Alrajeh, D., Kramer, J., Russo, A., Uchitel, S., Deriving non-zeno behaviour models from goal models using ilp (2010) Form Asp Comput, 22 (3-4), pp. 217-241. , 10.1007/s00165-009-0128-5
  • Alrajeh, D., Kramer, J., Russo, A., Uchitel, S., Learning from vacuously satisfiable scenario-based specifications (2012) FASE, pp. 377-393. , J. de Lara A. Zisman (eds) Lecture notes in computer science 7212 Springer Berlin
  • Alrajeh, D., Kramer, J., Van Lamsweerde, A., Russo, A., Uchitel, S., Generating obstacle conditions for requirements completeness (2012) Proc of 34th Intl Conf on Softw Eng
  • Alur, R., La Torre, S., Deterministic generators and games for LTL fragments (2004) ACM Trans Comput Log, 5 (1), pp. 1-25. , 2023086 10.1145/963927.963928
  • Asarin, E., Maler, O., Pnueli, A., Sifakis, J., Controller synthesis for timed automata (1998) Proceedings of the IFAC Symposium on System Structure and Control
  • Autili, M., Inverardi, P., Tivoli, M., Garlan, D., Synthesis of "correct" adaptors for protocol enhancement in component-based systems (2004) SAVCBS 2004 Specification and Verification of Component-based Systems, p. 79
  • Beatty, D., Bryant, R., Formally verifying a microprocessor using a simulation methodology (1994) Proceedings of Design Automation conference'94, pp. 596-602
  • Ben-David, S., Chechik, M., Gurfinkel, A., Uchitel, S., CSSL: A logic for specifying conditional scenarios (2011) SIGSOFT FSE, pp. 37-47. , T. Gyimóthy A. Zeller (eds) ACM New York (Acceptance rate: 16 %. Scopus)
  • Bertoli, P., Pistore, M., Planning with extended goals and partial observability (2004) Proceedings of ICAPS, , 4
  • Bertoli, P., Cimatti, A., Pistore, M., Roveri, M., Traverso, P., MBP: A model based planner (2001) Proceedings of the IJCAI'01 Workshop on Planning under Uncertainty and Incomplete Information
  • Bertolino, A., Inverardi, P., Pelliccione, P., Tivoli, M., Automatic synthesis of behavior protocols for composable web-services (2009) Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering on European Software Engineering Conference and Foundations of Software Engineering Symposium, pp. 141-150. , ACM New York 10.1145/1595696.1595719
  • Chatterjee, K., Henzinger, T.A., Jobstmann, B., Environment assumptions for synthesis (2008) Proceedings of the 19th International Conference on Concurrency Theory, CONCUR '08, pp. 147-161. , Springer Berlin 10.1007/978-3-540-85361-9-14
  • Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A., Multi-valued symbolic model-checking (2003) ACM Trans Softw Eng Methodol, 12 (4), pp. 371-408. , 10.1145/990010.990011
  • Chechik, M., Gheorghiu, M., Gurfinkel, A., Finding environment guarantees (2007) Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering, FASE'07, pp. 352-367. , Springer Berlin 10.1007/978-3-540-71289-3-27
  • Clarke, E., Grumberg, O., Peled, D., (1999) Model Checking, , MIT Press Cambridge
  • Dams, D., Gerth, R., Grumberg, O., Abstract interpretation of reactive systems (1997) ACM Trans Program Lang Syst, 2 (19), pp. 253-291. , 10.1145/244795.244800
  • Dardenne, A., Van Lamsweerde, A., Fickas, S., Goal-directed requirements acquisition (1993) Sci Comput Program, 20 (1), pp. 3-50. , 10.1016/0167-6423(93)90021-G
  • Darimont, R., Van Lamsweerde, A., Formal refinement patterns for goal-driven requirements elaboration (1996) Proc of 4th ACM SIGSOFT Symposium on Foundations of Softw Eng, pp. 179-190. , 10.1145/239098.239131
  • De Alfaro, L., Henzinger, T.A., Interface automata (2001) Softw Eng Notes, 26 (5), pp. 109-120. , 10.1145/503271.503226
  • De Caso, G., Braberman, V.A., Garbervetsky, D., Uchitel, S., Program abstractions for behaviour validation (2011) ICSE, pp. 381-390. , R.N. Taylor H. Gall N. Medvidovic (eds) ACM New York
  • De Caso, G., Braberman, V.A., Garbervetsky, D., Uchitel, S., Automated abstractions for contract validation (2012) IEEE Trans Softw Eng, 38 (1), pp. 141-162. , 10.1109/TSE.2010.98
  • Deline, R., Fahndrich, M., Typestates for objects (2004) Ecoop 2004-object-oriented Programming: 18th European Conference: Proceedings, , Oslo, Norway June, 2004
  • D'Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S., Mtsa: The modal transition system analyser (2008) ASE, pp. 475-476. , IEEE Press New York
  • D'Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S., Synthesis of live behaviour models for fallible domains (2011) ICSE, pp. 211-220. , R.N. Taylor H. Gall N. Medvidovic (eds) ACM New York
  • D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., Synthesising non-anomalous event-based controllers for liveness goals (2013) ACM Trans Softw Eng Methodol, 22 (1)
  • D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., The modal transition system control problem (2012) Lect Notes Comput Sci, , 10.1007/978-3-642-32759-9-15
  • Feather, M.S., Cornford, S.L., Quantitative risk-based requirements reasoning (2003) Requir Eng, 8, pp. 248-265. , 10.1007/s00766-002-0160-y
  • Finkelstein, A., The London ambulance system case study (1996) Proc of 8th Intl Work on Software Specification and Design, pp. 5-19
  • Fischbein, D., (2012) Foundations for Behavioural Model Elaboration Using Modal Transition Systems, , PhD thesis, Imperial College, London, UK
  • Fischbein, D., Uchitel, S., On correct and complete strong merging of partial behaviour models (2008) SIGSOFT FSE, pp. 297-307. , M.J. Harrold G.C. Murphy (eds) ACM New York
  • Fischbein, D., Braberman, V.A., Uchitel, S., A sound observational semantics for modal transition systems (2009) ICTAC, pp. 215-230. , M. Leucker C. Morgan (eds) Lecture notes in computer science 5684 Springer Berlin
  • Fischbein, D., D'Ippolito, N., Brunet, G., Chechik, M., Uchitel, S., Weak alphabet merging of partial behavior models (2012) ACM Trans Softw Eng Methodol, 21 (2), p. 9. , 10.1145/2089116.2089119
  • Fitting, M., Many-valued modal logics (1991) Fundam Inform, 15 (3-4), pp. 335-350. , 1153298
  • Gelfond, M., Lifschitz, V., The stable model semantics for logic programming (1988) Proc of 5th Int Conference on Logic Programming, pp. 1070-1080. , R.A. Kowalski K. Bowen (eds)
  • Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'03), pp. 257-266. , ACM New York
  • Grieskamp, W., Kicillof, N., Stobie, K., Braberman, V., Model-based quality assurance of protocol documentation: Tools and methodology (2011) Soft Test Verif Reliab, , 10.1002/stvr.427
  • Gurfinkel, A., Chechik, M., How vacuous is vacuous? (2004) Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), pp. 451-466. , Barcelona, Spain LNCS 2988 Springer Berlin 10.1007/978-3-540-24730-2-34
  • Harel, D., (2003) Come, Let's Play - Scenario-based Programming Using LSCs and the Play-engine, , Springer Berlin 10.1007/978-3-642-19029-2
  • Heaven, W., Sykes, D., Magee, J., Kramer, J., A case study in goal-driven architectural adaptation (2009) Software Engineering for Self-adaptive Systems, pp. 109-127. , Springer Berlin 10.1007/978-3-642-02161-9-6
  • Hoare, C.A.R., (1985) Communicating Sequential Processes, , Prentice Hall New York
  • (1990) IEEE Standard Glossary of Software Engineering Terminology, , IEEE
  • (2000) Message Sequence Charts. Technical Report Recommendation Z.120, , ITU International Telecommunications Union, Telecommunication Standardisation Sector
  • Jackson, M., (1995) Software Requirements & Specifications - A Lexicon of Practice, Principles and Prejudices, , Addison-Wesley Reading
  • Jackson, M., The world and the machine (1995) Proceedings of the 17th International Conference on Software Engineering, ICSE'95, pp. 283-292. , ACM New York
  • Keller, R., Formal verification of parallel programs (1976) Commun ACM, 19 (7), pp. 371-384. , 10.1145/360248.360251
  • Kowalski, R.A., Sergot, M., A logic-based calculus of events (1986) New Gener Comput, 4 (1), pp. 67-95. , 10.1007/BF03037383
  • Kramer, J., Magee, J., Sloman, M., Conic: An integrated approach to distributed computer control systems (1983) IEe Proc, Part e, , 130
  • Kripke, S.A., Semantical considerations on modal logic (1963) Acta Philos Fenn, 16, pp. 83-94. , 170800
  • Larsen, K.G., Thomsen, B., A modal process logic (1988) Proceedings of 3rd Annual Symposium on Logic in Computer Science (LICS'88), pp. 203-210. , IEEE Comput Soc Los Alamitos
  • Larsen, K., Xinxin, L., Equation solving using modal transition systems (1990) Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS'90), pp. 108-117. , IEEE Comput Soc Los Alamitos 10.1109/LICS.1990.113738
  • Larsen, K.G., Steffen, B., Weise, C., A constraint oriented proof methodology based on modal transition systems (1995) Tools and Algorithms for Construction and Analysis of Systems (TACAS'95), pp. 13-28. , LNCS Springer Berlin
  • Letier, E., Van Lamsweerde, A., Deriving operational software specifications from system goals (2002) Proc of 10th ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 119-128
  • Letier, E., Kramer, J., Magee, J., Uchitel, S., Deriving event-based transition systems from goal-oriented requirements models (2008) Autom Softw Eng, 15 (2), pp. 175-206. , 10.1007/s10515-008-0027-7
  • Parnas, D.L., Madey, J., Functional documents for computer systems (1995) Sci Comput Program, 25, pp. 41-61. , 10.1016/0167-6423(95)96871-J
  • Meyer, B., Applying 'design by contract' (1992) Computer, 25, pp. 40-51. , 10.1109/2.161279
  • Milner, R., (1989) Communication and Concurrency, , Prentice-Hall New York
  • Piterman, N., Pnueli, A., Sa'Ar, Y., Synthesis of reactive (1) designs (2006) Lect Notes Comput Sci, 3855, pp. 364-380. , 2258798 10.1007/11609773-24
  • Pnueli, A., Rosner, R., On the synthesis of a reactive module (1989) Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179-190. , ACM New York 10.1145/75277.75293
  • Pressman, R.S., (2010) Software Engineering: A Practitioner's Approach, , 7 McGraw-Hill New York
  • Ramadge, P.J.G., Wonham, W.M., The control of discrete event systems (1989) Proc IEEE, 77 (1), pp. 81-98. , 10.1109/5.21072
  • Rosenblum, D.S., A practical approach to programming with assertions (1995) IEEE Trans Softw Eng, 21 (1), pp. 19-31. , 10.1109/32.341844
  • Sassolas, M., Chechik, M., Uchitel, S., Exploring inconsistencies between modal transition systems (2011) Softw Syst Model, 10 (1), pp. 117-142. , 10.1007/s10270-010-0148-x
  • Sibay, G., Uchitel, S., Braberman, V.A., Existential live sequence charts revisited (2008) ICSE, pp. 41-50. , W. Schäfer M.B. Dwyer V. Gruhn (eds) ACM New York 10.1145/1368088.1368095
  • Sykes, D., Heaven, W., Magee, J., Kramer, J., Plan-directed architectural change for autonomous systems (2007) SAVCBS, pp. 15-21. , A. Poetzsch-Heffter (eds) ACM New York 10.1145/1292316.1292318
  • Uchitel, S., Chechik, M., Merging partial behavioural models (2004) Proceedings of 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 43-52
  • Uchitel, S., Kramer, J., Magee, J., Behaviour model elaboration using partial labelled transition systems (2003) ESEC/SIGSOFT FSE, pp. 19-27. , ACM New York
  • Uchitel, S., Brunet, G., Chechik, M., Behaviour model synthesis from properties and scenarios (2007) ICSE, pp. 34-43. , IEEE Comput Soc Los Alamitos
  • Uchitel, S., Brunet, G., Chechik, M., Synthesis of partial behavior models from properties and scenarios (2009) IEEE Trans Softw Eng, 35 (3), pp. 384-406. , 10.1109/TSE.2008.107
  • Van Gabbeek, R.J., Weijland, W.P., Branching time and abstraction in bisimulation semantics (1996) J ACM, 43 (3), pp. 555-600. , 1408565 10.1145/233551.233556
  • Van Lamsweerde, A., Goal-oriented requirements engineering: A guided tour (2001) Proceedings of the Fifth IEEE International Symposium on Requirements Engineering, , IEEE Comput Soc Washington
  • Van Lamsweerde, A., (2009) Requirements Engineering: From System Goals to UML Models to Software Specifications, , Wiley New York
  • Van Lamsweerde, A., Letier, E., Handling obstacles in goal-oriented requirements engineering (2000) IEEE Trans Softw Eng, 26, pp. 978-1005. , 10.1109/32.879820
  • Van, H.T., Van Lamsweerde, A., Massonet, P., Ponsard, C., Goal-oriented requirements animation (2004) Requirements Engineering Conference, 2004, pp. 218-228
  • Zoppi, E., Braberman, V., De Caso, G., Garbervetsky, D., Uchitel, S., Contractor net: Inferring typestate properties to enrich code contracts (2011) Proceedings of the 1st Workshop on Developing Tools As Plug-ins, TOPI '11, pp. 44-47. , ACM New York 10.1145/1984708.1984721

Citas:

---------- APA ----------
Uchitel, S., Alrajeh, D., Ben-David, S., Braberman, V., Chechik, M., De Caso, G., D'Ippolito, N.,..., Sibay, G. (2013) . Supporting incremental behaviour model elaboration. Computer Science - Research and Development, 28(4), 279-293.
http://dx.doi.org/10.1007/s00450-012-0233-1
---------- CHICAGO ----------
Uchitel, S., Alrajeh, D., Ben-David, S., Braberman, V., Chechik, M., De Caso, G., et al. "Supporting incremental behaviour model elaboration" . Computer Science - Research and Development 28, no. 4 (2013) : 279-293.
http://dx.doi.org/10.1007/s00450-012-0233-1
---------- MLA ----------
Uchitel, S., Alrajeh, D., Ben-David, S., Braberman, V., Chechik, M., De Caso, G., et al. "Supporting incremental behaviour model elaboration" . Computer Science - Research and Development, vol. 28, no. 4, 2013, pp. 279-293.
http://dx.doi.org/10.1007/s00450-012-0233-1
---------- VANCOUVER ----------
Uchitel, S., Alrajeh, D., Ben-David, S., Braberman, V., Chechik, M., De Caso, G., et al. Supporting incremental behaviour model elaboration. Comput. Sci. Res. Devel. Dev. 2013;28(4):279-293.
http://dx.doi.org/10.1007/s00450-012-0233-1