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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling

04.10.2023 | Regular Paper

A formal component model for UML based on CSP aiming at compositional verification

verfasst von: Flávia Falcão, Lucas Lima, Augusto Sampaio, Pedro Antonino

Erschienen in: Software and Systems Modeling

Einloggen

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

search-config
loading …

Abstract

Model-based engineering emerged as an approach to tackle the complexity of current system development. In particular, compositional strategies assume that systems can be built from reusable and loosely coupled units. However, it is still a challenge to ensure that desired properties hold for component integration. We present a component-based model for UML, including a metamodel, well-formedness conditions and formal semantics via translation into BRIC; the presentation of the semantics is given by a set of rules that cover all the metamodel elements and map them to their respective BRIC denotations. We use our previous work on BRIC as an underlying (and totally hidden) component development framework so that our approach benefits from all the formal infrastructure developed for BRIC using CSP. Component composition, specified via UML structural diagrams, ensures adherence to classical concurrent properties: our focus is on the preservation of deadlock freedom. Automated support is developed as a plug-in to the Astah modelling tool. Verification is carried out using FDR (a model checker for CSP); we address scalability using compositional reasoning (inherent to the approach) and behavioural patterns. The formal reasoning is transparent to the user: a distinguishing feature of our approach is its support for traceability. For instance, when FDR uncovers a deadlock, a sequence diagram is constructed from the deadlock trace and presented to the user at the modelling level. The overall approach is illustrated with a running example and two additional case studies.

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

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

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
A is a set of values that parameterise the process P.
 
3
The symbol \(*\) means that FDR failed to provide an answer since it consumed the entire memory of the dedicated machine.
 
Literatur
1.
Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Upper Saddle River (2005)
2.
Oliveira, M.V.M., et al.: Rigorous development of component-based systems using component metadata and patterns. Formal Aspects Comput. 28(6), 937–1004 (2016)MathSciNetCrossRefMATH
3.
Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28, 626–643 (1996)CrossRef
4.
Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model-driven design. Sci. Comput. Program. 74(4), 168–196 (2009)MathSciNetCrossRefMATH
5.
Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Distrib. Comput. 25(5), 383–409 (2012)CrossRefMATH
6.
Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in bip. In: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, pp. 3–12. IEEE Computer Society, Washington, DC, USA (2006)
7.
Horváth, B., Guerra, E., Iovino, L. et al. : Model checking as a service: towards pragmatic hidden formal methods. In: Guerra, E., Iovino, L. (eds.) MODELS’20: ACM/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems. ACM (2020)
8.
9.
10.
Ramos, R., Sampaio, A., Mota, A.: Systematic development of trustworthy component systems. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009: Formal Methods, pp. 140–156. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)CrossRef
11.
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)
12.
Falcão, F., Lima, L., Sampaio, A.: Safe and Constructive Design with UML Components: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26-30, 2018, Proceedings, pp. 234–251. Springer (2018)
13.
14.
15.
Heineman, G.T., Councill, W.T. (eds.): Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley Longman Publishing Co., Boston (2001)
16.
Lau, K.-K., Wang, Z.: A survey of software component models. Tech. Rep., in Software Engineering and Advanced Applications. 31st EUROMICRO Conference: IEEE Computer Society (2005)
17.
18.
Selic, B.: A systematic approach to domain-specific language design using uml. In: 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC’07), pp. 2–9 (2007)
19.
20.
21.
22.
23.
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Fdr3: A modern refinement checker for csp. In: Abraham, E. & Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, vol. 8413 of Lecture Notes in Computer Science, pp. 187–201. Springer Berlin Heidelberg (2014)
24.
Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W., Merz, S., Pang, J.: Computing maximal bisimulations. In: Merz, S., Pang, J. (eds.) Formal Methods and Software Engineering, pp. 11–26. Springer, Cham (2014)CrossRef
25.
Sampaio, A., Nogueira, S., Mota, A., Isobe, Y.: Sound and mechanised compositional verification of input–output conformance. Softw. Test. Verif. Reliab. 24(4), 289–319 (2013)CrossRef
26.
27.
Martin, J.M.R.: The Design and Construction of Deadlock-Free Concurrent Systems. Ph.D. thesis, University of Buckingham (1996)
28.
Antonino, P.R.G., Sampaio, A., Woodcock, J.: A refinement based strategy for local deadlock analysis of networks of CSP processes. In: FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, Vol. 8442 of Lecture Notes in Computer Science, pp. 62–77. Springer (2014)
29.
Antonino, P.R., Oliveira, M.M., Sampaio, A.C., Kristensen, K.E., Bryans, J.W.: Leadership election: źan industrial sos application of compositional deadlock verification. In: Proceedings of the 6th International Symposium on NASA Formal Methods - vol. 8430. Springer, Berlin, Heidelberg (2014)
30.
31.
Grüninger, M., Menzel, C.: The process specification language (psl) theory and applications. AI Mag. 24, 63–74 (2003)
32.
Chen, Z., Morisset, C., Stolz, V.: Specification and validation of behavioural protocols in the rcos modeler. In: Arbab, F. (ed.) Proceedings of the Third IPM International Conference on Fundamentals of Software Engineering, FSEN’09, pp. 387–401. Springer, Berlin, Heidelberg (2010)
33.
Chehida, S., Baouya, A., Bensalem, S.: Component-based approach combining uml and bip for rigorous system design. In: Salaün, G., Wijs, A. (eds.) Formal Aspects of Component Software, pp. 27–43. Springer, Cham (2021)CrossRef
34.
Graics, B., Molnár, V., Vörös, A., Majzik, I., Varró, D.: Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw. Syst. Model. 19, 1–35 (2020)CrossRef
35.
Molnár, V., Graics, B., Vörös, A., Majzik, I., Varró, D.: The gamma statechart composition framework: Design, verification and code generation for component-based reactive systems. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings, ICSE ’18, pp. 113–116. Association for Computing Machinery, New York, NY, USA (2018)
36.
Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. Wiley, New York (1994)MATH
37.
Pereira, D.I.A., Oliveira, M.V.M., Silva, S.R.R.: Tool support for formal component-based development. Tech. Rep., Escola de Informática Teórica e Métodos Formais (ETMF 2016) (2016)
38.
Lima, L., et al.: An integrated semantics for reasoning about sysml design models using refinement. Softw. Syst. Model. 16(3), 875–902 (2017)CrossRef
39.
Gibson, C., Karban, R., Andolfato, L., Day, J.: Abstractions for executable and checkable fault management models. Procedia Comput. Sci. 28, 146–154 (2014). Conference on Systems Engineering Research
40.
Meyers, B., et al.: Promobox: a framework for generating domain-specific property languages. In: Combemale, B., Pearce, D.J., Barais, O., Vinju, J.J. (eds.) Software Language Engineering, pp. 1–20. Springer, Cham (2014)
41.
Ramos, R., Sampaio, A., Mota, A.: A semantics for uml-rt active classes via mapping into circus. In: Steffen, M., Zavattaro, G. (eds.) Formal Methods for Open Object-Based Distributed Systems, pp. 99–114. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)CrossRef
42.
Woodcock, J. et al.: Features of cml: A formal modelling language for systems of systems. In: 2012 7th International Conference on System of Systems Engineering (SoSE), pp. 1–6 (2012)
43.
Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, New York (2009)CrossRefMATH
44.
Cavalcanti, A., et al.: Modelling and verification for swarm robotics. In: Furia, C.A., Winter, K. (eds.) Integrated Formal Methods—14th International Conference, IFM 2018, vol. 11023, pp. 1–19 (2018)
45.
Conserva Filho, M., Oliveira, M., Sampaio, A., Cavalcanti, A.: Compositional and local livelock analysis for csp. Inf. Process. Lett. 133, 21–25 (2018)MathSciNetCrossRefMATH
46.
Otoni, R., Cavalcanti, A., Sampaio, A.: Local analysis of determinism for CSP. In: da Costa Cavalheiro, S.A., Fiadeiro, J.L. (eds.) Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, vol. 10623 of Lecture Notes in Computer Science, pp. 107–124. Springer (2017)
47.
Gorrieri, R., Versari, C.: Introduction to Concurrency Theory: Transition Systems and CCS, 1st edn. Springer, Cham (2015)CrossRefMATH
Metadaten
Titel
A formal component model for UML based on CSP aiming at compositional verification
verfasst von
Flávia Falcão
Lucas Lima
Augusto Sampaio
Pedro Antonino
Publikationsdatum
04.10.2023
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-023-01127-z

Premium Partner

    Bildnachweise