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

Debian Pakete

Anwender von Debian GNU/Linux können HOL-OCL auch aus folgender apt Quelle beziehen:

deb http://kisogawa.inf.ethz.ch/isamorph/debian unstable main
deb-src http://kisogawa.inf.ethz.ch/isamorph/debian unstable main

Hinweis: Bitte ersetzen Sie unstable mit der Distribution, die Sie nutzen; also stable, testing, oder unstable.

Publikationen

2012

• Achim D. Brucker und Burkhart Wolff. Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and Textual Modelling (OCL 2012)., pages 19-24, 2012.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1145/2428516.2428520) ( )
  

2011

• Matthias P. Krieger und Achim D. Brucker. Extending OCL Operation Contracts with Objective Functions. In Electronic Communications of the EASST, 44, 2011.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (ECEASST) ( )
  

2010

• Achim D. Brucker und Matthias P. Krieger und Delphine Longuet und Burkhart Wolff. A Specification-based Test Case Generation Method for UML/OCL. In MoDELS Workshops. Lecture Notes in Computer Science (6627), pages 334-348, Springer-Verlag , 2010. Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-21210-9_33) ( )
  

2009

• Achim D. Brucker und 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) (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) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s00236-009-0093-8) ( )
  

2008

• 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) (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) (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) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s10817-008-9108-3) ( )
  

2007

• Achim D. Brucker. An Interactive Proof Environment for Object-oriented Specifications. ETH Zurich,2007. ETH Dissertation No. 17097.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2006

• Achim D. Brucker und 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) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/11880240_22) ( )
  
• Achim D. Brucker und Jürgen Doser und Burkhart Wolff. A Model Transformation Semantics and Analysis Methodology for SecureUML. ETH Zurich, Technical Report 524, 2006.
  Kategorien: , ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Achim D. Brucker und Jürgen Doser und Burkhart Wolff. An MDA Framework Supporting OCL. In Electronic Communications of the EASST, 5, 2006.
  Kategorien: , ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (ECEASST) ( )
  
• Achim D. Brucker und 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) (BibTeX) (Endnote) (RIS) (Word) (ECEASST) ( )
  
• 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) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Achim D. Brucker und Burkhart Wolff. The HOL-OCL Book. ETH Zurich, Technical Report 525, 2006.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2003

• Achim D. Brucker und Burkhart Wolff. Using Theory Morphisms for Implementing Formal Methods Tools. In Types for Proof and Programs. Lecture Notes in Computer Science (2646), pages 59-77, Springer-Verlag , 2003.
  Kategorien:
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-39185-1_4) ( )
  

2002

• 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) (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) (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) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2001

• Achim D. Brucker und Burkhart Wolff. Checking OCL Constraints in Distributed Systems Using J2EE/EJB. Albert-Ludwigs-Universität Freiburg, Technical Report 157, 2001.
  Kategorien:
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Achim D. Brucker und Burkhart Wolff. Testing Distributed Component Based Systems Using UML/OCL. In Informatik 2001.Tagungsband der GI/ÖCG Jahrestagung, 1 (157), pages 608-614, 2001.
  Kategorien:
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )