From 6e3f4f810563d4e8c9c27a5570af37969ff8f3a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?J=C3=BCrgen=20Doser?= Date: Fri, 16 Mar 2007 11:11:02 +0000 Subject: [PATCH] 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 --- manual/manual.tex | 89 ++++++++++++++++++++ manual/su4sml.bib | 203 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 292 insertions(+) create mode 100644 manual/manual.tex create mode 100644 manual/su4sml.bib diff --git a/manual/manual.tex b/manual/manual.tex new file mode 100644 index 0000000..1adbf69 --- /dev/null +++ b/manual/manual.tex @@ -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} diff --git a/manual/su4sml.bib b/manual/su4sml.bib new file mode 100644 index 0000000..012ffac --- /dev/null +++ b/manual/su4sml.bib @@ -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} + +}