Isabelle/HOL-OCL
HOL-OCL ist ein interaktives Beweissystem für die Object Constraint Language (OCL). HOL-OCL ist eine flache Einbettung von OCL in die Logik höhrer Ordnung (HOL) Instanz des interaktiven Theorembeweisers Isabelle. HOL-OCL wird von Achim D. Brucker und Burkhart Wolff entwickelt.
HOL-OCL erlaubt Beweise über OCL Spezifikationen zu führen, OCL Spezifikationen zu verfeinern und bietet die Grundlage für weitere Anwendungen, z.B. die automatische Test-Datensatz Berechnung.
HOL-OCL ist freie Software und kann unter den Bedingungen der GPL weitergegebenwerden und wird von Achim D. Brucker und Burkhart Wolff entwickelt.
Download
hol-ocl-0.9.0.tar.gz
(ca. 4.6 MiB, MD5: a41aa55362108d8141ec4d901844cc08)
ChangeLog
Publikationen
-
Achim D. Brucker, Gwendal Daniel, Martin Gogolla, Frédéric Jouault, Christophe Ponsard,, Valéry Ramon und Edward D. Willink.
Emerging Topics in Textual Modelling.
In OCL 2019. CEUR Workshop Proceedings, 2513, pages 91-104, CEUR-WS.org, 2019.
Kategorien:
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Jordi Cabot, Gwendal Daniel, Martin Gogolla, Adolfo Sánchez-Barbudo Herrera, Frank Hilken, Frédéric Tuong, Edward D. Willink und Burkhart Wolff.
Recent Developments in OCL and Textual Modelling.
In Proceedings of the International Workshop on OCL and Textual Modeling (OCL 2016). CEUR Workshop Proceedings, 1756, pages 157-165, CEUR-WS.org, 2016.
Kategorien:
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Frédéric Tuong und Burkhart Wolff.
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. LRI, Univ Paris Sud, CNRS, Centrale Supélec, Université Paris-Saclay, France, Technical Report 1582, 2015.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Frédéric Tuong und Burkhart Wolff.
A Meta-Model for the Isabelle API.
In Archive of Formal Proofs, 2015.
(BibTeX) (Endnote) (RIS) (Word) (URL) ( )
-
Achim D. Brucker, Dan Chiorean, Tony Clark, Birgit Demuth, Martin Gogolla, Dimitri Plotnikov, Bernhard Rumpe, Edward D. Willink und Burkhart Wolff.
Report on the Aachen OCL Meeting.
In Proceedings of the MODELS 2013 OCL Workshop (OCL 2013). CEUR Workshop Proceedings, 1092, pages 103-111, CEUR-WS.org, 2013.
Kategorien:
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Delphine Longuet, Frédéric Tuong und Burkhart Wolff.
On the Semantics of Object-oriented Data Structures and Path Expressions.
In Proceedings of the MODELS 2013 OCL Workshop (OCL 2013). CEUR Workshop Proceedings, 1092, pages 23-32, CEUR-WS.org, 2013. An extended version of this paper is available as LRI Technical Report 1565.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Delphine Longuet, Frédéric Tuong und Burkhart Wolff.
On the Semantics of Object-oriented Data Structures and Path Expressions (Extended Version). Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, Technical Report 1565, 2013.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Matthias P. Krieger und Burkhart Wolff.
Extending OCL with Null-References.
In Models in Software Engineering. Lecture Notes in Computer Science (6002), pages 261-275, Springer-Verlag , 2009. Selected best papers from all satellite events of the MoDELS 2009 conference.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-12261-3_25) ( )
-
Achim D. Brucker und Burkhart Wolff.
Semantics, Calculi, and Analysis for Object-oriented Specifications.
In Acta Informatica, 46 (4), pages 255-284, 2009.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s00236-009-0093-8) ( )
-
Achim D. Brucker und Burkhart Wolff.
HOL-OCL - A Formal Proof Environment for UML/OCL.
In Fundamental Approaches to Software Engineering (FASE08). Lecture Notes in Computer Science (4961), pages 97-100, Springer-Verlag , 2008.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-78743-3_8) ( )
-
Achim D. Brucker und Burkhart Wolff.
Extensible Universes for Object-oriented Data Models.
In ECOOP 2008 - Object-Oriented Programming. Lecture Notes in Computer Science (5142), pages 438-462, Springer-Verlag , 2008.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-70592-5_19) ( )
-
Achim D. Brucker und Burkhart Wolff.
An Extensible Encoding of Object-oriented Data Models in HOL.
In Journal of Automated Reasoning, 41, pages 219-249, 2008.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s10817-008-9108-3) ( )
-
Achim D. Brucker, Jürgen Doser und Burkhart Wolff.
A Model Transformation Semantics and Analysis Methodology for SecureUML.
In MoDELS 2006: Model Driven Engineering Languages and Systems. Lecture Notes in Computer Science (4199), pages 306-320, Springer-Verlag , 2006. An extended version of this paper is available as ETH Technical Report, no. 524.
Kategorien: , ,
(Zusammenfassung) (Artikel als PDF Datei) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/11880240_22) ( )
-
Achim D. Brucker, Jürgen Doser und Burkhart Wolff.
A Model Transformation Semantics and Analysis Methodology for SecureUML. ETH Zurich, Technical Report 524, 2006.
Kategorien: , ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Jürgen Doser und Burkhart Wolff.
An MDA Framework Supporting OCL.
In Electronic Communications of the EASST, 5, 2006.
Kategorien: , ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.14279/tuj.eceasst.5.45) ( )
-
Achim D. Brucker, Jürgen Doser und Burkhart Wolff.
Semantic Issues of OCL: Past, Present, and Future.
In Electronic Communications of the EASST, 5, 2006.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:http://dx.doi.org/10.14279/tuj.eceasst.5.46) ( )
-
Achim D. Brucker und Burkhart Wolff.
A Package for Extensible Object-Oriented Data Models with an Application to IMP++.
In International Workshop on Software Verification and Validation (SVV 2006), 2006.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker und Burkhart Wolff.
The HOL-OCL Book. ETH Zurich, Technical Report 525, 2006.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker und Burkhart Wolff.
HOL-OCL: Experiences, Consequences and Design Choices.
In UML 2002: Model Engineering, Concepts and Tools. Lecture Notes in Computer Science (2460), pages 196-211, Springer-Verlag , 2002.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-45800-X_17) ( )
-
Achim D. Brucker und Burkhart Wolff.
A Proposal for a Formal OCL Semantics in Isabelle/HOL.
In Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science (2410), pages 99-114, Springer-Verlag , 2002.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-45685-6_8) ( )
-
Achim D. Brucker und Burkhart Wolff.
A Note on Design Decisions of a Formalization of the OCL. Albert-Ludwigs-Universität Freiburg, Technical Report 168, 2002.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )