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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 2/2015

01.05.2015 | Regular Paper

AuRUS: explaining the validation of UML/OCL conceptual schemas

verfasst von: Guillem Rull, Carles Farré, Anna Queralt, Ernest Teniente, Toni Urpí

Erschienen in: Software and Systems Modeling | Ausgabe 2/2015

Einloggen

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

search-config
loading …

Abstract

The validation and the verification of conceptual schemas have attracted a lot of interest during the last years, and several tools have been developed to automate this process as much as possible. This is achieved, in general, by assessing whether the schema satisfies different kinds of desirable properties which ensure that the schema is correct. In this paper we describe AuRUS, a tool we have developed to analyze UML/OCL conceptual schemas and to explain their (in)correctness. When a property is satisfied, AuRUS provides a sample instantiation of the schema showing a particular situation where the property holds. When it is not, AuRUS provides an explanation for such unsatisfiability, i.e., a set of integrity constraints which is in contradiction with the property.
Vorheriger Artikel A generic model decomposition technique and its application to the Eclipse modeling framework
Nächster Artikel Formal verification of QVT transformations for code generation

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
Fußnoten
2
\(\mathrm{{CQC}}_\mathrm{E}\) stands for CQC with explanations. Note that although the CQC method was initially designed for query containment, it reformulated containment in terms of query satisfiability. So, it is essentially a query satisfiability checking method.
 
3
We consider that if a literal appears in node \(i\)+1 as a consequence of an unfolding, then the node that caused the appearance of the literal is the parent node \(i\).
 
Literatur
1.
Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases, vol. 8. Addison-Wesley, Reading (1995)MATH
2.
3.
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. Practical Aspects of Declarative Languages. Lecture Notes in Computer Science, vol. 3350, pp. 174–186 (2005)
4.
Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. Int. Joint Conf. Artif. Intell. 13, 276–276 (1993)
5.
Borgida, A., Calvanese, D., Rodriguez-Muro, M.: Explanation in the dl-lite family of description logics. On the Move to Meaningful Internet Systems: OTM 2008. Lecture Notes in Computer Science, vol. 5332, pp. 1440–1457 (2008)
6.
Brucker, A. D., Wolff, B.: HOL-OCL: A formal proof environment for UML/OCL. In: Fiadeiro, J.L., Inverardi, P. (eds.) Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, vol. 4961, pp. 97–100. Springer, Berlin, Heidelberg (2008)
7.
Brüning, J., Gogolla, M., Hamann, L., Kuhlmann, M.: Evaluating and debugging OCL expressions in UML models. In: Brucker, A.D., Julliand, J. (eds.) Tests and Proofs, vol. 7305, pp. 156–162. Springer, Berlin (2012)CrossRef
8.
Cabot, J., Clarisó, R., Riera, D.: UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming. In: Proceedings of the Twenty-Second IEEE/ACM International Conference on Automated Software Engineering, ASE ’07, pp. 547–548. New York, NY, USA (2007)
9.
Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning and efficient query answering in description logics: the DL-Lite family. J. Autom. Reason. 39(3), 385–429 (2007)CrossRefMATH
10.
Chiorean, D., Pasca, M., Cârcu, A., Botiza, C., Moldovan, S.: Ensuring UML models consistency using the OCL environment. Electron. Notes Theor. Comput. Sci. 102(November), 99–110 (2004)CrossRef
11.
Clavel, M., Egea, M.: ITP/OCL: a rewriting-based validation tool for UML+OCL static class diagrams. In: Johnson, M., Vene, V. (eds.) Algebraic Methodology and Software Technology, vol. 4019, pp. 368–373. Springer, Berlin (2006)CrossRef
12.
Decker, H., Teniente, E., Urpí, T.: How to tackle schema validation by view updating. In: Proceeding of the 5th International Conference on Extending Database Technology (EDBT), pp. 535–549 (1996)
13.
14.
Farré, C., Teniente, E., Urpí, T.: Checking query containment with the CQC method. Data Knowl. Eng. 53(2), 163–223 (2005)CrossRef
15.
Gogolla, M., Richters, M.: Expressing UML class diagrams properties with OCL. In: Object Modeling with OCL, Lecture Notes in Computer Science, vol. 2263, pp. 85–114 (2002)
16.
Gogolla, M., Bohling, J., Richters, M.: Validating UML and OCL models in USE by automatic snapshot generation. Softw. Syst. Model. 4(4), 386–398 (2005)CrossRef
17.
Grégoire, É., Mazure, B., Piette, C: On approaches to explaining infeasibility of sets of Boolean clauses. In: 20th IEEE International Conference on Tools with Artificial Intelligence, 2008. ICTAI’08 vol. 1, pp. 74–83 (2008)
18.
Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas. In: Theory and Applications of Satisfiability Testing, Lectur Notes in Computer Science, vol. 3569, pp. 173–186 (2005)
19.
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1–33 (2008)CrossRefMATHMathSciNet
20.
21.
Meyer, T., Lee, K., Booth, R., Pan, J.Z.: Finding maximally satisfiable terminologies for the description logic ALC. In: Proceedings of the National Conference on Artificial Intelligence, vol. 21, p. 269 (2006)
22.
23.
24.
25.
26.
Queralt, A., Teniente, E.: Verification and validation of UML conceptual schemas with OCL constraints. ACM Trans. Softw. Eng. Methodol. 21(2), 13 (2012)CrossRef
27.
28.
Rull, G., Farré, C., Teniente, E., Urpí, T.: Computing explanations for unlively queries in databases. In: Proceedings of the Sixteenth ACM Conference on Conference on Information and, Knowledge Management, pp. 955–958 (2007)
29.
Rull, G., Farré, C., Teniente, E., Urpí, T.: Providing explanations for database schema validation. In: Database and Expert Systems Applications, pp. 660–667 (2008)
30.
Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: International Joint Conference on Artificial Intelligence vol. 18, pp. 355–362 (2003)
31.
Schlobach, S., Huang, Z., Cornet, R., van Harmelen, F.: Debugging incoherent terminologies. J. Autom. Reason. 39(3), 317–349 (2007)CrossRefMATH
32.
De Siqueira, J.L., Puget, J.F.: Explanation-based generalisation of failures. In: Proceedings of ECAI vol. 88, pp. 339–344 (1988)
33.
Soeken, M., Wille, R., Drechsler, R.: Encoding OCL data types for SAT-based verification of UML/OCL models. In: Proceedings of the 5th International Conference on Tests and Proofs, TAP’11. pp. 152–170. Springer-Verlag, Berlin, Heidelberg (2011)
34.
Ullman, J.D.: Principles of Database and Knowledge-Base Systems, vol. 2. Computer Science Press, New York (1989)
35.
Wahler, M., Basin, D.A., Brucker, A.D., Koehler, J.: Efficient analysis of pattern-based constraint specifications. Softw. Syst. Model. 9(2), 225–255 (2010)CrossRef
36.
Wille, R., Soeken, M., Drechsler, R.: Debugging of inconsistent UML/OCL models. In: Design, Automation Test in Europe Conference Exhibition (DATE) 2012, pp. 1078–1083 (2012)
37.
Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Design, Automation and Test in Europe (DATE). pp. 10880–10885 (2003)
Metadaten
Titel
AuRUS: explaining the validation of UML/OCL conceptual schemas
verfasst von
Guillem Rull
Carles Farré
Anna Queralt
Ernest Teniente
Toni Urpí
Publikationsdatum
01.05.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 2/2015
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-013-0350-8

Weitere Artikel der Ausgabe 2/2015

Software and Systems Modeling 2/2015 Zur Ausgabe

Regular Paper

From subsets of model elements to submodels

Regular Paper

Formal verification of QVT transformations for code generation

Special Section Paper

An algorithm for generating model-sensitive search plans for pattern matching on EMF models

Regular Paper

A generic model decomposition technique and its application to the Eclipse modeling framework

Regular Paper

Formal synthesis of application and platform behaviors of embedded software systems

Regular Paper

A survey of approaches for verifying model transformations

Premium Partner

    Bildnachweise