Subject: lnews.tex.shar

From: "Prof K J Turner (Staff)" <[email-masked]>
Date: Mon, 24 Apr 1995 12:04:35 +0100

#! /bin/sh
# This is a shell archive, meaning:
# 1. Remove everything above the #! /bin/sh line.
# 2. Save the resulting text in a file.
# 3. Execute the file with /bin/sh (not csh) to create the files:
#	lnews.readme
#	lnews.sty
#	lnews.tex
# This archive created: Fri Apr 21 18:12:20 1995
export PATH; PATH=/bin:$PATH
if test -f 'lnews.readme'
then
	echo shar: will not over-write existing file "'lnews.readme'"
else
sed 's/^://' << \SHAR_EOF > 'lnews.readme'
:LOTOS News, Issue 03, February 1995
:
:The files constituting this are distributed in two forms:
:
:  o as LaTeX source `lnews.tex.shar' containing:
:  

:    -rw-------  1 kjt          527 Apr 21 18:11 lnews.readme
:    -rw-------  1 kjt         8217 Apr 20 20:28 lnews.sty
:    -rw-------  1 kjt        91250 Apr 21 18:04 lnews.tex
:
:  o as PostScript `lnews.ps.shar':
:  

:    -rw-------  1 kjt          527 Apr 21 18:11 lnews.readme
:    -rw-------  1 kjt       145851 Apr 21 18:06 lnews.ps
:
:Ken Turner, University of Stirling, 21/04/95
SHAR_EOF
fi # end of overwriting check
if test -f 'lnews.sty'
then
	echo shar: will not over-write existing file "'lnews.sty'"
else
sed 's/^://' << \SHAR_EOF > 'lnews.sty'
:%%% "lnews.sty"	K. J. Turner	20/04/95
:
:%%%%%%%%%%%%%%%%%%%%%%%% LOTOS News Formatting Macros  
%%%%%%%%%%%%%%%%%%%%%%%%
:
:% Basic document style
:
:\input{article.sty}
:
:% Page sizes for A4 - comment out for local default page size
:
:\topmargin 0 pt
:\oddsidemargin 0.25 in
:\evensidemargin \oddsidemargin
:\marginparwidth 1 in
:\textwidth 5.875 in 

:\textheight 53\baselineskip
:\advance\textheight by \topskip
:
:% Title and Page Heading
:
:\pagestyle{myheadings}
:
:\def\issue#1{\def\lnissue{#1}}
:
:\def\date#1{\def\lndate{#1}}
:
:\def\maketitle{
:  \rule[0.8mm]{\textwidth}{0.5mm}\\
:  {\large \bf Issue \lnissue} \hfill {\large \it Editor:} \\
:  \mbox{} \hfill Ken Turner \\
:  {\huge \bf L{\LARGE \bf OTOS} N{\LARGE \bf EWS}} \hfill Department of  
Computing Science \\
:  \mbox{} \hfill University of Stirling \\[0.8mm]
:  {\large \bf \lndate} \hfill {\it Email:} [email-masked] \\
:  \rule{\textwidth}{0.5mm}\par
:  \def\@evenhead{%
:    \it L{\small \it OTOS} News \hfill Issue \lnissue, \lndate \hfill%
:    Page \thepage%
:  }
:  \def\@oddhead{%
:    \it L{\small \it OTOS} News \hfill Issue \lnissue, \lndate \hfill%
:    Page \thepage%
:  }
:  \thispagestyle{empty}
:}
:
:% Contents
:
:\def\tableofcontents{%
:  \par\vspace{3mm}
:  {\LARGE \bf Contents}
:  \par\vspace{1mm}
:  \@starttoc{toc}
:}
:
:% Contribution sections
:
:\newlength{\sectline}
:
:\renewcommand{\section}[1]{		% section - title
:  \settowidth{\sectline}{\LARGE \bf #1}
:  \addtolength{\sectline}{3.7mm}
:  \setlength{\sectline}{-\sectline}
:  \addtolength{\sectline}{\textwidth}
:  \setlength{\sectline}{0.5 \sectline}
:  \clearpage
:  \rule{\sectline}{0.25mm}\hspace{1mm}
:  \raisebox{-1.5mm}{\LARGE \bf #1}
:  \hspace{1mm}\rule{\sectline}{0.25mm}
:  \addcontentsline{toc}{section}{#1}
:  \par\vspace{2mm}
:}
:
:\renewcommand{\subsection}[4]{	% subsection - title, name, organisation,  
email
:  \par\vspace{4mm}
:  \mbox{}\dotfill\raisebox{-1mm}{\large \bf #1}\dotfill\mbox{}
:  \addcontentsline{toc}{subsection}{#1}
:  \par\vspace{1mm}
:  {\bf Source:} #2, #3 \hfill {\bf Email:} #4
:  \par\vspace{2mm}
:}
:
:\renewcommand{\subsubsection}[1]{	% subsubsection - title
:  \par\vspace{2mm}
:  {\normalsize \bf #1}
:  \par\vspace{2mm}
:}
:
:% Editor's Note
:
:\newcommand{\ednote}[1]{
:  \begin{quote}
:  {\small \bf Editor's Note: \rm #1}
:  \end{quote}
:}
:
:% References
:
:\newcommand{\etalchar}[1]{$^{#1}$}
:
:\def\refsection#1{			% references - width
:  \section{Collected References}\list
:  {\@biblabel{\arabic{enumiv}}}{\settowidth\labelwidth{\@biblabel{#1}}%
:    \leftmargin\labelwidth
:    \advance\leftmargin\labelsep
:    \usecounter{enumiv}%
:    \let\p@enumiv\@empty
:    \def\theenumiv{\arabic{enumiv}}}%
:    \def\newblock{\hskip .11em plus.33em minus.07em}%
:    \sloppy\clubpenalty4000\widowpenalty4000
:    \sfcode`\.=1000\relax
:}
:
:\def\endrefsection{%
:  \def\@noitemerr{\@warning{Empty `refsection' environment}}%
:  \endlist
:}
:
:% End of Newsletter
:
:\newcommand{\newsend}{		% end of newsletter -
:  \par\vspace{8mm}
:  \rule[0.8mm]{\textwidth}{0.5mm}
:  \par
:}
:
:% Paragraphs and Lists
:
:\parindent 0em
:\parskip 1ex
:
:\def\labelenumi{(\alph{enumi})}    

:\def\theenumi{\alph{enumi}}
:\def\labelitemi{$\bullet$}
:\leftmargini 2em
:
:\def\labelenumii{(\arabic{enumii})}
:\def\theenumii{\arabic{enumii}}
:\def\labelitemii{$\circ$}
:\leftmarginii 2em
:
:\def\labelenumiii{(\Alph{enumiii})}    

:\def\theenumiii{\Alph{enumiii}}
:\def\labelitemiii{$\star$}
:\leftmarginiii 2em
:
:\def\labelenumiv{(\roman{enumiv})}    

:\def\theenumiv{\roman{enumi}}
:\def\labelitemiv{$\cdot$}
:\leftmarginiv 2em
:
:% Dimensions
:
:\setlength{\unitlength}{1mm}
:
:% Logos
:
:\newcommand{\ActOne}{{\sc ActOne}}
:
:\newcommand{\Estelle}{{\sc Estelle}}
:\newcommand{\Estellebf}{{\normalsize \bf E{\footnotesize \bf STELLE}}}
:\newcommand{\Estelleit}{{\normalsize \it E{\footnotesize \it STELLE}}}
:
:\newcommand{\Lotos}{{\sc Lotos}}
:\newcommand{\Lotosbf}{{\normalsize \bf L{\footnotesize \bf OTOS}}}
:\newcommand{\Lotosit}{{\normalsize \it L{\footnotesize \it OTOS}}}
:\newcommand{\Lotosss}{{\normalsize \bf L{\footnotesize \bf OTOS}}}
:
:\newcommand{\LotosNews}{{\Lotos\ News}}
:
:%%% "lotos.sty"	K. J. Turner	26/06/93
:
:% This is a style file that defines an environment for formatting
:% LOTOS specifications. Embedded spaces and tabs are presumed to have
:% been previously converted to tabs (\>) for the "tabbing"
:% environment, and newlines are presumed to have been previously
:% converted to newlines (\\) for the "tabbing" environment.
:%
:% Special characters (boxes) are defined for some operators:
:%
:%   \bec	:=
:%   \cho	[]
:%   \dis	[>
:%   \ena	>>
:%   \imp	=>
:%   \map	->
:%
:% For example, the Lotos specification:
:%
:%   specification Test [Ip, Op] : noexit :=
:% 

:%     library
:%     Nat
:%     endlib
:%   

:%     behaviour Ip ? N : Nat; Op ! N + N; stop
:% 

:%   endspec (* Test *)
:%
:% should be entered as:
:%
:%   {\bf specification} Test [Ip, Op] : {\bf noexit} :=\\
:%   \\
:%   \hspace{1.0em}{\bf library}\\
:%   \hspace{2.0em}Nat\\
:%   \hspace{1.0em}{\bf endlib}\\
:%   \\
:%   \hspace{1.0em}{\bf behaviour} Ip ? N : Nat; Op ! N + N; {\bf stop}\\
:%   \\
:%   {\bf endspec} (* Test *)\\
:%   \end{lotos}
:%
:% The size of LOTOS text is "\normalsize" by default but may be changed  
with:
:%
:%   \renewcommand{\lotossize}{small}
:
:\newcommand{\lotossize}{small}
:
:\newenvironment{lotos}
:  {
:    \vspace{-1.25ex}
:    \begin{\lotossize}
:    \begin{tabbing}
:      \hspace{2 \parindent}\=\hspace{4em}\=\hspace{4em}\=\hspace{4em}\=
:      \hspace{4em}\=\hspace{4em}\=\hspace{4em}\=\hspace{4em}\=
:      \hspace{4em}\=\hspace{4em}\=\hspace{4em}\=\hspace{4em}\=
:      \hspace{4em}\=\+\kill
:  }%
:  {
:    \end{tabbing}
:    \end{\lotossize}
:    \vspace{-4ex}
: }
:
:\setlength{\unitlength}{1mm}
:
:% Becomes Operator
:
:\newcommand{\bec}{\usebox{\becb}}
:\newsavebox{\becb}
:\sbox{\becb}{
:\begin{picture}(1.2, 1.6)(0.9, 0.2)
:\put(0, 0.2){:}
:\put(1.1, 0.6){\line(1, 0){1.6}}
:\put(1.1, 1.3){\line(1, 0){1.6}}
:\end{picture}
:}
:
:% Choice Operator
:
:\newcommand{\cho}{\usebox{\chob}}
:\newsavebox{\chob}
:\sbox{\chob}{
:\begin{picture}(-0.45, 2.5)(0.7, 0.8)
:\put(0, 0){\line(0, 1){3.4}}
:\put(0, 3.4){\line(1, 0){1.07}}
:\put(0, 0){\line(1, 0){1.07}}
:\put(0.95, 0){\line(0, 1){3.4}}
:\end{picture}
:}
:
:% Disable Operator
:
:\newcommand{\dis}{\usebox{\disb}}
:\newsavebox{\disb}
:\sbox{\disb}{
:\begin{picture}(0.7, 1)(0.8, 0)
:\put(0, 0){\line(0, 1){1.9}}
:\put(0, 1.9){\line(1, 0){0.55}}
:\put(0, 0){\line(1, 0){0.55}}
:\put(0.2, 0.13){$>$}
:\end{picture}
:}
:
:% Enable Operator
:
:\newcommand{\ena}{\usebox{\enab}}
:\newsavebox{\enab}
:\sbox{\enab}{
:\begin{picture}(2.0, 2.5)(1.1, 0)
:\put(0, 0){$>$}
:\put(1.5, 0){$>$}
:\end{picture}
:}
:
:% Implies Operator
:
:\newcommand{\imp}{\usebox{\impb}}
:\newsavebox{\impb}
:\sbox{\impb}{
:\begin{picture}(1.6, 2.5)(0.9, 0)
:\put(0, 0){$=$}
:\put(1, 0){$>$}
:\end{picture}
:}
:
:% Map Operator
:
:\newcommand{\map}{\usebox{\mapb}}
:\newsavebox{\mapb}
:\sbox{\mapb}{
:\begin{picture}(1.6, 2.5)(1.9, 0)
:\put(1.2, 0.83){\line(1, 0){2.9}}
:\put(2, 0){$>$}
:\end{picture}
:}
:
:%%% "comment.sty"   version 1.0 2 November 1990
:
:% to be used with plain TeX or LaTeX
:
:% Author
:%    Victor Eijkhout
:%    Center for Supercomputing Research and Development
:%    University of Illinois at Urbana-Champaign
:%    305 Talbot Lab
:%    104 South Wright Street
:%    Urbana, Illinois 61801, USA
:%
:%    [email-masked]
:%
:% Usage: all text included in between
:%    \comment ... \endcomment
:% or \begin{comment} ... \end{comment}
:% is discarded. The closing command should appear on a line
:% of its own. No starting spaces, nothing after it.
:% This environment should work with arbitrary amounts
:% of comment.
:%
:% Basic approach: take every line in verbatim mode as macro
:% argument, then don't do nothing with.
:
:\def\makeinnocent#1{\catcode`#1=12 }
:
:\def\comment{\begingroup
:    \let\do\makeinnocent \dospecials
:    \makeinnocent\^^L % and whatever other special cases
:    \endlinechar`\^^M \catcode`\^^M=12 \xcomment}
:{\catcode`\^^M=12 \endlinechar=-1 %
: \gdef\xcomment#1^^M{\def\test{#1}
:      \ifx\test\plainendcommenttest
:          \let\next\endgroup
:      \else\ifx\test\lalaendcommenttest
:          \def\next{\endgroup\end{comment}}
:      \else
:          \let\next\xcomment
:      \fi \fi \next}
:}
:
:{\escapechar=-1
: \xdef\plainendcommenttest{\string\\endcomment}
: \xdef\lalaendcommenttest{\string\\end\string\{comment\string\}}
:}
:
:\endinput
SHAR_EOF
fi # end of overwriting check
if test -f 'lnews.tex'
then
	echo shar: will not over-write existing file "'lnews.tex'"
else
sed 's/^://' << \SHAR_EOF > 'lnews.tex'
:%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LOTOS News Issue 3  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:
:\documentstyle[times]{lnews}
:
:%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Issue Details  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:
:\issue{03}
:
:\date{February 1995}
:
:%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Body of Text  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:
:\begin{document}
:
:\maketitle
:
:\tableofcontents
:
:%%% Editorial
:
:\section{Editorial}
:
:I much regret that this issue of \LotosNews\ has fallen through a  
time-warp
:(otherwise known as the European Fourth Framework Programme!). Like most
:European academics I have been working flat out to make European project
:proposals. I kept the date of February 1995 since most of the material  
dates
:from then, even though it has taken me weeks to find time for collating  
it.
:
:Of course, this problem is one of the reasons why this is likely to
:be the last issue of \LotosNews\ in its present form. There seems to be a
:high degree of agreement that the information should be published via WWW
:(World-Wide Web) in future. This issue is revisited under General News.  
The
:net result should be a greater variety of information, available in a more
:digestible form. Bon appetit!
:
:%%% General News
:
:\section{General News}
:
:This section is devoted to general developments of interest to the
:\Lotos\ community.
:
:% A BibTeX Bibliography for LOTOS, Ken Turner
:
:\subsection{A Bib\TeX\ Bibliography for \Lotos}{Ken Turner}{University of
:[email-masked]}
:
:With contributions from G\"unter Karjoth ([email-masked]) and others I
:have extended my Bib\TeX\ bibliography of \Lotos\ papers to about 350
:references. Until WELL is organised (see below) you can get the  
bibliography
:from me by email. Pepe Ma\~nas ([email-masked]) has also combined a
:version of my bibliography with his own and made it available via WAIS
:(wais://www.dit.upm.es:210/lotos).  This permits on-line searches, but
:currently needs more work to eliminate duplicates and to deal with
:abbreviations.
:
:I have written a shell script based on a Bib\TeX\ style file that
:automatically calculates labels for bibliographic entries based on  
surnames
:and year. If you have a favourite style of label, you could modify my  
script
:to generate that instead (in case you do not like my own style).
:
:% WELL - World-widE LOTOS Library, Ken Turner
:
:\subsection{WELL -- World-widE \Lotos\ Library}{Ken Turner}{University of
:[email-masked]}
:
:In the previous issue of \LotosNews\ I proposed making this available via
:WWW (World-Wide Web). The general response was positive, though we should
:not forget those with email but not Internet access. The best solution  
seems
:to be to allow ftp access as well, with email (via
:[email-masked]) used to circulate notifications of new
:additions.
:
:I had extensive email discussions with Axel Belinfante
:([email-masked]), Hubert Garavel ([email-masked]) and Pepe
:Ma\~nas ([email-masked]) about how best to make \Lotos\ information
:available via WWW. The following describes the current version of the
:proposal. The aim is to produce a common, world-wide, distributed  
repository
:of information about \Lotos\ (and E\Lotos). The repository will consist of  
a
:number of different elements including:
:
:\begin{center}
:
:\begin{tabular}{l l}
:Top-Level WWW Access & Axel Belinfante? \\
:Replicated Access Sites & Pepe Manas? \\
:Who's Who in the \Lotos\ Community & Dave Bustard? \\
:Frequently Asked Questions & Hubert Garavel? \\
:\Lotos\ News (past, current, future) & Ken Turner? \\
:Papers, Theses, Presentations, Tutorials, ... & Luigi Logrippo? \\
:Collected \Lotos\ Bibliography & Ken Turner? \\
:Example Specifications & Dave Bustard? \\
:E\Lotos\ documents & Juan Quemada? \\
:Pointers to Tool Information & Pepe Manas? \\
:comp.specification[.lotos]/lotos-world Link & Pepe Manas? \\
:\end{tabular}
:
:\end{center}
:
:For each topic, the name and email address of the relevant coordinator  
will
:be defined; several of the names above are tentative and not yet agreed.
:Extensive cross-links should exist (e.g.\ from `Who's Who' to individual
:site pages). The repository should be available via raw ftp and via  
network
:browsing (WWW, WAIS, ...). The repository should be organised to support  
all
:these forms of access (format to be agreed, including appropriate  
directory
:structure). The repository should be replicated across a number of sites,
:with one site designated as the master one for certain elements (procedure
:to be agreed).
:
:Initially comp.specification is recommended as the newsgroup for  
discussion.
:For the moment, Pepe Ma\~nas automatically feeds lotos-world into
:comp.specification. In time, it is hoped that a separate
:comp.specification.lotos could be justified; this would initially be
:unmoderated.
:
:%%% Work in Progress
:
:\section{Work in Progress}
:
:This section is devoted to announcements of new projects, project
:results, and position statements.
:
:% Enhancing Soft Systems Analysis with Formal (LOTOS) Modelling, Dave  
Bustard
:
:\subsection{Enhancing Soft Systems Analysis with Formal (\Lotos)
:Modelling}{Dave Bustard}{University of
:[email-masked]}
:
:A new requirements definition method for computing systems is currently
:under development at the University of Ulster. The method, known as RACE
:\cite{Bustard-1994} (Requirements Acquisition and Controlled Evolution),  
is
:being built around Checkland and WilsonUs Soft Systems Methodology (SSM)
:\cite{Wilson-1990} and one element of RACE is the use of formal modelling  
in
:\Lotos\ to clarify and help explore the implications of the systems being
:described. A full paper on this work is being presented at the IEEE
:Requirements Engineering T95 Symposium in York at the end of March
:\cite{Bustard-Lundy-1995}. This article gives a brief summary of the
:technique involved and a rationale for the use of formality in this case.
:
:SSM is a general problem-solving technique which has been used  
successfully
:in many computing application areas, including, in particular, the
:development of information systems. SSM seeks to identify the reasons why  
a
:system exists and consequently determine the activities that should be
:undertaken to achieve those purposes. The differences between these
:TconceptualU views of the problem situation and what is currently  
happening
:in practice gives the basis for determining and implementing system
:improvements. In practice, SSM establishes the business case for the
:introduction of a computing system.
:
:The need for formality arises because the SSM process produces models of
:system activity that are largely informal and therefore subject to
:misunderstanding.  This is made worse by the fact that there are often two
:analysts present: one performing the business analysis and one the
:subsequent computing analysis.  Overall, the introduction of formal
:techniques to the soft systems analysis process has been guided by four  
main
:principles:
:
:\begin{enumerate}
:
:\item
:The formal techniques used should complement the soft systems process in a
:support role \cite{Lundy-Bustard-1994}. That is, the formal techniques
:should enhance the process without introducing significant difficulties,  
so
:that the net benefit is obvious.
:
:\item
:As a corollary to (a), the use of formal modelling should be optional.   
This
:sets the rather ambitious target of providing formal support that analysts
:choose to use because they believe it is cost-effective rather than  
because
:it is 'required'.
:
:\item
:To help the cost-benefit equation, good use should be made of tool support
:to assist the construction, examination and maintenance of formal
:descriptions.
:
:\item
:The techniques used should concentrate on supporting soft systems analysis
:without considering the type of computing-oriented analysis to follow.  
Thus,
:for example, the formal techniques involved should be equally beneficial  
for
:Structured Analysis and Object-Oriented Analysis, without being unduly
:influenced by their specific requirements.
:
:\end{enumerate}
:
:The possible use of formal descriptions in the SSM process is shown in
:italics in the following summary of the four main SSM development phases:
:
:\begin{enumerate}
:
:\item
:understand the problem situation
:
:\item
:produce activity models
:
:\item
:refine activity models:
:
:\begin{enumerate}
:
:\item
:develop interactions models
:
:\item
:develop formal specifications and animate them to improve the analyst's
:understanding of the system being described
:
:\item
:validate the models with the client, discussing implications using  
animated
:specifications projected onto activity diagrams
:
:\end{enumerate}
:
:\item
:develop recommendations for change:
:
:\begin{enumerate}
:
:\item
:merge activity models, using automated assistance that takes advantage of
:the formal specifications of the activity models
:
:\item
:validate the merged model, using automated assistance to examine the  
merged
:model and to verify its consistency with individual models
:
:\item
:compare the merged model with the current problem situation to identify
:differences and make recommendations for change accordingly
:
:\end{enumerate}
:
:\end{enumerate}
:
:The research goal is to implement, evaluate and refine this 'formal  
method',
:to ensure its effectiveness and to better understand its limitations. The
:development is proceeding in three stages, each of which will bring  
benefit
:individually. The first two stages are in support of the third and fourth
:phases of analysis shown above and the third stage is concerned with
:developing links to computing-oriented analysis techniques. The first  
stage
:of the work is well advanced and tool development has begun. Evaluation  
and
:refinement of the proposed approach is proceeding in parallel, using  
manual
:techniques. This is being undertaken in collaboration with the Northern
:Ireland Civil Service, where SSM has been in use for several years. Tool
:support is extending the development of \Lotos\ animation and comparison
:tools produced in earlier projects
:\cite{Winstanley-Bustard-1991,Bustard-Winstanley-1994}.  Work to link SSM
:with Structured Analysis and Object-Oriented Analysis is also in progress
:and at some point in the future will be integrated with the formal  
modelling
:techniques to form the overall RACE Method.
:
:Space does not permit much to be said about how exactly how \Lotos\
:descriptions are developed so the interested reader is referred to the  
full
:paper. However, as a rough indication of what is involved, the process is
:largely one of transforming interaction models (similar to data flow
:descriptions) into \Lotos\ skeletons and then adding detail to those
:skeletons. The structure of the \Lotos\ description corresponds to the
:hierarchical structure of an interaction model, leading to a specification
:of the following form:
:
:\begin{comment}
:specification system_name: noexit
:  ... type definitions for data
:behaviour
:  ... instantiation of processes for elements of the top level interaction  
model
:where
:  ... definitions for above processes, mirroring the interaction model  
hierarchy
:endspec
:\end{comment}
:
:\begin{lotos}
:{\bf specification} system\_\,name: {\bf noexit}\\
:\hspace{1.0em}... type definitions for data\\
:{\bf behaviour}\\
:\hspace{1.0em}... instantiation of processes for elements of the top level
:interaction model\\
:{\bf where}\\
:\hspace{1.0em}... definitions for above processes, mirroring the  
interaction
:model hierarchy\\
:{\bf endspec}\\
:\end{lotos}
:
:%%% Conferences and Workshops
:
:\section{Conferences and Workshops}
:
:This section is devoted to calls for papers, announcements and reports of
:conferences, symposia, workshops and the like.
:
:% AMAST 95
:
:\subsection{Algebraic Methodology And Software Technology 95}{Pippo
:Scollo}{University of [email-masked]}
:
:The Preliminary Programme of the AMAST~95 Conference (4th International
:Conference on Algebraic Methodology And Software Technology, Montr\'eal,
:Canada, 3rd--7th July 1995) is available on the WWW at the following URL:
:
:\begin{verbatim}
:  http://www.cs.utwente.nl/data/amast/amast95/PreliminaryProgramme.txt
:\end{verbatim}
:
:The file includes abstracts of the invited talks, conference schedule,
:registration information and registration forms, and accommodation and
:travel information. The deadline for reduced registration fees is Monday  
5th
:June 1995.
:
:The file is also available by anonymous ftp:
:
:\begin{verbatim}
:  host:      ftp.cs.utwente.nl
:  username:  anonymous
:  password:  your e-mail address
:  directory: pub/doc/amast/amast95/
:  get file:  PreliminaryProgramme.txt
:\end{verbatim}
:
:More information about AMAST~95 is available from the following sources:
:
:\begin{itemize}
:
:\item
:For bulletins on current status of the conference: 

:
:\begin{verbatim}
:    [email-masked]
:    Tools and Demos: [email-masked]
:    Registration: [email-masked]
:    Local Arrangements: [email-masked]
:\end{verbatim}
:    

:\item
:For subscribing to AMAST~95 mailing list: [email-masked]
:
:\end{itemize}
:
:% FITSS III
:
:\subsection{Third International Workshop on Feature Interaction}{Kong Eng
:Cheng}{Royal Melbourne Institute of [email-masked]}
:
:\begin{centering}
:{\bf
:Third International Workshop on Feature Interactions \\
:in Telecommunications Software Systems \\
:\mbox{}\\
:Call for Participation \\
:\mbox{}\\
:Kyoto, Japan \\
:\mbox{}\\
:11th--13th October 1996 \\
:}
:\end{centering}
:
:\vspace{3ex}
:
:\subsubsection{Description}
:
:This workshop is the third in a series,  whose  mission
:is  to  encourage  researchers  from  a  variety of computer
:science  specialities   (software   engineering,   enterprise
:modeling,   protocol   engineering,  distributed  artificial
:intelligence,  formal  techniques,  software  testing,   and
:distributed systems, among others) to apply their techniques
:to the feature interaction problem that arises  in  building
:telecommunications software systems (see the back page for a
:description of the problem).  We welcome papers on avoiding,
:detecting,   and/or  resolving  feature  interactions  using
:either analytical or structural approaches.  Submissions are
:encouraged  in  (but are not limited to) the following topic
:areas:
:
:\begin{itemize}
:
:\item
:Classification of feature interactions.
:
:\item
:Modeling,  reasoning,  and  testing  techniques  for detecting feature
:interactions.
:
:\item
:Software platforms and architecture designs  to  aid in   avoiding,
:detecting,  and  resolving  feature interactions.
:
:\item
:Tools  and  methodologies  for  promoting   software compatibility and
:extensibility.
:
:\item
:Mechanisms   for   managing   feature   interactions throughout the  
service
:life-cyle.
:
:\item
:Management of feature interactions in PCS, ISDN, and Broadband services,  
as
:well as IN services.
:
:\item
:Management of feature interactions in various of the operations   support
:functions   such  as  Service Negotiation,   Service   Management,   and
:Service Assurance.
:
:\item
:Feature Interactions and their potential  impact  on system Security and
:Safety.
:
:\item
:Environments  and  automated   tools   for   related problems in other
:software systems.
:
:\item
:Management of Feature Interactions in various  other enterprises, such as
:banking, medicine, etc.
:
:\end{itemize}
:
:\subsubsection{Workshop Statement}
:
:The feature interaction problem is a major obstacle  to the rapid  
deployment
:of new telephone services. Some feature communications system.
:Telecommunications software is  huge, real-time,   and  distributed;
:adding  new  features  to  a telecommunication system, like adding new
:functionalities to any  large software system, can be very difficult.   
Each
:new feature may interact with many  existing  features,  causing customer
:annoyance    or    total    system    breakdown.  Traditionally,
:interactions were detected and resolved on  a feature by feature basis by
:experts who are knowledgeable on all existing features.  As the number of
:features  grows  to satisfy   diverse   needs  of  customers,  managing
:feature interactions  in   a   single   administrative   domain   is
:approaching   incomprehensible   complexity.   In  a  future marketplace
:where features deployed in the  network  may  be developed   by    
different
:operating  companies  and  their associated vendors, the traditional
:approach  is  no  longer feasible.   How  to  detect,  resolve,  or  even
:prevent the occurrence of feature interactions in an open network is now  
an
:important research issue.
:
:The  feature  interaction   problem   is   not   unique   to
:telecommunications    software;    similar    problems   are encountered  
in
:any long-lived software system that  requires frequent   changes   and
:additions  to  its  functionality.  Techniques in many related areas  
appear
:to be applicable  to the    management   of   feature   interactions.
:Software methodologies  for  extensibility  and  compatibility,   for
:example,  could  be useful for providing a structured design that can
:prevent many feature interactions  from  occurring.  Features are  
typically
:design to suit the purposes of a user or business, hence Enterprise  
modeling
:will play a  role  in the  identification  of  certain  classes of
:interaction, in particular the solution of an interaction in one   
enterprise
:may   not  be  desired  by  another.  Formal  specification, verification,
:and testing techniques, being widely  used  in protocol engineering and
:software engineering, contribute to the  detection  of  interactions.
:Several  causes  of  the problem,  such  as aliasing, timing, and the
:distribution of software components, are similar to  issues  in   
distributed
:systems.   Cooperative problem solving, a promising approach for
:resolving   interactions   at   run   time,   resembles distributed
:planning and resolution of conflicting subgoals among multiple agents in  
the
:area of distributed  artificial intelligence.   This workshop aims to
:provide an opportunity for participants to share ideas  and  experiences
:in  their respective  fields,  and  to  apply  their  expertise to the
:feature interaction problem.
:
:\subsubsection{Format}
:
:We hope to promote  a  dialogue  among  researchers  in various related
:areas, as well as the designers and builders of telecommunications  
software.
:To this  end,  the  workshop will   have  sessions  for  paper
:presentations,  including relatively long discussion periods.  Panel
:discussions  and tool  demonstrations  are also planned. The first day of
:the workshop,  October  11,  is   devoted   to   tutorials   and  
discussions
:on areas related to feature interactions.
:
:\subsubsection{Attendance}
:
:Workshop attendance will  be  limited  to  100  people.  Attendance will  
be
:by invitation only. Prospective attendees are asked to submit either a  
paper
:(maximum 5000 words) or a single  page  description  of  their  interests
:and how they relate  to  the  workshop.  Proposals  for   tutorials   and
:discussions  are  also requested (maximum 3000 words). About 16-20 of the
:attendees will be asked to  present  talks;  a small  number  of   
tutorials
:and/or discussions will also be selected.  We will strive for an equal   
mix
:of  theoretical results  and practical experiences. Papers will be  
published
:in a conference proceedings.
:
:\subsubsection{Further Information}
:
:\begin{raggedright}
:Kong Eng Cheng \\
:Department of Computer Science \\
:Royal Melbourne Institute of Technology \\
:GPO Box 2476V \\
:Melbourne, Victoria \\
:AUSTRALIA 3001 \\
:\mbox{} \\
:E-mail: [email-masked] \\
:Tel: +61 3 660 3266 \\
:FAX: +61 3 662 1617 \\
:\end{raggedright}
:
:\subsubsection{Workshop Co-Chairpersons}
:
:\begin{raggedright}
:Tadashi Ohta (ATR, Japan) \\
:Nancy Griffeth (Bellcore, USA) \\
:Kong Eng Cheng  (Royal Melbourne Institute of Technology, Australia) \\
:E. Jane Cameron (Bellcore, USA) \\
:\end{raggedright}
:
:\subsubsection{Program Committee}
:
:\begin{raggedright}
:Jan Bergstra         (CWI and University of Amsterdam, The Netherlands) \\
:Ralph Blumenthal     (Bellcore, USA) \\
:Rolv Braek           (SINTEF DELAB, Norway) \\
:Bernie Cohen         (City University of London, UK) \\
:Robert France        (Florida Atlantic University, USA) \\
:Haruo Hasegawa       (OKI, Japan) \\
:Dieter Hogrefe       (University of Bern, Switzerland) \\
:Richard Kemmerer     (UCSB, USA) \\
:Victor Lesser        (University of Massachusetts, USA) \\
:Yow-Jian Lin         (Bellcore, USA) \\
:Luigi Logrippo       (University of Ottawa, Canada) \\
:Jan van der Meer     (Ericsson, The Netherlands) \\
:Robert Milne         (BNR, UK) \\
:Leo Motus            (Tallinn Technical University, Estonia) \\
:Jacques Muller       (CNET, France) \\
:Jan-Olof Nordenstam  (ELLEMTEL, Sweden) \\
:Yoshihiro Niitsu     (NTT, Japan) \\
:Ben Potter           (University of Hertfordshire, UK) \\
:Henrikas Pranevicius (Kaunas University of Technology, Lithuania) \\
:Martin Sadler        (HP, UK) \\
:Jean-Bernard Stefani (CNET, France) \\
:Greg Utas            (BNR, USA) \\
:Jyri Vain            (Institute of Cybernetics, Estonia) \\
:Hugo Velthuijsen     (PTT Research, The Netherlands) \\
:Yasushi Wakahara     (KDD R\&D Laboratories, Japan) \\
:Ron Wojcik           (BellSouth, USA) \\
:Pamela Zave          (AT\&T Bell Laboratories, USA) \\
:\end{raggedright}
:
:% FM-OODS 96
:
:\subsection{Formal Methods for Open Object-based Distributed Systems
:96}{Andreas Vogel}{Distributed Systems Technology  
[email-masked]}
:
:\begin{centering}
:{\bf
:FM-OODS 96 \\
:Call for Papers \\
:\mbox{}\\
:Formal Methods for Open Object-based Distributed Systems 96 \\
:\mbox{}\\
:Paris, France \\
:\mbox{}\\
:4th--6th March 1996 \\
:}
:\end{centering}
:
:\vspace{3ex}
:
:\subsubsection{Objectives}
:
:Object-based  Distributed Computing is being established as the most
:pertinent basis for the support of large, heterogeneous computing and
:telecommunications systems. Indeed, several important international
:organisations,  such as ITU, ISO, OMG, TINA-C, ... are defining similar
:distributed object-based frameworks as a foundation for open distributed
:computing.
:
:The advent of Open Object-based Distributed Systems - OODS - brings new
:challenges and opportunities for the use and development of formal  
methods.
:New architectures and system models are emerging (e.g., the enterprise,
:information, computational and engineering viewpoints of the ITU-T/ISO/IEC
:ODP Reference Model) which may require formal notational support. Usual
:design issues such as specification, verification, refinement, and testing
:need to take into account new dimensions introduced by distribution and
:openness, such as quality of service and dependability constraints,  
dynamic
:binding and reconfiguration, consistency between multiple models and
:viewpoints, etc. OODS is a challenging research context and a source of
:motivation for semantical models of object-based systems and notations
:(e.g.\ concurrent and distributed OO languages), for the evolution of
:standardised formal description techniques (e.g.\  SDL, \Lotos, Estelle,  
Z,
:...), for the application and assessment of logic based approaches
:(e.g.\ temporal logic, TLA, ...),  and for the further development and use
:of Object Oriented methodologies and tools (OMT, HOOD, Fusion,
:...).
:
:The objective of FM-OODS is to provide an integrated forum for the
:presentation of research in several related fields, and the exchange of
:ideas and experiences in the topics concerned with the formal methods
:support for Open Object-based Distributed Systems.
:
:\subsubsection{Topics}
:
:Topics of interest of the workshop include but are not restricted to:
:
:\begin{itemize}
:
:\item
:formal models for object-based distributed computing
:
:\item
:semantics of object-based distributed programming languages
:
:\item
:formal techniques in object-based and object-oriented analysis and design
:
:\item
:refinement and transformation of specifications
:
:\item
:multiple viewpoint modelling and consistency between different models
:
:\item
:formal techniques in distributed systems verification and testing
:
:\item
:types, service types and subtyping
:
:\item
:specification, verification and testing of quality of service constraints
:
:\item
:formal methods and object life cycle
:
:\end{itemize}
:
:\subsubsection{Organisers}
:
:\begin{verbatim}
:Elie NAJM                        Jean-Bernard STEFANI
:[email-masked]                 [email-masked]
:Tel: + 33 1 45 81 77 09          Tel: +33 1 45 29 59 87
:Fax: + 33 1 45 89 16 64          Fax: +33 1 45 29 66 04
:ENST                             CNET  France Telecom
:Networks Department              PAA/TSA
:46, Rue Barrault                 38-40 rue du general Leclerc
:75013 Paris, FRANCE              92131 Issy-Les-Moulineaux, FRANCE
:\end{verbatim}
:
:% FORTE 95
:
:\subsection{Formal Description Techniques 95}{Daniel Ouimet}{University of
:Montr\[email-masked]}
:
:\begin{centering}
:{\bf
:FORTE 95 \\
:Call for Papers \\
:\mbox{}\\
:IFIP TC6/WG6.1 Eighth International Conference on \\
:Formal Description Techniques \\
:for Distributed Systems and Communications Protocols \\
:\mbox{}\\
:Montr\'eal (Quebec), Canada \\
:\mbox{}\\
:17th--20th October 1995 \\
:}
:\end{centering}
:
:\vspace{3ex}
:
:\subsubsection{Objective and Scope}
:
:FORTE~95 will address Formal Description Techniques (FDTs) applicable to
:Distributed Systems such as Estelle, Lotos, SDL, ASN.1, Z, Automata,  
Logics,
:Process, Algebras, etc., and will include industrial applicability to
:Protocols and Distributed Systems. The conference will be a forum for
:presentation of the state of the art in theory, application, tools and
:industrialization of (FDTs) and will provide an excellent orientation for
:newcomers. Research papers and industrial usage reports as well as  
proposals
:for tutorials (advanced technology seminars), poster displays and tool
:demonstrations are solicited. Topics of interests include (but are not
:restricted to) the following areas:
:
:\begin{itemize}
:
:\item
:FDT-based software engineering
:
:\item
:Design and implementation
:
:\item
:Methodologies and architectures
:
:\item
:Verification and validation
:
:\item
:Comparative analyses of FDTs
:
:\item
:Testing
:
:\item
:Extensions of FDTs
:
:\item
:Tools and tool support
:
:\item
:Real-time and probability aspects
:
:\item
:Practical experience and case studies
:
:\item
:Examples and analyses of formal descriptions
:
:\item
:Corporate strategic and financial consequences of FDT use.
:
:\end{itemize}
:
:FORTE~95 will be sponsored by IFIP WG6.1. It will start with one day of
:tutorials and advanced technology seminars on 17th October 1995 and will
:continue with three days of technical presentations. Tool presentations  
and
:poster displays will be offered throughout all four days of FORTE~95.
:
:\subsubsection{Important Dates}
:
:30th April 1995: Submission deadline
:
:15th July 1995: Notification of acceptance
:
:30th August 1995: Camera ready copy for participants proceedings due
:
:\subsubsection{Conference Co-Chairs}
:
:G. von Bochmann, R. Dssouli and O. Rafiq
:
:\subsubsection{Program Committee}
:
:P. Amer (Univ. of Delaware, USA), T. Bolognesi (CNUCE, Italy), J. Bowen
:(Univ. of Oxford, UK), E. Brinksma (Univ. of Twente, Netherlands), A.
:Cavalli (INT, France), S.T. Chanson (Univ. of Science and Technology, Hong
:Kong), J-P. Courtiat (LAAS, France), P. Dembinski (Academy of Science,
:Poland), J. deJMeer (GMD FOKUS, Germany), M. Ferguson (INRS, Canada), R.
:Gotzhein (Univ. of Kaiserslautern, Germany), M. Gouda (Univ. of Texas,
:Austin, USA), R. Groz (CNET, France), D. Hogrefe (Univ. of Bern,
:Switzerland), Y. Hirakawa (NTT, Japan), G. Holzmann (AT\&T, USA), T. Kato
:(KDD, Japan), L. Kovacs (CAI, Hungaria), J. Kroon (PTT Research,
:Netherlands), G. Leduc (Univ. of Lige, Belgium), L. Logrippo (Univ. of
:Ottawa, Canada), G. Luo (BNR, Canada), L. Marshall (BNR, Canada), E. Najm
:(ENST, France), A. Obaid (UQAH, Canada), K. Parker (Telecom Research Lab.,
:Australia), A. Petrenko (Univ. of Montr\'eal, Canada), J. Quemada  
(Technical
:Univ. of Madrid, Spain), S. V. Raghavan (IIT, Madras, India), H. Rudin  
(IBM,
:Switzerland), K. Turner (Univ. of Stirling, UK)
:
:\subsubsection{Submissions Solicited}
:
:Full original research papers and industrial usage reports, 5 copies, up  
to
:16 pages (including bibliography), 12 point, single spaced, including an
:informative abstract as well as names and affiliations of all authors, and  
a
:list of keywords facilitating the assignment of papers to referees. A  
cover
:letter naming a contact author (including postal and email address) and
:indicating the preferred category (research paper or industrial usage
:report) in which the paper should be considered, is required. The cover
:letter should also state that the paper has not been presented in any
:language at another conference nor is it currently being considered by
:another conference or by a journal. Authors may propose a list of Program
:Committee members whom they consider to be particularly qualified to  
review
:their submission. Only those papers presented by an author during FORTE~95
:will be included in the final proceedings which will be published by the
:official publisher of IFIP WG6.1.
:
:Proposals for tool demonstrations (including hardware and software
:requirements), poster displays, tutorials and advanced technology  
seminars.
:
:All submissions should be sent to:
:
:\begin{raggedright}
:Prof. Rachida Dssouli \\
:D\'epartement d'IRO \\
:Universite de Mont\'real \\
:Pavillon des sciences mathematiques et informatiques \\
:C.P. 6128 Succursale Centre-Ville \\
:(2920 Chemin de la Tour) \\
:Montr\'eal, (Quebec) \\
:Canada H3C 3J7 \\
:Tel. : (514) 343 7599, Fax : (514) 343 5834 \\
:Email: [email-masked] \\
:\end{raggedright}
:
:\subsubsection{For Further Information}
:
:\begin{raggedright}
:Lucie Levesque \\
:D\'epartement d'IRO \\
:Universite de Montr\'eal \\
:Pavillon des sciences mathematiques et informatiques \\
:2900, blvd Edouard-Montpetit \\
:(2920 Chemin de la Tour) \\
:Montr\'eal, (Quebec) \\
:Canada H3T 1J4 \\
:Tel. : (514) 343 6111 (ext. 3520), Fax : (514) 343 5834 \\
:Email: [email-masked] \\
:\end{raggedright}
:  

:% PROMELA/SPIN Workshop
:
:\subsection{PROMELA/SPIN Workshop}{Daniel Ouimet}{University of
:Montr\[email-masked]}
:
:\begin{centering}
:{\bf
:Workshop on PROMELA/SPIN \\
:(preliminary announcement) \\
:\mbox{}\\
:Montr\'eal (Quebec), Canada \\
:\mbox{}\\
:16th October 1995 (just before FORTE~95) \\
:}
:\end{centering}
:
:\vspace{3ex}
:
:SPIN is a reachability analysis tool designed for the general verification
:of distributed systems.  First made available publicly in 1991, a  
completely
:new version new version has recently been released.  SPIN is used both for
:teaching and for industrial applications.  It has inspired many other  
tools
:in various ways.
:
:This workshop aims at bringing together the community of users and
:researchers interested in SPIN as a tool, as well as an experimentation or  
a
:research vehicle.  It will be an opportunity to discuss the current status
:of the tool, and the evolution of SPIN.
:
:We have identified the following areas of interest for this workshop:
:
:\begin{itemize}
:
:\item
:bottlenecks in the practical application of verification technology and
:possible solutions that could be adopted in tools such as SPIN
:
:\item
:effective methods for, and practical experience with, the modeling
:verification of large systems with SPIN
:
:\item
:algorithmic improvements that should be considered
:
:\item
:new types of verification
:
:\item
:integration of SPIN with other tools, such as theorem provers, hardware
:design tools, code generators etc.
:
:\item
:a panel on possible extensions of SPIN
:
:\end{itemize}
:
:Further suggestions are most welcome.
:
:Participants are invited to present a position statement to be presented  
and
:discussed at the workshop.
:
:Workshop Organizer: INRS-T\'el\'ecommunications
:
:All Correspondence: [email-masked]
:
:% PSTV XV
:
:\subsection{Protocol Specification, Testing and Verification XV}{Piotr
:Dembinski}{Polish Academy of [email-masked]}
:
:\begin{centering}
:{\bf
:PSTV 95 \\
:Preliminary Programme \\
:\mbox{}\\
:IFIP TC6/WG6.1 Fifteenth International Symposium on \\
:Protocol Specification, Testing and Verification \\
:\mbox{}\\
:With support from European Commission\\
:\mbox{}\\
:Warsaw, Poland \\
:\mbox{}\\
:13th--16th June 1995 \\
:}
:\end{centering}
:
:\vspace{3ex}
:
:\subsubsection{Information, Program and Registration}
:
:PSTV~95 information, registration form and program can be ftp'ed from
:ftp.ipipan.waw.pl, userid `anonymous' and password email address, from the
:directory pub/konferencje/pstv95.
:
:PSTV symposia have served for fifteen years as a premier forum for
:researchers and practitioners in industry and academia interested in  
theory
:and application of formal methods in specifying, testing and verifying
:communication protocols and services.  For the first time the PSTV  
Symposium
:is held in Central Europe. Hence it creates an ideal possibility for
:extending the international co-operation, in this very important domain of
:protocol engineering, to this and eastern part of the continent. Also, it
:offers a forum for presentation and promotion of research being done in  
this
:part of Europe.
:
:PSTV~95 is organized jointly by the Institute of Computer Science of the
:Polish Academy of Sciences (IPI PAN) and the Institute of  
Telecommunications
:of the Warsaw University of Technology (IT PW).  The symposium Proceedings
:will be published in the IFIP series by Chapman \& Hall. PSTV~95 starts  
with
:one day tutorials and continues with three days of technical  
presentations.
:
:\subsubsection{Symposium Co-Chairpersons}
:
:\begin{verbatim}
:Piotr Dembinski                 Marek Sredniawa
:IPI PAN                         IT PW
:Ordona 21,                      Nowowiejska 15/19
:01-237 Warsaw, Poland           00-665 Warsaw, Poland
:Tel. +48 22 362841              Tel. +48 22 259820
:Fax. +48 22 376564              Fax. +48 22 254950
:E-mail: [email-masked]    E-mail: [email-masked]
:\end{verbatim}
:
:\subsubsection{Program Committee}
:
:\begin{raggedright} 

:P. Amer (University of Delaware, USA),  \\ 

:A. Blikle (Acad. of Sci., PL),  \\ 

:G. von Bochmann (University of Montr\'eal, CND),  \\ 

:T. Bolognesi (CNUCE, I),  \\ 

:E. Borcoci (University of Bucharest, R),  \\ 

:E. Brinksma (University of Twente, NL),  \\ 

:S. Budkowski (INT, F),  \\ 

:W. Cellary (EFP, PL),  \\ 

:S. Chanson (University of British Columbia, CND),  \\ 

:G. Csopaki (University of Budapest, H),  \\ 

:M. Diaz (LAAS, F),  \\ 

:D. Hogrefe (University of Bern, CH),  \\ 

:G. Holzmann (Bell Labs, USA),  \\ 

:K. Inan (Middle East Techn. University, TR),  \\ 

:P. Kritzinger (University of Cape Town, ZA),  \\ 

:R. Lai (La Trobe University, AUS),  \\ 

:G. Leduc (University of Liege, B),  \\ 

:L. Logrippo (University of Ottawa, CND),  \\ 

:J. Lubacz (University of Warsaw, PL),  \\ 

:M. Malek (Humboldt University, D),  \\ 

:J. de Meer (GMD, D),  \\ 

:T. Mizuno (Shizuoka University, J),  \\ 

:V. Nepomniashy (Acad. of Sci., RUS),  \\ 

:J. Quemada (University of Madrid, S),  \\ 

:O. Rafiq (University of Pau, F),  \\ 

:H. Rudin (IBM Zurich, CH),  \\ 

:W. Sobczak (University of Gdansk, PL),  \\ 

:R. Tenney (University of Massachusetts, USA),  \\ 

:M. Tienari (University of Helsinki, SF),  \\ 

:K. Turner (University of Stirling, UK),  \\ 

:S. Vuong (University of  British Columbia, CND). \\ 

:\end{raggedright}
:
:\subsubsection{Administrative Secretariat}
:
:\begin{raggedright} 

:Ms. Ewa Gasiorowska \\ 

:IPI PAN  \\ 

:Ordona 21, \\ 

:01-237 Warsaw, Poland \\ 

:Tel. +48 22 362841, Fax. +48 22 376564 \\ 

:E-mail: [email-masked] \\ 

:\end{raggedright}
:
:\subsubsection{Programme}
:
:\paragraph{Tuesday 13th June}
:
:\begin{verbatim} 

:8:00-9:00       Registration
:9:00-12:30      Tutorial I: 

:                Formal design and implementation of high 

:                speed multimedia protocols
:                Michel Diaz, LAAS/CNRS, Toulouse
:
:                First, the tutorial presents constraints that exist in  

:                distributed multimedia systems and a general view at 

:                high speed and multimedia networks. Then a formal       

:                approach is proposed for representing synchronisation in 

:                multimedia objects based on different Petri Net models 

:                such as:Time and Hierarchical Time Stream Petri Nets. 

:                Finally, a new concept of `partial order connection' is 

:                presented and is shown to be a more adequate and general 

:                solution for designing and implementing high speed      

:                transfer multimedia protocols than usual connexion      

:                oriented or connectionless protocols.
:                

:12:30-14:00     LUNCH
:
:14:00-17:30     Tutorial II
:                Formal Methods in Conformance Testing
:                Finn Kristoffersen, Tele Danmark Research, Horsholm
:                Marc Phalippou, France Telecom - CNET, Lannion
:                Jan Tretmans, University of Twente, Enschede
:
:                The emerging standard `Formal Methods in        

:                Conformance Testing' defines a framework, independent 

:                of any formal description technique, for conformance 

:                testing based on formal specifications. An overview of 

:                this framework is presented by showing how the FDTs 

:                Estelle, LOTOS, and SDL fit within it. Concepts like 

:                conformance to a formal specification, test generation, 

:                fault model, and test selection, which are defined      

:                abstractly within the framework, are applied to these   

:                three FDTs.
:
:18:00-20:00     WELCOME RECEPTION
:\end{verbatim}
:
:\paragraph{Wednesday 14th June}
:
:\begin{verbatim}
:8:00-8:45       Registration
:8:45-9:00       Opening Remarks: P. Dembinski and M.  Sredniawa
:9:00-10:30      Session 1: Specification & Verification: 

:                           Time-dependent Analysis
:
:                Simple On-the-fly Automatic Verification of Linear      

:                Temporal Logic
:                R. Gerth, Technical University Eindhoven, 

:                The Netherlands
:                D. Peled, AT&T Bell Lab., USA
:                M.Y. Vardi, Rice University, USA
:                P. Wolper, Universite de Liege, Belgium
:
:                Specifying Real-Time Requirements for SDL       

:                Specifications - a Temporal Logic-Based Approach
:                S. Leue, University of Berne, Switzerland
:
:                A Temporal Reachability Analysis
:                L. Cacciari, O. Rafiq, University of Pau, France
:
:10:30-11:00     BREAK
:
:11:00-13:00     Session 2: Specification of Concurrent Systems
:
:                Invited Talk: `True' versus `Artificial' Concurrency
:                Antoni Mazurkiewicz, Academy of Sciences, Poland
:
:                Action refinement and fairness are discussed for        

:                concurrent systems with their behaviour represented either 

:                by a set of action sequences (`artificial' concurrency  

:                representation), or by a family of partially ordered sets 

:                (`true' concurrency representation). The behaviour of a 

:                refined system is compared with the refinement of the 

:                original system behaviur, for both representations. Then, 

:                it is argued that there is no need for fairness notion in  
the 

:                `true' concurrency framework.
:
:                On Compositionality and Petri Nets in Protocol  

:                Engineering
:                N. A. Anisimov, Academy of Sciences, Russia
:                M. Koutny, University of Newcastle, United Kingdom
:
:                Composition of LOTOS Specifications
:                M. Steen, H. Bowman, J. Derrick, University of Kent, 

:                United Kingdom
:
:13:00-14:30     LUNCH
:
:14:30-16:00     Session 3: Testing
:
:                Principles for validation of abstract test suites  
specified in 

:                concurrent TTCN
:                M. Toro, K. Tarnay, KFKI Budapest, Hungary
:
:                An Approach for Testing Distributed Software Systems
:                A. Ulrich, S. T. Chanson, University of Technology,     

:                Hong Kong
:
:                Modeling Basic LOTOS by FSMs for Conformance    

:                Testing
:                Q.M. Tan, A. Petrenko, G.v. Bochmann, University of 

:                Montreal, Canada
:
:16:00-16:30     BREAK
:
:16:30-18:00     Session 4: Specification & Verification:
:                           Temporal Approach
:
:                The Specification and Verification of an Experimental 

:                ATM Signalling Protocol
:                D. Barnard, Siemens AG, Germany
:                S. Crosby, University of Cambridge, United Kingdom
:
:                Re-Usable Verification Elements for High-Speech         

:                Transfer Protocol Configurations
:                P. Herrmann, H. Krumm, University of Dortmund,  

:                Germany
:
:                An Algebraic-Temporal Specification of a CSMA/CD-
:                Protocol
:                M. Jmaiel, TU Berlin, Germany
:\end{verbatim}
:
:\paragraph{Thursday 15th June}
:
:\begin{verbatim}
:9:00-10:30      Session 5: Validation & Testing
:
:                Validation, Verification and Implementation of Timed 

:                Protocols using AORTA
:                S. Bradley, W. Henderson, D. Kendall, A. Robson,        

:                University of Northumbria, United Kingdom
:
:                Validation in Context
:                L. Heerink, E. Brinksma, University of Twente, 

:                The Netherlands
:
:                Characterizing Termination in LOTOS via Testing
:                D. Frutos, M. Nunez, University of Madrid, Spain
:                J. Quemada, Polytechnic of Madrid, Spain
:
:10:30-13:30     BREAK
:
:                This year, Corpus Christi, a holy day solemnly celebrated 

:                by Catholics in Poland, falls on Thursday, June 15. Big 

:                crowds attend colourful outdoor processions organized by 

:                churches all over Poland. A central ceremony takes place 

:                in the streets of the old part of Warsaw in the proximity 

:                of the Symposium venue. The organizers decided to break 

:                the conference to give an opportunity for participants to 

:                have a look at this, specifically Polish, old custom.  

:
:13:30-14:30     LUNCH
:
:14:30-16:00     Session 6: Specification & Analysis
:
:                Quantified reduced views of state graphs using  

:                Markovian and timed observational equivalence
:                K. Drira, LAAS/CNRS Toulouse, France
:                Y. Atamna, West Virginia University, USA
:                G. Juanole,  LAAS/CNRS Toulouse, France
:
:                SDL and Petri Net Performance Analysis of               

:                Communicating Systems
:                F. Bause, P. Kemper, University of Dortmund, Germany
:                H. Kabutz, P. Kritzinger, University of Cape Town, 

:                South Africa
:
:                On the Introduction of Gate Typing in E-LOTOS
:                H. Garavel, INRIA Rhone-Alpes, France
:
:16:00-16:30     BREAK
:
:16:30-18:00     Panel Discussion
:
:19:00-23:00     BANQUET
:\end{verbatim}
:
:\paragraph{Friday 16th June}
:
:\begin{verbatim}
:9:00-10:30      Session 7: Verification: Model Checking
:
:                An Analysis of Bitstate Hashing
:                G.J. Holzmann, AT&T Bell Lab., USA
:
:                Using Asynchronous Buchi Automata for Efficient         

:                Automatic Verification of Concurrent Systems
:                D. Peled, AT&T Bell Lab., USA
:                W. Penczek, University of Eindhoven, The Netherland s 

:                and Academy of Sciences, Poland
:
:                A Method to Build Symbolic Representations of LOTOS 

:                Specifications
:                R. Sisto, Polytechnic of Torino, Italy
:
:10:30-11:00     BREAK
:
:11:00-13:00     Session 8: High Speed / Multimedia
:
:                Invited Talk: Design, specification and verification of a 

:                N-connection dynamic membership for cooperative         

:                groups 

:                Michel Diaz, LAAS/CNRS Toulouse, France
:
:                A model for basic cooperation, based on information     

:                sharing between agents, is introduced. The model allows 

:                the users to define dynamic cooperative groups whose 

:                structure changes in time. A communication service and 

:                an associated protocol, managing cooperative dynamic N-
:                connection group, is then presented. The protocol has 

:                been verified using VAL, a multi-agent environment 

:                based on Petrri nets and then translated into Estelle for 

:                automatic implementation using EDT (Estelle     

:                Development Tool). 

:
:                On the Suitability of Estelle for Multimedia Systems
:                S. Fisher, University of Mannheim, Germany
:
:                Protocol Analysis and Verification Methods, Application 

:                to the Xpress Transfer Protocol 4.0
:                O. Catrina, Polytechnic of Bucarest, Romania
:
:13:00-14:30     LUNCH
:
:14:30-16:00     Session 9: Towards Implementation
:
:                PARES - a Portable Parallel Estelle Compiler
:                R. Plato, T. Held, University of Mgdeburg, Germany
:                H. Koenig, Cottbus University of Technology, Germany
:
:                A Methodology to the Implementation of Distributed 

:                Systems in Hardware from a Formal Description
:                L. Pirmez, A.C.P. Pedroza, A.C. Mesquita, University of 

:                Rio de Janeiro, Brazil
:
:                Hardware Specification Generated from Estelle
:                J. Wytrebowicz, INT Evry, France, and  Warsaw   

:                University of Technology, Poland
:
:16:00           Closing
:\end{verbatim}
:
:\subsubsection{General Information}
:
:The Symposium will take place in conference rooms of Palac Staszica 

:(Palace of Staszic) -- an XIX century, classical style, building belonging  
to 

:the Polish Academy of Sciences and located in the center of Warsaw on an 

:old route crossing the town from North to South along the Vistula river. A 

:Kopernik monument in front of the palace is a characteristic point in 

:Warsaw.
:
:The address is:
:
:\begin{raggedright}
:Palac Staszica \\
:ul. Nowy Swiat 72 \\
:00-330 WARSAW \\
:\end{raggedright}
:
:\subsubsection{Registration}
:
:Tutorials only: tutorial sessions, tutorial notes, coffee breaks and  
lunch.
:
:Conference only: conference sessions, conference proceedings, coffee 

:breaks, lunches, welcome reception, and banquet
:
:Full: tutorial and conference sessions, tutorial notes and conference 

:proceedings, coffee breaks, lunches, welcome reception, and banquet
:
:Early registration: Early fee deadline is May 20, 1995. 

:
:Payment: Registration fees can be paid either by a Banker's Cheque payable 

:to `IPI PAN PSTV~95' (personal cheques will not be accepted) or by a bank 

:transfer to: BPH Krakow XIV O/W-wa, Al. Jerozolimskie 7, 00-495 Warsaw,  
Poland
:Account no. 320007-2408
:
:Registration fees from outside Poland are to be paid in US Dollars only.  
At 

:site you can pay in cash (also in Polish currency `zloty') or by major  
credit 

:cards (Visa, MasterCard, EuroCard or Diners Club). However, paying by 

:card you will be charged additional 5\% of bank commission.
:
:Cancellation: Cancellation received later than 5th June will be charged  
US\$ 

:50 handling fee. 

:
:\subsubsection{Accommodation}
:
:A number of rooms have been reserved in different category hotels, all of 

:them within walking distance from the conference venue (Palac Staszica). 

:All rooms are with bath or shower.
:
:Please indicate your accommodation preferences completing the 

:Registration and Accommodation Form (you may indicate other 

:preferences than listed). Requests will be honoured in the order received.  
If 

:your choice is not available, we will make an effort to find a comparable 

:accommodation.
:
:Payment: Accommodation charges will be paid directly to the hotel by each 

:participant. It can be paid by cash (in Polish zloty).  Most hotels accept 

:major credit cards as well. Detailed information will be sent separately  
to 

:each registered participant.
:
:\subsubsection{Transportation}
:
:Warsaw  is easily reachable from all parts of the world and by all means  
of 

:transportation. There are several direct air connections from many cities  
in 

:Europe, USA and elsewhere. It takes some 20 minutes by a shuttle bus 

:(recommended) or taxi to get from the airport to the city center.
:
:\subsubsection{Visas}
:
:Citizens of the USA and most European countries do not need any visa. 

:Please check with your local Polish consulate if you need a visa.
:
:\subsubsection{Financial Support}
:
:Due to a special grant obtained from European Commission, the organizers 

:are able to offer a number of stipends to enable participation in the 

:PSTV~95 Symposium for persons from Central and Eastern Europe. The 

:stipends, in principle, serve to cover the registration fee. Other  
expenses 

:can be covered only as possible. Those willing to apply for such a stipend 

:should complete the special application form and send it together with  
their 

:registration as soon as possible. Priority is reserved for those who have 

:their paper accepted.
:
:\begin{comment}
:
:%%% Training
:
:\section{Training}
:
:This section is devoted to courses and books on \Lotos\ and its  
applications.
:
:\end{comment}
:
:%%% Abstracts of Papers and Theses
:
:\section{Abstracts of Papers and Theses}
:
:This section is devoted to abstracts of published papers, theses and
:dissertations related to \Lotos.
:
:% Rigorous Object-Oriented Analysis, Ana Moreira
:
:\subsection{Rigorous Object-Oriented Analysis}{Ana Moreira}{New
:University of [email-masked]}
:
:\ednote{The following Ph.D. thesis is available as Technical Report
:CS-TR~132 from the University of Stirling. Paper copies can be obtained at
:cost of copying from Moira Taylor: [email-masked].}
:
:Object-oriented methods for analysis, design and programming are commonly
:used by software engineers.  Formal description techniques, however, are
:mainly used in a research environment.  We have investigated how rigour  
can
:be introduced into the analysis phase of the software development process  
by
:combining object-oriented analysis (OOA) methods with formal description
:techniques.  The main topics of this investigation are a formal
:interpretation of the OOA constructs using LOTOS, a mathematical  
definition
:of the basic OOA concepts using a simple denotational semantics and a new
:method for object-oriented analysis that we call the Rigorous
:Object-Oriented Analysis method (ROOA).
:
:The \Lotos\ interpretation of the OOA concepts is an intrinsic part of the
:ROOA method.  It was designed in such a way that software engineers with  
no
:experience in \Lotos, can still use ROOA.
:
:The denotational semantics of the concepts of object-oriented analysis
:illuminates the formal syntactic transformations within ROOA and  
guarantees
:that the basic object-oriented concepts can be understood independently of
:the specification language we use.
:
:The ROOA method starts from a set of informal requirements and an object
:model and produces a formal object-oriented analysis model that acts as a
:requirements specification.  The resulting formal model integrates the
:static, dynamic and functional properties of a system in contrast to
:existing OOA methods which are informal and produce three separate models
:that are difficult to integrate and keep consistent.  ROOA provides a
:systematic development process, by proposing a set of rules to be followed
:during the analysis phase.  During the application of these rules,  
auxiliary
:structures are created to help in tracing the requirements through to the
:final formal model.
:
:As \Lotos\ produces executable specifications, prototyping can be used to
:check the conformance of the specification against the original  
requirements
:and to detect inconsistencies, omissions and ambiguities early in the
:development process.
:
:% Performance-Oriented Specification of Communication Protocols and
:% Verification of their QoS Characteristics, Ina Schieferdecker
:
:\subsection{Performance-Oriented Specification and Verification of
:Protocols}{Ina Schieferdecker}{Technical University of  
[email-masked]}
:
:\ednote{The full title of this Ph.D. thesis is `Performance-Oriented
:Specification of Communication Protocols and Verification of their QoS
:Characteristics'.}
:
:The need for performance considerations at each level of the communication
:protocol development process arose and were forced by the advances in
:high-speed networks and the evolution of new communication services with
:their rigorous Quality-of-Service (QoS) requirements.
:
:This thesis presents an approach for the QoS-oriented design of
:communication protocols using formal specifications. It includes a
:specification technique for the performance-oriented behaviour description
:of communication protocols, a real-time temporal logic for the description
:of deterministic bounds, which are a special kind of QoS requirements, and
:decision procedures for verifying the fulfillment of deterministic bounds  
by
:a given communication protocol.
:
:The developed performance-oriented specification technique LotoTis extends
:LOTOS --- a standardized specification technique based on process algebras
:--- by means of quantified time, quantified parallelism, quantified
:nondeterminism, and monitoring of system execution. The central concept  
are
:structured actions which allow very concise and elegant description of
:performance-oriented behaviour. The presented approach uses a real-time
:temporal logic called AMTL, the --action-based version of MTL, for the
:description of deterministic bounds of performance characteristics.
:Deterministic bounds can be proven to be fulfilled by a given LotoTis,
:protocol specification provided the specification possesses only a finite
:--- but possibly cyclic --- state space. The implementation of the  
developed
:verification method is conceived, which allows us to investigate realistic
:communication protocols.
:
:The thesis can be retrieved by ftp or WWW:
:
:ftp://ftp.fokus.gmd.de/pub/step/papers/Schi9411:Performance.ps.gz
:
:http://www.fokus.gmd.de/htbin/info/step/ina
:
:%%% Standardisation
:
:\section{Standardisation}
:
:This section is devoted to international and national activities on the
:standardisation of \Lotos\ and its application to standards.
:
:% Report on E-LOTOS Status and Progress, Juan Quemada
:
:\subsection{Report on E-\Lotos\ Status and Progress}{Juan
:Quemada}{Polytechnic University
:of [email-masked]}
:
:\subsubsection{Scope of the Work Item on `Enhancements to \Lotos'}
:
:The scope of the work item was defined by the following list of  
enhancements
:to be defined:
:
:\begin{description}
:
:\item[Data-type enhancements:]
:A more user-friendly notation for data-type descriptions will be defined.
:This will consider:
:
:\begin{enumerate}
:
:\item
:Built-in types (e.g. booleans, characters, bits, integers, enumerations,
:possible reals)
:
:\item
:Composed types (e.g.\ records, unions, sets, arrays, strings, character
:strings, bitstrings)
:
:\item
:Partialy defined functions or subtyping
:
:\item
:Constructive types
:
:\item
:Interface with data types in other languages, e.g.\ ASN.1, SDL.
:
:\end{enumerate}
:
:\item[Introduction of modules:]
:
:A means to compose a specification from pre-existing modules will be  
defined
:to promote reusability and structuring.  This will consider:  data/process
:modules, information hiding, abstraction, object orientation.
:
:\item[Structure of events and true parallelism:]
:
:Mechanisms will be considered to remove the inability to express partial
:synchronization and data exchange.  This includes: compound events, gate
:typing, generalized termination and enabing, modelling of true  
parallelism,
:dynamic configuration.
:
:\item[Non-functional extensions:]
:Enhancements will be considered to allow specifying time and priorities.
:This has many applications in the area of protocols, ODP, telephony,
:real-time, testing.
:
:\end{description}
:
:All enhancements to be defined shall meet the following requirements:
:
:\begin{itemize}
:
:\item
:They shall maintain the existing \Lotos\ properties which support design  
and
:engineering procedures, i.e. for refinement, behavioural compatibility,
:executable specifications, for test derivation and proper tool support.
:
:\item
:The enhancement to \Lotos\ shall progress the definition of the textual
:version of the language together with the graphical version (G\Lotos).
:
:\item
:The enhancement to \Lotos\ shall ensure compatibility with the \Lotos\  
base
:standard.
:
:\end{itemize}
:
:\subsubsection{Current Proposals}
:
:This document describes the status of the standardization activities in  
the
:ISO-IEC Work Item on `Enhancement to \Lotos'. It reports the status after
:the last interim meeting which took place in Paris in February 1995 with
:participation of experts from Belgium, Canada, France, Japan, The
:Netherlands, Great Britain and Spain.
:
:The ISO-IEC Work Item on `Enhancements to \Lotos', known as E-\Lotos, has
:continued its progress since it started after a positive ballot in the  
fall
:of 1993. The E-\Lotos\ Work Item has to add new compatible features to
:\Lotos\ which shall increase its expressive power as well as facilitate  
its
:industrial usage.
:
:The E-\Lotos\ WI is presently part of the Working Group 7
:(ISO-IEC/JTC1/SC21/WG7) dealing with Open Distributed Processing (ODP),
:although it started in Working Group 1 (ISO-IEC/JTC1/SC21/WG1) dealing  
with
:OSI Architecture.
:
:Till now, the E-\Lotos\ Work Item has been centered in preparing and/or
:identifying suitable language enhancement proposals which shall provide  
the
:basis for the new version of the standard.
:
:The first version of E-\Lotos\ is expected to appear in short which will
:include the proposals which a high degree of consensus.
:
:The following enhancement proposals exists:
:
:\begin{itemize}
:
:\item
:Enhancements of existing \Lotos\ operators: generalization of termination,
:enabling and disabling
:
:\item
:Enhancements of the \Lotos\ event structure: gate typing and tagging.
:
:\item
:Introduction of time into \Lotos\
:
:\item
:Enhancement of the Data Typing part of \Lotos\
:
:\item
:Introduction of modules
:
:\item
:Introduction of Mobility in \Lotos\
:
:\item
:Other enhancements.
:
:\end{itemize}
:
:A brief description of the existing proposals is given now. For more
:information consult the ftp server `ftp.dit.upm.es' (directory
:\~{}/pub/lotos/elotos).   It can by accessed also through WWW:
:
:ftp://ftp.dit.upm.es/pub/lotos/elotos
:
:\subsubsection{Generalisation of \Lotos\ Operators}
:
:\Lotos\ is a language for expressing temporal ordering relations. The
:\Lotos\ operators are general in nature and are able to express many
:ordering relations quite naturally.
:
:Neverthess some ordering relations can only be expressed with artificial  
and
:lengthy constructs.  Therefore, generalization of some \Lotos\ operators  
has
:been proposed in order to enhance the expressive and structuring
:capabilities of \Lotos. A unique proposal exist which has been achieved
:after convergence of older proposals.
:
:The following proposals exist for generalizing the existing \Lotos\
:operators:
:
:\begin{description}
:
:\item[Generalised termination:]
:This proposal generalizes the \Lotos\ termination, which includes only
:synchronized termination, with a non-synchronised termination scheme. In a
:synchronized termination of a parallel composition, the composition will
:finish only if all parallel behaviour finish. This termination type exists
:in \Lotos. In a non-synchronised termination of a parallel composition,  
the
:composition can be defined to finish when only one or some parallel
:behaviour finish. This termination type does not exist in \Lotos.
:
:\item[Generalised enabling:]
:This proposal generalises the \Lotos\ enabling operator by parameterizing  
it
:with a termination gate name ($B_1>$$t$$>B_2$). This allows a termination
:event to decide the behaviour to enable by terminating with the gate name
:associated with the desired enabling operator. This construct is in fact  
an
:exception handling mechanism.
:
:\item[Generalised Disabling:]
:This proposal adds to the \Lotos\ disabling the capability of resuming the
:disabled behaviour after the disabling behaviour terminates. The  
generalized
:disabling is parameterized by a termination name ($B_1[t$$>B_2$). The
:occurrence of this termination name in the disabling behaviour will resume
:the disabled behaviour at the point where it was disabled. Any other
:termination event will be similar to an exit statement in the
:\Lotos\ disabling.
:
:\end{description}
:
:\subsubsection{Gate Typing and Tagging}
:
:This proposals deal with introducing strong typing to action denotations  
and
:a tagging mechanism for referencing the elements of an event by name.  
Gates
:are used to provide formal models of interfaces in \Lotos\ specifications.
:The inclusion of a gate typing mechanism in \Lotos\ provides a clear
:identification of the interfaces and its structure. It enhances the
:readability of \Lotos\ specifications. As any strong typing mechanism gate
:typing introduces redundancy and this will improve automatic error
:detection.
:
:In \Lotos\ the complete event structure must be made explicit in any  
action
:denotation and access to the individual variables or values can be made  
only
:by position. The tagging mechanism introduces a shorter and more concise
:representation based on reference-by-name which allows the representation  
of
:only the relevant part of the event structure of a given action  
denotation.
:Gate tagging supports also the hidding of part of the event structure.
:Several proposals exist which are compatible in the core. The proposals  
are
:in the process converging.
:
:\subsubsection{Time}
:
:\Lotos\ can express event ordering without any quantification of the exact
:timing of events. The inclusion of a quantitative notion of time in
:\Lotos\ is considered necessary for specifying a large number of systems.  
A
:unique proposal exist which has been achieved after convergence of older
:proposals.
:
:The timed model provides a precise definition of the instants of time at
:which events occur.  Therefore specifications will not define only the
:ordering of events in time, but also the quantitative aspects of timing.
:
:This proposal enriches \Lotos\ with 3 constructs for introducing timing
:information:
:
:\begin{itemize}
:
:\item
:Event Restriction. A predicate restricting the time of execution of an
:event.
:
:\item
:A Delay Statement which delays the ocurrence of any event of a behaviour a
:given amount of time.
:
:\item
:A Internal Time Choice construct which models the occurrence of an  
internal
:choice in a given tme interval.
:
:\end{itemize}
:
:The semantics of the new model is defined in terms of Time/Action Trees
:(with two types of transitions: time transitions and action transitions.  
The
:proposal provides also an informative annex containing an equivalent
:semantics in terms of Timed-action trees (actions labelled with time
:stamps).
:
:\subsubsection{Data Part}
:
:The enhancement of the data part of \Lotos\ is considered of great
:importance for the practical application of \Lotos.  The following  
approach
:for the data type has been adopted for E-\Lotos.
:
:A two level data definition scheme will be used in which an equational
:requirement definition level will be integrated with a more concrete
:functional data definition level.  A clear interface to external languages
:will be provided, e.g.\ towards ASN.1, IDL, SDL, ... A convergence  
proposal
:is planned for the next meeting.
:
:\subsubsection{Modules}
:
:An unanimous recognition exist about the necessity of introducing some
:module concept. A proposal exists which has been achieved after  
convergence
:of older proposals. Modules have a surface which defines the visible
:interface and a body which shall contain the specification of the module.
:Modules may use other modules by means of a `used by' relation which  
enables
:the creation of a hierarchy of module usages.
:
:\subsubsection{Mobility}
:
:The ability to model Open Distributed Processing (ODP), mobility and  
object
:orientation is considered a desirable feature for E-\Lotos.  A proposal
:exist for introducing mobility in \Lotos\ which facilitates modelling
:dynamically changing communication patterns. This proposal is based on
:combining the $\pi$-calculus with \Lotos.  The proposal is based on  
merging
:\Lotos\ operators with some operators of the $\pi$-calculus and  
introducing
:an additional encapsulation operator. Encapsulated objects can be composed
:with the operators borrowed from the $\pi$-calculus.
:
:\subsubsection{Other Improvements}
:
:There exist other proposals of improvements which deal with short hands,
:syntax or static semantic issues of the present \Lotos\ definition.
:
:%%% Applications to Problems
:
:\section{Applications to Problems}
:
:This section is devoted to work on artificial or real problems using
:\Lotos.
:
:\subsection{Formal Methods Applications Database}{Nico Plat}{Cap
:[email-masked]}
:
:\ednote{This general article is included in the hope that the
:\Lotos\ community may wish to contribute.}
:
:The industrial use of formal methods is limited and much of the experience
:gained with that industrial use is not available to the outside world.  
That
:is a pity, considering the fact that such experience can be very useful in
:avoiding the pitfalls one may encounter when starting to use formal  
methods
:in a `serious' way. It is with this thought in the back of their heads  
that
:some people active in FME (Formal Methods Europe) have come up with the  
idea
:to start a database with examples of applications of formal methods,
:accessible through ftp and WWW on a public site. The intention of the
:database is to give concise descriptions of - either successful or
:unsuccessful - application of formal methods/specification languages that
:will allow users to assess:
:
:\begin{itemize}
:
:\item
:whether or not formal methods/specification languages are being used for
:large, industrial applications;
:
:\item
:what the difficulties/advantages are of applying formal
:methods/specification languages on a larger scale;
:
:\item
:for which application domains formal methods/specification languages are
:being  used and which formal methods/specification languages are actually
:being used.
:
:\end{itemize}
:
:If you know of any applications of formal methods/specification languages
:worth considering for inclusion in the database (i.e.\ you have been
:involved yourself or you know someone who was involved with such an
:application) then it would be appreciated if you would fill in the form
:below and send it to the contact person. Leave any fields with information
:that you do not want to make public blank.
:
:\begin{verbatim}
:Name of the application:
:  <Name of the application or a one-line description of it.>
:
:Developed by organisation/consortium:
:  <Main organisation(s) involved with the development of the
:    application.>
:
:Formal method/specification language used:
:  <Self explanatory.>
:
:Tools used:
:  <Name of the tool used (if any).>
:
:Domain:
:  <A short characterisation of the application domain in which
:    the formal method/specification language has been applied, e.g.  
"medical
:    systems", "railway systems" or "Air-traffic control (ATC) systems".>
:
:Period:
:  <Period in time during which the application has been or will
:    be developed. We think this is relevant information because as time
:    passes, the time during which something has been developed can be used
:    as an indication of the state of the art that has been applied.>
:
:Size:
:  <A rough indication of the "size" of the application, in terms
:    of lines of specification/source code of the implementation or in  
terms
:    of human resources, i.e. the number of man-years involved.>
:
:Short description:
:  <A short (maximum 15 lines) description of the application and
:    the way formal methods/specification languages were applied on the
:    application, e.g. did you apply formal proofs? Which mode of working  
did
:    you use, i.e. separate specification teams/ implementation teams, did
:    you consult a formal method "guru", did you use formal
:    methods/specification languages in conjunction with other software
:    engineering techniques (e.g. Yourdon). Etc.>
:
:Conclusions:
:  <Any (subjective) observations on the application of formal
:    methods/ specification languages for your application. Do you feel  
that
:    application of formal methods/specification languages for the case you
:    describe was successful? If so/not, why/not? Etc.>
:
:Relevant publications:
:  <Adequate references to relevant publications, if any.>
:
:Contact:
:  <Name + address details (snail mail, phone, fax, e-mail) of a
:    contact person who may be approached if a person wants to have more
:    information about a case. Fill in "unavailable" if you do not want to  
or
:    can not be contacted for further information.>
:
:Further remarks:
:  <Any further remarks which you think may be relevant.>
:\end{verbatim}
:
:An electronic copy of the form can be obtained by 

:sending an e-mail message containing only the line:
:
:send vdm-forum fm-appl-db-form.txt
:
:to [email-masked]; the form will be send back to you.
:Alternatively, you can pick it up on WWW at URL: 

:
:gopher://nisp.ncl.ac.uk/11/lists-u-z/vdm-forum/files
:
:or by anonymous ftp from:
:
:ftp.ifad.dk (130.225.136.3) (directory pub/vdm)
:
:Send your contributions to (e-mail preferred):
:
:\begin{raggedright}
:Nico Plat  \\
:Cap Volmac  \\
:Dolderseweg 2  \\
:3712 BP Huis ter Heide  \\
:The Netherlands  \\
:\mbox{} \\
:Fax: +31-3404-31174  \\
:E-mail: [email-masked]  \\
:\end{raggedright}
:
:\begin{comment}
:
:%%% Language Issues
:
:\section{Language Issues}
:
:This section is devoted to issues in the design and use of \Lotos. It
:includes problems and solutions, theory and practice, technical queries,  
and
:frequently asked questions.
:
:\end{comment}
:
:%%% Tools
:
:\section{Tools}
:
:This section is devoted to new and existing developments in tools for
:\Lotos\ and their application.
:
:% Protocol Engineering in Lotos using the EUCALYPTUS Toolset, Hubert  
Garavel
:
:\subsection{Protocol Engineering in \Lotos\ using the {\sc Eucalyptus}  
Toolset}{Hubert Garavel}{Verimag/[email-masked]}
:
:\newcommand{\ALDEBARAN}{\mbox{\sc Ald\'ebaran}}
:\newcommand{\OPENCAESAR}{\mbox{\sc Open/C{\ae}sar}}
:\newcommand{\CAESAR}{\mbox{\sc C{\ae}sar}}
:\newcommand{\CAESARADT}{\mbox{\sc C{\ae}sar.adt}}
:\newcommand{\EUCALYPTUS}{{\sc Eucalyptus}}
:\newcommand{\APERO}{{\sc Apero}}
:\newcommand{\Apero}{APERO}
:\newcommand{\APEROSYN}{{\sc Apero.syn}}
:\newcommand{\APEROLIB}{{\sc Apero.lib}}
:\newcommand{\ELUDO}{{\sc Eludo}}
:\newcommand{\ILOT}{{\sc Ilot}}
:\newcommand{\DAFY}{{\sc Dafy}}
:\newcommand{\GOAL}{{\sc Goal}}
:\newcommand{\ISLA}{{\sc Isla}}
:\newcommand{\SELA}{{\sc Sela}}
:\newcommand{\TETRA}{{\sc Tetra}}
:\newcommand{\XTPANEL}{{\sc XtPanel}}
:\newcommand{\BCG}{\mbox{\sc Bcg}}
:
:The development of telecommunication protocols and distributed systems can
:be improved by the use of formal methods supported by appropriate software
:tools. We summarize here the main achievements of the European-Canadian
:project \EUCALYPTUS\footnote{ This work has been supported in part by the
:Commission of the European Communities, under ESPRIT EC-Canada Exploratory
:Collaborative Activity EC-CA~001:76099 `EUCALYPTUS: A European/Canadian
:\Lotos\ Protocol Tool Set'.}, a two-year collaboration (in 1993 and 1994)
:between the Universities of Grenoble, Li\`ege, Montr\'eal, and Ottawa.
:
:The \EUCALYPTUS\ project has led to a protocol engineering toolset  
dedicated
:to the \Lotos\ language. It consists of several tools, which have been
:developed or improved during the project:
:
:\begin{description}
:
:\item[Grenoble:]
:\ALDEBARAN\  
\cite{Fernandez-90,Fernandez-Mounier-91-b,Fernandez-Kerbrat-Mounier-93},
:\BCG\ \cite{Garavel-94-c,Ruffiot-94},
:\CAESAR\ \cite{Garavel-Sifakis-90},
:\CAESARADT\ \cite{Garavel-89-c,Garavel-Turlier-93}, \OPENCAESAR\
:\cite{Garavel-92-a}
:
:\item[Li\`ege:]
:\APERO\ \cite{Pecheur-93}
:
:\item[Montr\'eal:]
:\TETRA\  
\cite{Bochmann-Bellal-89,Bochmann-Desbiens-Dubuc-Ouimet-Saba-90,Dubuc-Bochma 
nn-Bellal-Saba-90}
:
:\item[Ottawa:]
:\ELUDO\ \cite{Stepien-Tourrilhes-Sincennes-94},
:\ISLA\ \cite{Guillemot-HajHussein-Logrippo-88},
:\SELA\ \cite{Ghribi-Logrippo-93},
:\GOAL\ \cite{HajHussein-Logrippo-Sincennes-92}.
:
:\end{description}
:
:These tools are integrated together and offer an extensive set of
:functionalities through a unified graphical interface:
:
:\begin{description}
:
:\item[Lotos Extensions:]
:It is possible to enrich \Lotos\ with new constructs (especially, compact
:notations for type definitions) by using a preprocessor which allows
:macro-definitions to be defined and expanded into standard \Lotos.
:
:\item[Analysis:]
:The \EUCALYPTUS\ toolset contains two compilers, which implement the
:lexical, syntactic, and static semantics analyzes described in the  
ISO~8807
:standard.
:
:\item[Report generation:]
:The toolset can pretty-print \Lotos\ descriptions, and can also generate
:cross-references.
:
:\item[Code generation:]
:From \Lotos\ types and process definitions, one can produce C code to be
:interfaced and used in application programs.
:
:\item[Simulation:]
:The toolset supports various forms of simulation, such as interactive
:simulation (step-by-step execution with backtracking), symbolic expansion
:(in which input values are handled symbolically), goal-oriented  
simulation,
:and random execution.
:
:\item[Exhaustive verification:]
:The \EUCALYPTUS\ toolset allows to generate the Labelled Transition System
:(LTS) corresponding to a \Lotos\ description: LTSs with millions of states
:and transitions can be generated, within the limits of available memory.
:LTSs are stored using a compact format based on ad'hoc data compression
:techniques.
:
:These LTSs can be analyzed and verified in several ways. They can be
:minimized and compared modulo various equivalence (bisimulations) and
:preorder relations.  They can also be validated using properties expressed
:as formulas of temporal logic or $\mu$-calculus:  the \EUCALYPTUS\ toolset
:provides connections with external verification tools such as {\sc Mec}
:\cite{Arnold-89}, {\sc Xesar}
:\cite{Richier-Rodriguez-Sifakis-Voiron-87-b,Graf-Richier-Rodriguez-Voiron-8 
9},
:the {\em Concurrency Workbench\/} \cite{Cleaveland-Parrow-Steffen-89}, as
:well as the common format FC2 \cite{Madelaine-DeSimone-93} defined in the
:ESPRIT CONCUR-2 project.
:
:The toolset includes a tool that displays (in PostScript) the generated
:LTSs; it also allows the connection with other tools such as {\sc
:Auto/Autograph} \cite{Roy-DeSimone-90}, {\sc 2D-Viscope} or {\sc  
3D-Viscope}
:\cite{Jard-Jeron-94}.
:
:\item[Compositional verification:]
:Due to the well-known state explosion problem, the exhaustive generation  
of
:LTSs is not always possible.  The \EUCALYPTUS\ toolset allows to divide a
:\Lotos\ description into parallel processes, to generate the LTSs
:corresponding to these processes, to minimize these LTSs modulo a
:bisimulation relation, and to build the LTS for the whole system by
:recombining these reduced LTSs. In practice, this ``divide and conquer''
:approach gives satisfactory results.
:
:\item[On-the-fly verification:]
:As an alternative approach to avoid the state explosion problem, the
:\EUCALYPTUS\ toolset allows certain properties to be verified even if the
:whole LTS is not generated. It is therefore possible to detected the
:presence of deadlocks, the existence of certain execution sequences, or  
even
:to make on-the-fly comparisons for bisimulation relations.
:
:\item[Trace analysis:]
:Finally, the \EUCALYPTUS\ toolset allows to verify whether a given trace
:(execution sequence) can be obtained from a \Lotos\ description. This  
allows
:to validate test suites and their verdicts with respect to a
:\Lotos\ description representing the behavior of the system under test.
:
:\end{description}
:
:The \EUCALYPTUS\ toolset has been used in many case-studies: high-speed
:protocols, telecommunication switches, atomic multicast protocols, cache
:memory protocols, etc. It will be made available in March or April 1995.
:
:For further information please contact:
:
:\begin{raggedright}
:Hubert GARAVEL \\
:INRIA Rh\^one-Alpes \\
:VERIMAG --- Miniparc-ZIRST \\
:rue Lavoisier \\
:38330 MONTBONNOT ST MARTIN \\
:FRANCE \\
:Tel: +(33) 76 90 96 34 \\
:Fax: +(33) 76 41 36 20 \\
:E-mail: {\tt [email-masked]}
:\end{raggedright}
:
:% GraphicaL Designer/Animator, Jesus Sanchez Allende
:
:\subsection{GraphicaL Designer/Animator}{Jesus Sanchez  
Allende}{Polytechnic
:University of [email-masked]}
:
:This is the announcement of the new releases of GLD and GLA graphical
:tools for \Lotos. Precompiled versions for SunOS are available using
:anonymous ftp.
:
:\subsubsection{GLD (GraphicaL Designer)}
:
:GLD is a tool aimed at graphical editing and design for \Lotos. It uses  
two
:different formalisms: G-\Lotos\ and DART (can be mixed).
:
:\begin{itemize}
:
:\item
:\Lotos\ mode:
:
:\begin{itemize}
:
:\item
:Automatic layout
:
:\item
:Automatic conversion from/to textual \Lotos
:
:\item
:Free editing or syntax oriented editing
:
:\end{itemize}
:
:\item
:DART mode: (To design the architecture of processes of the
:system and its relations of parallelism, sequences and disabling)
:
:\begin{itemize}
:
:\item
:DART editing
:
:\item
:Use of adjustable grid
:
:\item
:DART transformation
:
:\end{itemize}
:
:\item
:Both:
:
:\begin{itemize}
:
:\item
:Mixed design: You can use G-\Lotos\ or DART at any moment.
:
:\item
:Usual edit functions (Cut, Copy, Paste, Zoom, ...)
:
:\item
:Programmable transformation from DART into G-\Lotos\ and vice versa.
:
:\item
:Rapid navigation over the specification
:
:\end{itemize}
:
:\end{itemize}
:
:New in version 2R1b (with respect to 2R1) are:
:
:\begin{itemize}
:
:\item
:Faster drawing of complex DARTs
:
:\item
:Faster conversion of complex DARTs
:
:\item
:New option: Binary SP
:
:\item
:New option: DART parameters
:
:\item
:A couple of bugs corrected.
:
:\end{itemize}
:
:\subsubsection{GLA (Graphical Animator)}
:
:GLA is a simulator of the behaviour of a \Lotos\ specification, using
:graphical views from the DART specification to show:
:
:\begin{itemize}
:
:\item
:Process involved in a synchronisation
:
:\item
:What actions are the potential offerts of each process
:
:\item
:The history of instantiations
:
:\item
:Which process are active
:
:\item
:A trace of the execution.
:
:\end{itemize}
:
:New in version 2R0 (with respect to 1R0) is:
:
:\begin{itemize}
:
:\item
:Support for full \Lotos.
:
:\end{itemize}
:
:\subsubsection{Where to find GLD and GLA}
:
:Use anonymous ftp at ftp.dit.upm.es in pub/lotos/tools/medas/ and get the  
files:
:
:\begin{raggedright}
:GLD\_2R1b.README.gz \\ 

:GLD\_2R1b.Sun4.tar.gz \\ 

:GLA\_2R0.README.gz \\ 

:GLA\_2R0.Sun4.tar.gz \\ 

:\end{raggedright}
:
:% LOLA 3R6, David Larrabeiti
:
:\subsection{LOLA 3R6}{David Larrabeiti}{Polytechnic University of
:[email-masked]}
:
:Release 3R6 of LOLA (LOtos LAboratory) is now available at:
:
:ftp://ftp.dit.upm.es/pub/lotos/tools/TOPO\_3R6/contrib/LOLA\_3R6
:
:including a compiled version for 386+.
:
:LOLA is an experimental tool which supports
:different aspects of \Lotos-based design. Its present performance
:enables its use with large \Lotos\ specifications in an efficient way.
:
:New in this release are:
:
:\begin{itemize}
:
:\item
:several bugs fixed
:
:\item
:new test options for non-exhaustive state space exploration 

:(bit state hashing techniques and choice random selection) and
:automatic test passing break
:
:\item
:speed and memory optimisation
:
:\item
:customization facilities
:
:\item
:optionally compilable to include timing features (experimental).
:
:\end{itemize}
:
:LOLA provides the following functionalities:
:
:\begin{itemize}
:
:\item
:Debugging and step-by-step simulation of \Lotos\ specifications
:
:\begin{itemize}
:
:\item
:User guided step-by-step execution.
:
:\item
:Value expressions optionally provided by the user.
:
:\item
:Automatic composition of test processes.
:
:\item
:Full description of states ( process instantiations,
:synchronisation analysis, tracing, ... ).
:
:\end{itemize}
:
:\item
:Verification of \Lotos\ specifications by state exploration
:with several optimisations:
:
:\begin{itemize}
:
:\item
:Full computation of test response analysis (must, may or 

:reject) according to Testing Equivalence.
:
:\item
:Symbolic state space explorations
:
:\item
:Factoring out of interleaving
:
:\item
:Internal action reduction according to testing equivalence
:
:\end{itemize}
:
:\item
:Testing and random execution of \Lotos\ specifications
:
:\begin{itemize}
:
:\item
:Analysis of test response in random executions.
:
:\end{itemize}
:
:\item
:Transformation of \Lotos\ specifications into
:
:\begin{itemize}
:
:\item
:FSM (Expansion into an equivalent Finite State Machine)
:
:\item
:EFSM. (Expansion with symbolic treatment of values)
:
:\item
:Plain behaviour tree (without duplicate states detection)
:
:\item
:Interleaved expansion (Factoring out of interleaving).
:
:\end{itemize}
:
:\item
:Data value expressions evaluation.
:
:\item
:Two user interfaces available:
:
:\begin{itemize}
:
:\item
:Textual interface
:
:\item
:Graphical interface based on X-windows.
:
:\end{itemize}
:
:\end{itemize}
:
:It provides therefore automatic batch and full-interactive support
:to several activities of a \Lotos\ based design cycle .
:
:Coverage: Full \Lotos\ (IS-8807).
:
:Runs on:
:
:\begin{itemize}
:
:\item
:Sun-3, Sun-4 (sparc) with SunOS 4.0.3 or Solaris 2.3
:
:\item
:IBM-PC or compatible (386 or 486 required) with DOS
:
:\item
:HP-9000 with HP-UX. 

:
:\end{itemize}
:
:Installation: See files install.* in the distribution directory. 

:
:Distribution:
:
:LOLA is part of the DIT-UPM \Lotos\ toolset and is integrated with the
:TOPO \Lotos\ tool set under which it runs, using its static semantics
:analyser. This package is necessary to run LOLA.
:
:LOLA is distributed as free software for non-profit use,
:and can be obtained from the addresses below.
:
:On the network, LOLA is obtainable via anonymous ftp from:
:
:\begin{verbatim}
:  host             IP address      directory
:  --------------   -------------   -------------------------------
:  ftp.dit.upm.es   [138.4.2.10]    lotos/tools/TOPO_.../contrib/
:  --------------   -------------   --------------------------------
:\end{verbatim}
:
:where ... stands for the version.
:
:For a streamer, send us two standard Sun streamers (QIC-11, 600ft)
:LOLA will be loaded into one of them, and returned to you.
:The other streamer will be retained as payment for administrative
:costs.
:
:Please send your comments, questions, bug-reports and results to : 

:
:\begin{verbatim}
:  <[email-masked]>
:  <[email-masked]>
:  <[email-masked]>
:  <[email-masked]>
:\end{verbatim}
:
:% TOPO 3R6, Pepe Manas
:
:\subsection{TOPO 3R6}{Pepe Ma\~nas}{Polytechnic University of  
[email-masked]}
:
:We have released a new version of TOPO, a bunch of tools for \Lotos.  A
:previous release (3R5, 7th December 1994) had some flaws that we have  
tried
:to repair in 3R6.
:
:Available at:
:
:ftp://ftp.dit.upm.es/pub/lotos/tools/TOPO\_3R6/
:
:A brief overview of facilities may be found at:
:
:ftp://ftp.dit.upm.es/pub/lotos/tools/TOPO\_3R6/distribution/doc/WhatIs
:
:%%% References
:
:\begin{refsection}{99}
:
:\bibitem{Arnold-89}
:Andr\'e Arnold.
:\newblock MEC: A System for Constructing and Analysing Transition Systems.
:\newblock In Joseph Sifakis, editor, {\em Proceedings of the 1st Workshop  
on
:Automatic Verification Methods for Finite State Systems (Grenoble,  
France)},
:volume 407 of {\em Lecture Notes in Computer Science}, pages 117--132,
:Berlin, June 1989. Springer Verlag.
:
:\bibitem{Bochmann-Bellal-89}
:G.v. Bochmann and O.~Bellal.
:\newblock Test Result Analysis with respect to Formal Specification.
:\newblock In {\em Proceedings of the 2nd International Workshop on  
Protocol
:Test Systems (Berlin, Germany)}, October 1989.
:
:\bibitem{Bochmann-Desbiens-Dubuc-Ouimet-Saba-90}
:G.v. Bochmann, D.~Desbiens, M.~Dubuc, D.~Ouimet, and F.~Saba.
:\newblock Test Result Analysis and Validation of Test Verdicts.
:\newblock In {\em Proceedings of the 3rd International Workshop on  
Protocol
:Test Systems (McLean, Virginia, USA)}, October 1990.
:
:\bibitem{Bustard-1994}
:Bustard DW: Progress Towards RACE, a `Soft-Centred' Requirements  
Definition
:Method, 1st IFIP/SQI International Conference on Software Quality and
:Productivity, Hong Kong, Dec 1994, pp 29-36 (Chapman \& Hall)
:
:\bibitem{Bustard-Lundy-1995}
:Bustard DW and Lundy PJ: Enhancing Soft Systems with Formal Modelling,
:Proceedings of the 2nd International IEEE Symposium on Requirements  
Engineering,
:York, March 1995
:
:\bibitem{Bustard-Winstanley-1994}
:Bustard DW and Winstanley A: Making Changes to Formal Specifications:
:Requirements and an Example, IEEE Trans. Soft. Eng., August 1994, 20(8),  
pp.
:562-568
:
:\bibitem{Cleaveland-Parrow-Steffen-89}
:R.~Cleaveland, J.~Parrow, and B.~Steffen.
:\newblock The Concurrency Workbench.
:\newblock In J.~Sifakis, editor, {\em Proceedings of the 1st Workshop on
:Automatic Verification Methods for Finite State Systems (Grenoble,  
France)},
:volume 407 of {\em Lecture Notes in Computer Science}, pages 24--37,  
Berlin,
:June 1989. Springer Verlag.
:
:\bibitem{Dubuc-Bochmann-Bellal-Saba-90}
:M.~Dubuc, G.v. Bochmann, O.~B. Bellal, and F.~Saba.
:\newblock Translation from TTCN to LOTOS and the Validation of Test Cases.
:\newblock In Juan Quemada, Jos\'e~Ma\ nas, and Enrique V\'azquez, editors,  
{\em
:Proceedings of the 3rd International Conference on Formal Description
:Techniques {FORTE}'90 (Madrid, Spain)}, Amsterdam, November 1990.
:North-Holland.
:
:\bibitem{Fernandez-90}
:Jean-Claude Fernandez.
:\newblock An Implementation of an Efficient Algorithm for Bisimulation
:Equivalence.
:\newblock {\em Science of Computer Programming}, 13(2--3):219--236, May  
1990.
:
:\bibitem{Fernandez-Kerbrat-Mounier-93}
:Jean-Claude Fernandez, Alain Kerbrat, and Laurent Mounier.
:\newblock Symbolic Equivalence Checking.
:\newblock In C.~Courcoubetis, editor, {\em Proceedings of the 4th Workshop  
on
:Computer-Aided Verification (Heraklion, Greece)}, June 1993.
:
:\bibitem{Fernandez-Mounier-91-b}
:Jean-Claude Fernandez and Laurent Mounier.
:\newblock A Tool Set for Deciding Behavioral Equivalences.
:\newblock In {\em Proceedings of CONCUR'91 (Amsterdam, The Netherlands)},
:August 1991.
:
:\bibitem{Garavel-89-c}
:Hubert Garavel.
:\newblock Compilation of LOTOS Abstract Data Types.
:\newblock In Son~T. Vuong, editor, {\em Proceedings of the 2nd  
International
:Conference on Formal Description Techniques {FORTE}'89 (Vancouver B.C.,
:Canada)}, pages 147--162, Amsterdam, December 1989. North-Holland.
:
:\bibitem{Garavel-92-a}
:Hubert Garavel.
:\newblock The OPEN/C{\AE}SAR Reference Manual.
:\newblock Rapport SPECTRE C33, Laboratoire de G\'enie Informatique ---  
Institut
:IMAG, Grenoble, May 1992.
:
:\bibitem{Garavel-94-c}
:Hubert Garavel.
:\newblock Binary Coded Graphs --- Definition of the BCG Format  
(version~1.0).
:\newblock Rapport Technique tp appear, INRIA Rh\^one-Alpes, Grenoble,  
1995.
:
:\bibitem{Guillemot-HajHussein-Logrippo-88}
:R.~Guillemot, R.~Haj-Hussein, and L.~Logrippo.
:\newblock Executing Large LOTOS Specifications.
:\newblock In S.~Aggarwal and K.~Sabnani, editors, {\em Proceedings of the  
8th
:International Workshop on Protocol Specification, Testing and Verification
:(Atlantic City, NJ, USA)}, pages 399--410, Amsterdam, 1988. IFIP,
:North-Holland.
:
:\bibitem{Ghribi-Logrippo-93}
:B.~Ghribi and L.~Logrippo.
:\newblock A Validation Environment for LOTOS.
:\newblock In A.~Danthine, G.~Leduc, and P.~Wolper, editors, {\em  
Proceedings of
:the 13th IFIP International Workshop on Protocol Specification, Testing  
and
:Verification (Li\'ege, Belgium)}, pages 93--108, Amsterdam, May 1993.  
IFIP,
:North-Holland.
:
:\bibitem{Graf-Richier-Rodriguez-Voiron-89}
:Suzanne Graf, Jean-Luc Richier, Carlos Rodr\'{\i}guez, and Jacques Voiron.
:\newblock What are the Limits of Model Checking Methods for the  
Verification of
:Real Life Protocols?
:\newblock In Joseph Sifakis, editor, {\em Proceedings of the 1st Workshop  
on
:Automatic Verification Methods for Finite State Systems (Grenoble,  
France)},
:volume 407 of {\em Lecture Notes in Computer Science}, pages 275--285,
:Berlin, June 1989. Springer Verlag.
:
:\bibitem{Garavel-Sifakis-90}
:Hubert Garavel and Joseph Sifakis.
:\newblock Compilation and Verification of LOTOS Specifications.
:\newblock In L.~Logrippo, R.~L. Probert, and H.~Ural, editors, {\em  
Proceedings
:of the 10th International Symposium on Protocol Specification, Testing and
:Verification (Ottawa, Canada)}, pages 379--394, Amsterdam, June 1990.  
IFIP,
:North-Holland.
:
:\bibitem{Garavel-Turlier-93}
:Hubert Garavel and Philippe Turlier.
:\newblock C{\AE}SAR.ADT~: un compilateur pour les types abstraits  
alg\'ebriques
:du langage LOTOS.
:\newblock In Rachida Dssouli and Gregor v.~Bochmann, editors, {\em Actes  
du
:Colloque Francophone pour l'Ing\'enierie des Protocoles CFIP'93  
(Montr\'eal,
:Canada)}, 1993.
:
:\bibitem{HajHussein-Logrippo-Sincennes-92}
:M.~Haj-Hussein, L.~Logrippo, and J.~Sincennes.
:\newblock Goal-Oriented Execution of LOTOS Specifications.
:\newblock In M.~Diaz and R.~Groz, editors, {\em Proceedings of the 4th
:International Conference on Formal Description Techniques {FORTE}'92
:(Perros-Guirec, France)}, pages 311--327, Amsterdam, 1992. North-Holland.
:
:\bibitem{Jard-Jeron-94}
:Claude Jard and Thierry J\'eron.
:\newblock 3D layout of reachability graphs of communicating processes.
:\newblock PI 852, INRIA, Centre IRISA, Rennes, August 1994.
:
:\bibitem{Lundy-Bustard-1994}
:Lundy PJ and Bustard DW: Making Formal Methods Work: What's Being Done and
:What Can be Done, Proceedings of 2nd International Conference on Software
:Quality Management, Edinburgh, July 1994, pp. 485-499 (Elsevier)
:
:\bibitem{Madelaine-DeSimone-93}
:Eric Madelaine and {Robert de} Simone.
:\newblock {\em FC2: Reference Manual Version 1.1}.
:\newblock INRIA, Sophia-Antipolis (France), July 1993.
:
:\bibitem{Pecheur-93}
:Charles Pecheur.
:\newblock VLib: Infinite Virtual Libraries for LOTOS.
:\newblock In A.~Danthine, G.~Leduc, and P.~Wolper, editors, {\em  
Proceedings of
:the 13th IFIP International Workshop on Protocol Specification, Testing  
and
:Verification (Li\'ege, Belgium)}, pages 1--16, Amsterdam, May 1993. IFIP,
:North-Holland.
:
:\bibitem{Richier-Rodriguez-Sifakis-Voiron-87-b}
:Jean-Luc Richier, Carlos Rodr\'{\i}guez, Joseph Sifakis, and Jacques  
Voiron.
:\newblock Verification in XESAR of the Sliding Window Protocol.
:\newblock In Harry Rudin and Colin~H. West, editors, {\em Proceedings of  
the
:7th International Symposium on Protocol Specification, Testing and
:Verification (Zurich)}, Amsterdam, May 1987. IFIP, North-Holland.
:
:\bibitem{Roy-DeSimone-90}
:Val\'erie Roy and {Robert de} Simone.
:\newblock Auto/Autograph.
:\newblock In R.~P. Kurshan and E.~M. Clarke, editors, {\em Proceedings of  
the
:2nd Workshop on Computer-Aided Verification (Rutgers, New Jersey, USA)},
:volume~3 of {\em DIMACS Series in Discrete Mathematics and Theoretical
:Computer Science}, pages 477--491. AMS-ACM, June 1990.
:
:\bibitem{Ruffiot-94}
:Renaud Ruffiot.
:\newblock D\'efinition et r\'ealisation d'un atelier logiciel pour  
l'\'etude
:des syst\`emes de transitions.
:\newblock M\'emoire d'ing\'enieur CNAM, Institut IMAG, Grenoble, December  
1994.
:
:\bibitem{Stepien-Tourrilhes-Sincennes-94}
:B.~Stepien, J.~Tourrilhes, and J.~Sincennes.
:\newblock ELUDO: The University of Ottawa LOTOS Toolkit.
:\newblock Technical Report, University of Ottawa, 1994.
:\newblock Obtainable by FTP on lotos.csi.uottawa.ca.
:
:\bibitem{Wilson-1990}
:Wilson B: Systems: Concepts, Methodologies and Applications, 2nd Edition,
:Wiley, 1990
:
:\bibitem{Winstanley-Bustard-1991}
:Winstanley A and Bustard DW: EXPOSE: An Animation Tool for  
Process-Oriented
:Specifications, Software Engineering Journal, 6 (6), November 1991, pp.  
463-475
:
:\end{refsection}
:
:%%% End
:
:\newsend
:
:\end{document}
SHAR_EOF
fi # end of overwriting check
#	End of shell archive
exit 0