Supporting incremental behaviour model elaboration

详细信息    查看全文

• 作者：Sebastian Uchitel (1) (2)
  Dalal Alrajeh (1)
  Shoham Ben-David (3)
  Victor Braberman (2)
  Marsha Chechik (3)
  Guido De Caso (2)
  Nicolas D鈥橧ppolito (1)
  Dario Fischbein (1)
  Diego Garbervetsky (2)
  Jeff Kramer (1)
  Alessandra Russo (1)
  German Sibay (1)
  
• 关键词：Partial behaviour modelling
• 刊名：Computer Science - Research and Development
• 出版年：2013
• 出版时间：November 2013
• 年：2013
• 卷：28
• 期：4
• 页码：279-293
• 全文大小：801KB
• 参考文献：1. Alexander聽I, Maiden聽N (2004) Scenarios, stories, use cases: through the systems development life-cycle. Wiley, New York
  2. Alrajeh聽D, Russo聽A, Uchitel聽S (2008) Deriving non-zeno behavior models from goal models using ilp. In: Fiadeiro JL, Inverardi聽P (eds) FASE. Lecture notes in computer science, vol 4961. Springer, Berlin, pp 1鈥?5
  3. Alrajeh聽D, Kramer聽J, Russo聽A, Uchitel聽S (2009) Learning operational requirements from goal models. In: Proc of 31st intl conf on softw eng, pp 265鈥?75
  4. Alrajeh聽D, Ray聽O, Russo聽A, Uchitel聽S (2009) Using abduction and induction for operational requirements elaboration. J Appl Log 7(3):275鈥?88 CrossRef
  5. Alrajeh聽D, Kramer聽J, Russo聽A, Uchitel聽S (2010) Deriving non-zeno behaviour models from goal models using ilp. Form Asp Comput 22(3鈥?):217鈥?41 CrossRef
  6. Alrajeh聽D, Kramer聽J, Russo聽A, Uchitel聽S (2012) Learning from vacuously satisfiable scenario-based specifications. In: de Lara聽J, Zisman聽A (eds) FASE. Lecture notes in computer science, vol 7212. Springer, Berlin, pp 377鈥?93
  7. Alrajeh聽D, Kramer聽J, van Lamsweerde聽A, Russo聽A, Uchitel聽S (2012) Generating obstacle conditions for requirements completeness. In: Proc of 34th intl conf on softw eng
  8. Alur聽R, La Torre聽S (2004) Deterministic generators and games for LTL fragments. ACM Trans Comput Log 5(1):1鈥?5 CrossRef
  9. Asarin聽E, Maler聽O, Pnueli聽A, Sifakis聽J (1998) Controller synthesis for timed automata. In: Proceedings of the IFAC symposium on system structure and control
  10. Autili聽M, Inverardi聽P, Tivoli聽M, Garlan聽D (2004) Synthesis of 鈥渃orrect鈥?adaptors for protocol enhancement in component-based systems. In: SAVCBS 2004 specification and verification of component-based systems, p 79
  11. Beatty聽D, Bryant聽R (1994) Formally verifying a microprocessor using a simulation methodology. In: Proceedings of design automation conference鈥?4, pp 596鈥?02
  12. Ben-David聽S, Chechik聽M, Gurfinkel聽A, Uchitel聽S (2011) CSSL: a logic for specifying conditional scenarios. In: Gyim贸thy聽T, Zeller聽A (eds) SIGSOFT FSE. ACM, New York, pp 37鈥?7. (Acceptance rate: 16聽%. Scopus)
  13. Bertoli聽P, Pistore聽M (2004) Planning with extended goals and partial observability. In: Proceedings of ICAPS, vol 4
  14. Bertoli聽P, Cimatti聽A, Pistore聽M, Roveri聽M, Traverso聽P (2001) MBP: a聽model based planner. In: Proceedings of the IJCAI鈥?1 workshop on planning under uncertainty and incomplete information
  15. Bertolino聽A, Inverardi聽P, Pelliccione聽P, Tivoli聽M (2009) Automatic synthesis of behavior protocols for composable web-services. In: 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. ACM, New York, pp 141鈥?50 CrossRef
  16. Chatterjee聽K, Henzinger TA, Jobstmann聽B (2008) Environment assumptions for synthesis. In: Proceedings of the 19th international conference on concurrency theory, CONCUR 鈥?8. Springer, Berlin, pp 147鈥?61 CrossRef
  17. Chechik聽M, Devereux聽B, Easterbrook聽S, Gurfinkel聽A (2003) Multi-valued symbolic model-checking. ACM Trans Softw Eng Methodol 12(4):371鈥?08 CrossRef
  18. Chechik聽M, Gheorghiu聽M, Gurfinkel聽A (2007) Finding environment guarantees. In: Proceedings of the 10th international conference on fundamental approaches to software engineering, FASE鈥?7. Springer, Berlin, pp 352鈥?67 CrossRef
  19. Clarke聽E, Grumberg聽O, Peled聽D (1999) Model checking. MIT Press, Cambridge
  20. Dams聽D, Gerth聽R, Grumberg聽O (1997) Abstract interpretation of reactive systems. ACM Trans Program Lang Syst 2(19):253鈥?91 CrossRef
  21. Dardenne聽A, van Lamsweerde聽A, Fickas聽S (1993) Goal-directed requirements acquisition. Sci Comput Program 20(1):3鈥?0 CrossRef
  22. Darimont聽R, van Lamsweerde聽A (1996) Formal refinement patterns for goal-driven requirements elaboration. In: Proc of 4th ACM SIGSOFT symposium on foundations of softw eng, pp 179鈥?90 CrossRef
  23. de Alfaro聽L, Henzinger TA (2001) Interface automata. Softw Eng Notes 26(5):109鈥?20 CrossRef
  24. de Caso聽G, Braberman VA, Garbervetsky聽D, Uchitel聽S (2011) Program abstractions for behaviour validation. In: Taylor RN, Gall聽H, Medvidovic聽N (eds) ICSE. ACM, New York, pp 381鈥?90
  25. de Caso聽G, Braberman VA, Garbervetsky聽D, Uchitel聽S (2012) Automated abstractions for contract validation. IEEE Trans Softw Eng 38(1):141鈥?62 CrossRef
  26. DeLine聽R, Fahndrich聽M (2004) Typestates for objects. In: Ecoop 2004-object-oriented programming: 18th European conference: proceedings, Oslo, Norway, June, 2004.
  27. D鈥橧ppolito聽N, Fischbein聽D, Chechik聽M, Uchitel S (2008) Mtsa: the modal transition system analyser. In: ASE. IEEE Press, New York, pp 475鈥?76
  28. D鈥橧ppolito聽N, Braberman VA, Piterman聽N, Uchitel聽S (2011) Synthesis of live behaviour models for fallible domains. In: Taylor RN, Gall聽H, Medvidovic聽N (eds) ICSE. ACM, New York, pp 211鈥?20
  29. D鈥橧ppolito聽N, Braberman聽V, Piterman聽N, Uchitel聽S (2013) Synthesising non-anomalous event-based controllers for liveness goals. ACM Trans Softw Eng Methodol 22(1)
  30. D鈥橧ppolito聽N, Braberman聽V, Piterman聽N, Uchitel聽S (2012) The modal transition system control problem. Lect Notes Comput Sci. doi:10.1007/978-3-642-32759-9_15
  31. Feather MS, Cornford SL (2003) Quantitative risk-based requirements reasoning. Requir Eng 8:248鈥?65 CrossRef
  32. Finkelstein聽A (1996) The London ambulance system case study. In: Proc of 8th intl work on software specification and design, pp聽5鈥?9
  33. Fischbein聽D (2012) Foundations for behavioural model elaboration using modal transition systems. PhD thesis, Imperial College, London, UK
  34. Fischbein聽D, Uchitel聽S (2008) On correct and complete strong merging of partial behaviour models. In: Harrold MJ, Murphy GC (eds) SIGSOFT FSE. ACM, New York, pp 297鈥?07
  35. Fischbein聽D, Braberman VA, Uchitel聽S (2009) A聽sound observational semantics for modal transition systems. In: Leucker聽M, Morgan聽C (eds) ICTAC. Lecture notes in computer science, vol聽5684. Springer, Berlin, pp 215鈥?30
  36. Fischbein聽D, D鈥橧ppolito聽N, Brunet聽G, Chechik聽M, Uchitel聽S (2012) Weak alphabet merging of partial behavior models. ACM Trans Softw Eng Methodol 21(2):9 CrossRef
  37. Fitting聽M (1991) Many-valued modal logics. Fundam Inform 15(3鈥?):335鈥?50
  38. Gelfond聽M, Lifschitz聽V (1988) The stable model semantics for logic programming. In: Kowalski RA, Bowen聽K (eds) Proc of 5th int conference on logic programming, pp 1070鈥?080
  39. Giannakopoulou聽D, Magee聽J (2003) Fluent model checking for event-based systems. In: Proceedings of the 9th joint meeting of the European software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering (ESEC/FSE鈥?3). ACM, New York, pp 257鈥?66
  40. Grieskamp聽W, Kicillof聽N, Stobie聽K, Braberman聽V (2011) Model-based quality assurance of protocol documentation: tools and methodology. Soft Test Verif Reliab. doi:10.1002/stvr.427
  41. Gurfinkel聽A, Chechik聽M (2004) How vacuous is vacuous? In: Proceedings of 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS鈥?4), Barcelona, Spain. LNCS, vol 2988. Springer, Berlin, pp 451鈥?66 CrossRef
  42. Harel聽D (2003) Come, let鈥檚 play鈥攕cenario-based programming using LSCs and the play-engine. Springer, Berlin CrossRef
  43. Heaven聽W, Sykes聽D, Magee聽J, Kramer聽J (2009) A聽case study in goal-driven architectural adaptation. In: Software engineering for self-adaptive systems. Springer, Berlin, pp 109鈥?27 CrossRef
  44. Hoare CAR (1985) Communicating sequential processes. Prentice Hall, New York
  45. IEEE (1990) IEEE standard glossary of software engineering terminology
  46. ITU (2000) Message sequence charts. Technical report recommendation Z.120, International Telecommunications Union, Telecommunication Standardisation Sector
  47. Jackson聽M (1995) Software requirements & specifications鈥攁聽lexicon of practice, principles and prejudices. Addison-Wesley, Reading
  48. Jackson聽M (1995) The world and the machine. In: Proceedings of the 17th international conference on software engineering, ICSE鈥?5. ACM, New York, pp 283鈥?92
  49. Keller聽R (1976) Formal verification of parallel programs. Commun ACM 19(7):371鈥?84 CrossRef
  50. Kowalski RA, Sergot聽M (1986) A聽logic-based calculus of events. New Gener Comput 4(1):67鈥?5 CrossRef
  51. Kramer聽J, Magee聽J, Sloman聽M (1983) Conic: an integrated approach to distributed computer control systems. In: IEE proc, part聽E, vol 130
  52. Kripke SA (1963) Semantical considerations on modal logic. Acta Philos Fenn 16:83鈥?4
  53. Larsen KG, Thomsen聽B (1988) A聽modal process logic. In: Proceedings of 3rd annual symposium on logic in computer science (LICS鈥?8). IEEE Comput Soc, Los Alamitos, pp 203鈥?10
  54. Larsen聽K, Xinxin聽L (1990) Equation solving using modal transition systems. In: Proceedings of the 5th annual IEEE symposium on logic in computer science (LICS鈥?0). IEEE Comput Soc, Los Alamitos, pp 108鈥?17 CrossRef
  55. Larsen KG, Steffen聽B, Weise聽C (1995) A聽constraint oriented proof methodology based on modal transition systems. In: Tools and algorithms for construction and analysis of systems (TACAS鈥?5). LNCS. Springer, Berlin, pp 13鈥?8
  56. Letier聽E, Van Lamsweerde聽A (2002) Deriving operational software specifications from system goals. In: Proc of 10th ACM SIGSOFT symposium on foundations of software engineering, pp 119鈥?28
  57. Letier聽E, Kramer聽J, Magee聽J, Uchitel聽S (2008) Deriving event-based transition systems from goal-oriented requirements models. Autom Softw Eng 15(2):175鈥?06 CrossRef
  58. Parnas DL, Madey聽J (1995) Functional documents for computer systems. Sci Comput Program 25:41鈥?1 CrossRef
  59. Meyer聽B (1992) Applying 鈥榙esign by contract鈥? Computer 25:40鈥?1 CrossRef
  60. Milner聽R (1989) Communication and concurrency. Prentice-Hall, New York
  61. Piterman聽N, Pnueli聽A, Sa鈥檃r聽Y (2006) Synthesis of reactive (1) designs. Lect Notes Comput Sci 3855:364鈥?80 CrossRef
  62. Pnueli聽A, Rosner聽R (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 179鈥?90 CrossRef
  63. Pressman RS (2010) Software engineering: a聽practitioner鈥檚 approach, 7th edn. McGraw-Hill, New York
  64. Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81鈥?8 CrossRef
  65. Rosenblum DS (1995) A聽practical approach to programming with assertions. IEEE Trans Softw Eng 21(1):19鈥?1 CrossRef
  66. Sassolas聽M, Chechik聽M, Uchitel聽S (2011) Exploring inconsistencies between modal transition systems. Softw Syst Model 10(1):117鈥?42 CrossRef
  67. Sibay聽G, Uchitel聽S, Braberman VA (2008) Existential live sequence charts revisited. In: Sch盲fer聽W, Dwyer MB, Gruhn聽V (eds) ICSE. ACM, New York, pp 41鈥?0 CrossRef
  68. Sykes聽D, Heaven聽W, Magee聽J, Kramer聽J (2007) Plan-directed architectural change for autonomous systems. In: Poetzsch-Heffter聽A (ed) SAVCBS. ACM, New York, pp 15鈥?1 CrossRef
  69. Uchitel聽S, Chechik聽M (2004) Merging partial behavioural models. In: Proceedings of 12th ACM SIGSOFT international symposium on foundations of software engineering, pp 43鈥?2
  70. Uchitel聽S, Kramer聽J, Magee聽J (2003) Behaviour model elaboration using partial labelled transition systems. In: ESEC/SIGSOFT FSE. ACM, New York, pp 19鈥?7
  71. Uchitel聽S, Brunet聽G, Chechik聽M (2007) Behaviour model synthesis from properties and scenarios. In: ICSE. IEEE Comput Soc, Los Alamitos, pp 34鈥?3
  72. Uchitel聽S, Brunet聽G, Chechik聽M (2009) Synthesis of partial behavior models from properties and scenarios. IEEE Trans Softw Eng 35(3):384鈥?06 CrossRef
  73. van Gabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3):555鈥?00 CrossRef
  74. van Lamsweerde聽A (2001) Goal-oriented requirements engineering: a聽guided tour. In: Proceedings of the fifth IEEE international symposium on requirements engineering. IEEE Comput Soc, Washington
  75. van Lamsweerde聽A (2009) Requirements engineering: from system goals to UML models to software specifications. Wiley, New York
  76. van Lamsweerde聽A, Letier聽E (2000) Handling obstacles in goal-oriented requirements engineering. IEEE Trans Softw Eng 26:978鈥?005 CrossRef
  77. Van HT, van Lamsweerde聽A, Massonet聽P, Ponsard聽C (2004) Goal-oriented requirements animation. In: Requirements engineering conference, 2004, pp 218鈥?28
  78. Zoppi聽E, Braberman聽V, de Caso聽G, Garbervetsky聽D, Uchitel聽S (2011) Contractor.net: inferring typestate properties to enrich code contracts. In: Proceedings of the 1st workshop on developing tools as Plug-ins, TOPI 鈥?1. ACM, New York, pp 44鈥?7 CrossRef
  
• 作者单位：Sebastian Uchitel (1) (2)
  Dalal Alrajeh (1)
  Shoham Ben-David (3)
  Victor Braberman (2)
  Marsha Chechik (3)
  Guido De Caso (2)
  Nicolas D鈥橧ppolito (1)
  Dario Fischbein (1)
  Diego Garbervetsky (2)
  Jeff Kramer (1)
  Alessandra Russo (1)
  German Sibay (1)
  
  1. Imperial College London, London, UK
  2. FCEN, Universidad de Buenos Aires, Buenos Aires, Argentina
  3. University of Toronto, Toronto, Canada
  
• ISSN：1865-2042

文摘

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 鈥淧artial Behaviour Modelling鈥擣oundations 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.