Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

14

TPHOL
2002
IEEE

favoriteEmaildiscussreport

98views Automated Reasoning» more TPHOL 2002»

A Proposal for a Formal OCL Semantics in Isabelle/HOL

13 years 9 months ago

A Proposal for a Formal OCL Semantics in Isabelle/HOL

Download www.brucker.ch

Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within the OMG; our work is an attempt to accompany this process by a proposal solving open questions in a consistent way and exploring alternatives of the language design. Moreover, our encoding gives the foundation for tool supported reasoning over OCL speciﬁcations, for example as basis for test case generation.

Achim D. Brucker, Burkhart Wolff

Real-time Traffic

Automated Reasoning | Conservative Shallow Embedding | Object Constraint Language | Open Standardization Process | TPHOL 2002 |

claim paper

Related Content

» Unifying Theories in IsabelleHOL

» FreeStyle Theorem Proving

» Enhancing the Message Concept of the Object Constraint Language

» Towards the Completion of the Formal Semantics of OCL 20

» Improving the OCL Semantics Definition by Applying Dynamic Meta Modeling and Design Patter...

» An Executable UML with OCLbased Action Semantics Language

» A Lightweight Approach for the Semantic Validation of Model Refinements

» Human Comprehensible and Machine Processable Specifications of Operational Semantics

» cmUML A UML based Framework for Formal Specification of Concurrent Reactive Systems

Post Info
More Details (n/a)

Added	16 Jul 2010
Updated	16 Jul 2010
Type	Conference
Year	2002
Where	TPHOL
Authors	Achim D. Brucker, Burkhart Wolff

Comments (0)