Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
SICS Software-Intensive Cyber-Physical Systems
Erschienen in: SICS Software-Intensive Cyber-Physical Systems 4/2013

01.11.2013 | Special Issue Paper

Supporting incremental behaviour model elaboration

verfasst von: Sebastian Uchitel, Dalal Alrajeh, Shoham Ben-David, Victor Braberman, Marsha Chechik, Guido De Caso, Nicolas D’Ippolito, Dario Fischbein, Diego Garbervetsky, Jeff Kramer, Alessandra Russo, German Sibay

Erschienen in: SICS Software-Intensive Cyber-Physical Systems | Ausgabe 4/2013

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel A journey through SMScom: self-managing situational computing
Nächster Artikel From software verification to ‘everyware’ verification

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Computer Science - Research and Development

Computer Science – Research and Development (CSRD), formerly Informatik – Forschung und Entwicklung (IFE), is a quarterly international journal that publishes high-quality research and survey papers from the Software Engineering & Systems area.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Weitere Produktempfehlungen anzeigen
Literatur
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–15
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–275
4.
Alrajeh D, Ray O, Russo A, Uchitel S (2009) Using abduction and induction for operational requirements elaboration. J Appl Log 7(3):275–288 MathSciNetCrossRefMATH
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–4):217–241 CrossRefMATH
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–393
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–25 MathSciNetCrossRef
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 “correct” 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’94, pp 596–602
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–47. (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’01 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–150 CrossRef
16.
Chatterjee K, Henzinger TA, Jobstmann B (2008) Environment assumptions for synthesis. In: Proceedings of the 19th international conference on concurrency theory, CONCUR ’08. Springer, Berlin, pp 147–161 CrossRef
17.
Chechik M, Devereux B, Easterbrook S, Gurfinkel A (2003) Multi-valued symbolic model-checking. ACM Trans Softw Eng Methodol 12(4):371–408 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’07. Springer, Berlin, pp 352–367 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–291 CrossRef
21.
Dardenne A, van Lamsweerde A, Fickas S (1993) Goal-directed requirements acquisition. Sci Comput Program 20(1):3–50 CrossRefMATH
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–190 CrossRef
23.
de Alfaro L, Henzinger TA (2001) Interface automata. Softw Eng Notes 26(5):109–120 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–390
25.
de Caso G, Braberman VA, Garbervetsky D, Uchitel S (2012) Automated abstractions for contract validation. IEEE Trans Softw Eng 38(1):141–162 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’Ippolito N, Fischbein D, Chechik M, Uchitel S (2008) Mtsa: the modal transition system analyser. In: ASE. IEEE Press, New York, pp 475–476
28.
D’Ippolito 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–220
29.
D’Ippolito 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.
31.
Feather MS, Cornford SL (2003) Quantitative risk-based requirements reasoning. Requir Eng 8:248–265 CrossRef
32.
Finkelstein A (1996) The London ambulance system case study. In: Proc of 8th intl work on software specification and design, pp 5–19
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–307
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–230
36.
Fischbein D, D’Ippolito 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–4):335–350 MathSciNet
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–1080
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’03). ACM, New York, pp 257–266
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’04), Barcelona, Spain. LNCS, vol 2988. Springer, Berlin, pp 451–466 CrossRef
42.
Harel D (2003) Come, let’s play—scenario-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–127 CrossRef
44.
Hoare CAR (1985) Communicating sequential processes. Prentice Hall, New York MATH
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—a 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’95. ACM, New York, pp 283–292
49.
Keller R (1976) Formal verification of parallel programs. Commun ACM 19(7):371–384 CrossRefMATH
50.
Kowalski RA, Sergot M (1986) A logic-based calculus of events. New Gener Comput 4(1):67–95 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.
53.
Larsen KG, Thomsen B (1988) A modal process logic. In: Proceedings of 3rd annual symposium on logic in computer science (LICS’88). IEEE Comput Soc, Los Alamitos, pp 203–210
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’90). IEEE Comput Soc, Los Alamitos, pp 108–117 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’95). LNCS. Springer, Berlin, pp 13–28
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–128
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–206 CrossRef
58.
Parnas DL, Madey J (1995) Functional documents for computer systems. Sci Comput Program 25:41–61 CrossRef
59.
Meyer B (1992) Applying ‘design by contract’. Computer 25:40–51 CrossRef
60.
Milner R (1989) Communication and concurrency. Prentice-Hall, New York MATH
61.
Piterman N, Pnueli A, Sa’ar Y (2006) Synthesis of reactive (1) designs. Lect Notes Comput Sci 3855:364–380 MathSciNetCrossRef
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–190 CrossRef
63.
Pressman RS (2010) Software engineering: a practitioner’s approach, 7th edn. McGraw-Hill, New York
64.
Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81–98 CrossRef
65.
Rosenblum DS (1995) A practical approach to programming with assertions. IEEE Trans Softw Eng 21(1):19–31 CrossRef
66.
Sassolas M, Chechik M, Uchitel S (2011) Exploring inconsistencies between modal transition systems. Softw Syst Model 10(1):117–142 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–50 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–21 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–52
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–27
71.
Uchitel S, Brunet G, Chechik M (2007) Behaviour model synthesis from properties and scenarios. In: ICSE. IEEE Comput Soc, Los Alamitos, pp 34–43
72.
Uchitel S, Brunet G, Chechik M (2009) Synthesis of partial behavior models from properties and scenarios. IEEE Trans Softw Eng 35(3):384–406 CrossRef
73.
van Gabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3):555–600 MathSciNetCrossRef
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–1005 CrossRef
77.
Van HT, van Lamsweerde A, Massonet P, Ponsard C (2004) Goal-oriented requirements animation. In: Requirements engineering conference, 2004, pp 218–228
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 ’11. ACM, New York, pp 44–47 CrossRef
Metadaten
Titel
Supporting incremental behaviour model elaboration
verfasst von
Sebastian Uchitel
Dalal Alrajeh
Shoham Ben-David
Victor Braberman
Marsha Chechik
Guido De Caso
Nicolas D’Ippolito
Dario Fischbein
Diego Garbervetsky
Jeff Kramer
Alessandra Russo
German Sibay
Publikationsdatum
01.11.2013
Verlag
Springer Berlin Heidelberg
Erschienen in
SICS Software-Intensive Cyber-Physical Systems / Ausgabe 4/2013
Print ISSN: 2524-8510
Elektronische ISSN: 2524-8529
DOI
https://doi.org/10.1007/s00450-012-0233-1

Weitere Artikel der Ausgabe 4/2013

SICS Software-Intensive Cyber-Physical Systems 4/2013 Zur Ausgabe

Special Issue Paper

A journey through SMScom: self-managing situational computing

Editorial

ERC grants

Editorial

Rigorous software engineering

Special Issue Paper

Quantitative reactive modeling and verification

Special Issue Paper

From software verification to ‘everyware’ verification

Special Issue Paper

Requirements-driven software evolution

Premium Partner

    Bildnachweise