outline for a technical manual
git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@6245 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Jürgen Doser
parent
4bd8124d03
commit
6e3f4f8105
|
|
@ -0,0 +1,89 @@
|
|||
\documentclass[bibtotoc,liststotoc]{scrbook}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage[draft]{fixme}
|
||||
\begin{document}
|
||||
\titlehead{Information Security Group\\ETH Zurich}
|
||||
\title{The SU4SML Manual}
|
||||
\author{Jürgen Doser (et al.?)}
|
||||
\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.
|
||||
|
||||
%%% bibliography: all the related papers and student theses
|
||||
\bibliographystyle{alpha}
|
||||
\bibliography{su4sml}
|
||||
%\appendix
|
||||
%\listoffixmes
|
||||
\end{document}
|
||||
|
|
@ -0,0 +1,203 @@
|
|||
@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}
|
||||
|
||||
}
|
||||
Loading…
Reference in New Issue