HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

Removed outdated manual setup.

This commit is contained in:
Achim D. Brucker 2016-10-21 21:20:07 +01:00
parent e9c4af41bb
commit 228c59f7c8
2 changed files with 0 additions and 301 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

98
manual/manual.tex
View File

@ -1,98 +0,0 @@
\documentclass[bibtotoc,liststotoc]{scrbook}
\usepackage[utf8]{inputenc}
\usepackage[draft]{fixme}
\begin{document}
\title{The SU4SML Manual}
\author{Achim Brucker and Jürgen Doser}
\maketitle
\tableofcontents
\chapter{Introduction}
general introduction and overview over the capabilities presented
below. Installation and ``getting started'' and short usage
instructions?
Overview of the use of su4sml in the complete toolchain as described
in \cite{brucker.ea:mda:2006-b}. Also mention the work in
\cite{marcel.beer:sa:2006,beer:generic:2007,brucker.ea:mda:2006-b}.
\chapter{XMI \& Rep Parser}
describe requirements on the xmi format. How to adjust to other xmi
dialects. How to add other input languages (other than xmi) to the
rep\_parser.
\chapter{Model Transformation Support}
describe any major transformation function (su2holocl, normalizing
associations,...), as well as any major functionality for writing
transformation functions (are there any?)
\section{su2holocl}
Based on \cite{crijke:transforming:2006}.
\section{association-related}
\section{generic transformation framework?}
\chapter{The HOL-OCL Interface?}
describe any requirements/limitations the HOL-OCL interface currently
has. (no associations, etc.). Based on
\cite{brucker.ea:hol-ocl-book:2006}?
\chapter{The Generic Code Generator: GCG}
\section{The GCG Framework}
some overall architecture stuff from
\cite{eidenbenz:development:2006}. lots of
pictures :)
\section{Individual Cartridge Documentation}
describe each cartridge in a fixed form (using some predefined
makros). Basically a list of the supported variables, lists, and
predicates of the cartridge, together with (short) descriptions of
them.
\subsection{The BaseCartridge}
\subsection{The C\# Cartridge}
\subsection{The StateMachine Cartridge}
Based on \cite{adelsberger:development:2006}
\subsection{The JavaCartridge}
\subsection{The Junit Cartridge}
Based on \cite{stock:automatic:2007}
\subsection{The SecureUML Cartridge}
\subsection{...}
\section{Misc. utilities}
subsections for additional things like the jtestdataaccessor
library from Manfred, or the statemachine animator from Rolf.
\chapter{Developer's Guide}
\section{Build Setup}
We currently support the following SML compiler:
\begin{itemize}
\item sml/NJ (tested with version 110.52 and 110.62) using CM files
\item mlton (tested with version 20061107-1) using CM files
\item poly/ML (tested with version 5.0) using ROOT.ML files (i.e., plain \texttt{use} commands)
\end{itemize}
%%% bibliography: all the related papers and student theses
\bibliographystyle{alpha}
\bibliography{su4sml}
%\appendix
%\listoffixmes
\end{document}

203
manual/su4sml.bib
View File

@ -1,203 +0,0 @@
@Article{ brucker.ea:mda:2006-b,
abstract = {We present an MDA framework, developed in the functional
programming language SML, that tries to bridge the gap
between formal software development and the needs of
industrial software development, e.g., code generation.
Overall, our tool-chain provides support for software
modeling using UML/OCL and guides the user from
type-checking and model transformations to code generation
and formal analysis of the UML/OCL model. We conclude with
a report on our experiences in using a functional language
for implementing MDA tools. },
author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
language = {USenglish},
public = {yes},
categories = {holocl},
classification= {ejournal},
title = {An {MDA} Framework Supporting{ OCL}},
editor = {Birgith Demuth and Dan Chiorean and Martin Gogolla and Jos
Warmer},
issn = {1863-2122},
volume = 5,
year = 2006,
journal = j-eceasst,
pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-mda-2006-b.pd
f},
ps = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-mda-2006-b.ps
.gz},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-mda-2006-b}
}
@Misc{marcel.beer:sa:2006,
author = {Marcel Beer},
title = {Development of a {GUI} for {SecureUML}},
howpublished = {Semester thesis, ETH Zurich},
year = 2006}
@Thesis{ schmid:integrating:2007,
abstract = {In diesem Vortrag wird die Analyse und Implementierung der
Integration eines OCL-Typ-Checkers in ArgoUML vorgestellt
und erl{\"a}utert. Nach der Diskussion {\"u}ber die Architektur der
Integration, bildet ein Ausblick auf m{\"o}gliche weiterf{\"u}hrende
Arbeiten den Abschluss.},
author = {Raphael Schmid},
month = {March},
supervisor = {Basin David, Brucker Achim, Doser Juergen},
title = {Integrating an {OCL} Typechecker into {ArgoUML}},
howpublished = {Semester thesis, ETH Zurich},
type = {semester thesis},
year = 2007,
user = {bgeiser}
}
@Thesis{ stock:automatic:2007,
abstract = {Testing is an important activity in the development of
(software) systems. This presentation will first give short
introductions to UML class diagrams, the Object Constraint
Language (OCL) for the specification of contracts in the
context of the UML and unit testing. It will then go on
togive an overview of the existing tool-chain also showing
where the work of this thesis fits in. Finally, the chosen
layout and implementation of the generated test suites
including the file format for providing test data to the
unit tests will be explained in more detail. },
author = {Manfred Stock},
month = {January},
supervisor = {Achim Brucker and J\"urgen Doser},
title = {Automatic Generation of {Junit} Test-Harnesses},
howpublished = {Semester Thesis, ETH Zurich},
type = {semester thesis},
year = 2007,
user = {bgeiser}
}
@Thesis{ beer:generic:2007,
abstract = {In this Diploma Thesis, a generic metamodel-based GUI to
display and edit SecureUML policies has been developed and
plugged into the open source CASE-tool ArgoUML. SecureUML
policies are displayed in a more compact way than in the
UML notation for SecureUML and can be edited more easily.
The GUI supports arbitrary SecureUML dialects and considers
role hierarchies and composite actions.In the first part of
the presentation, the concepts of the GUI and some solved
problems are presented. In the second part, the
functionality of the GUI and its integration into the CASE
tool ArgoUML is shown in a short Demo.},
author = {Marcel Beer},
month = {March},
supervisor = {Basin David, Brucker Achim, Doser Juergen},
title = {A generic metamodel-based {GUI} for {SecureUML}},
howpublished = {Diploma thesis, ETH Zurich},
type = {diploma thesis},
year = 2007,
user = {bgeiser}
}
@Thesis{ adelsberger:development:2006,
author = {Rolf Adelsberger},
month = {March},
supervisor = {J\"urgen Doser and Achim Brucker},
title = {Development of a Template-driven Code Generator for {UML}
Statecharts},
type = {semester thesis},
howpublished = {Semester thesis, ETH Zurich},
year = 2006,
user = {dsenn}
}
@Thesis{ eidenbenz:development:2006,
author = {Raphael Eidenbenz},
month = {March},
supervisor = {J\"urgen Doser and Achim Brucker},
title = {Development of a Template-driven Code Generator},
type = {semester thesis},
howpublished = {Semester thesis, ETH Zurich},
year = 2006,
pdf = {papers/2005/2005_eraphael_codegen.pdf},
user = {dsenn}
}
@Thesis{ crijke:transforming:2006,
author = {Christian Rijke},
month = March,
supervisor = {J\"urgen Doser and Achim Brucker},
title = {Transforming {SecureUML} Models into {UML}/{OCL} Models},
type = {master thesis},
howpublished = {Master thesis, ETH Zurich},
year = 2006,
pdf = {papers/2005/2005_crijke_su2holocl.pdf},
user = {dsenn}
}
@Article{ basin.ea:model:2006,
abstract = {We present a new approach to building secure systems. In
our approach, which we call Model Driven Security,
designers specify system models along with their security
requirements and use tools to automatically generate system
architectures from the models including complete,
configured access control infrastructures. Rather than
fixing one particular modeling language for this process,
we propose a general schema for constructing such languages
that combines languages for modeling systems with languages
for modeling security. We present several instances of this
schema thatcombine (both syntactically and semantically)
different UML modeling languages with a security modeling
language for formalizing access control requirements. From
models in the combined languages, we automatically generate
access control infrastructures for server-based
applications, built from declarative and programmatic
access control mechanisms. The modeling languages and
generation process are semantically well-founded and are
based on an extension of Role-Based Access Control. We have
implemented this approach ina UML-based CASE-tool and
report on experiments.},
author = {David Basin and J\"urgen Doser and Torsten Lodderstedt},
copyright = {© ACM, (2006)},
copyrighturl = {http://doi.acm.org/10.1145/1125808.1125810},
issn = {1049-331X},
journal = {ACM Transactions on Software Engineering and Methodology},
language = {USenglish},
month = {January},
note = {An intermediate version is available as ETH technical
report no. 414},
number = 1,
pages = {39--91},
title = {Model Driven Security: from {UML} Models to Access Control
Infrastructures},
volume = 15,
year = 2006,
user = {doserj}
}
@TechReport{ brucker.ea:hol-ocl-book:2006,
author = {Achim D. Brucker and Burkhart Wolff},
institution = {ETH Zurich},
language = {USenglish},
title = {The {HOL-OCL} Book},
classification= {unrefereed},
categories = {holocl},
year = 2006,
number = 525,
abstract = {HOL-OCL is an interactive proof environment for the Object
Constraint Language (OCL). It is implemented as a shallow
embedding of OCL into the Higher-order Logic (HOL) instance
of the interactive theorem prover Isabelle. HOL-OCL defines
a machine-checked formalization of the semantics as
described in the standard for OCL 2.0. This conservative,
shallow embedding of UML/OCL into Isabelle/HOL includes
support for typed, extensible UML data models supporting
inheritance and subtyping inside the typed lambda-calculus
with parametric polymorphism. As a consequence of
conservativity with respect to higher-order logic (HOL), we
can guarantee the consistency of the semantic model.
Moreover, HOL-OCL provides several derived calculi for
UML/OCL that allow for formal derivations establishing the
validity of UML/OCL formulae. Elementary automated support
for such proofs is also provided top },
bibkey = {brucker.ea:hol-ocl-book:2006},
pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf},
keywords = {security, SecureUML, UML, OCL, HOL-OCL,
model-transformation},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006}
}