Quelle  root.tex

\documentclass[11pt,a4paper]{book}
\usepackage{isabelle,isabellesym}
\usepackage{graphicx}
\graphicspath{document}


% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{pifont}

\usepackage{latexsym}
\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% fixes generation until the AFP updates their LaTeX
\pagestyle{plain}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{HOL-CSPM - Architectural operators for HOL-CSP}
\author{Benoît Ballenghien \and Safouan Taha \and Burkhart Wolff}
\maketitle
\chapter*{Abstract}

   Recently, a modern version of Roscoes and Brookes \cite{brookes-roscoe85} 
   Failure-Divergence Semantics for CSP has been formalized in Isabelle \cite{HOL-CSP-AFP}. 
   On top of this theory, we develop the so-called ``architectural operators'', i.e.
   generalizations of basic non-deterministic choices, synchronized producs and sequetializations,
   as has been introduced in the well-known FDR4 model-checker for CSP.

   While FDR4 uses these architectural operators as handy macros that help to structure
   the specifications, they are basically syntactic sugar and expanded before the Labelled 
   Transition Systems were generated. In contrast, we develop the formal theory of these 
   operators in themselves which paves the way for a more structured approach to reasoning 
   in HOL-CSP. Our generalizations will take commutativity and idempotence into account,
   such that they become fully-abstract wrt. to index-sets, index-multi-sets or lists, 
   respectively. 

   Additionally, the theory of some more exotic --- but in the CSP literature discussed --- 
   operators have been developed; in particular throw and interupt.

   For these "architectural operators", we will prove the properties of refinement,
   monotonicity and continuity and the laws of interaction in order to simplify their use.

   Finally, we will give examples of their usefulness when trying to model complex systems.

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: