Theory Introduction

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Introduction
 *
 * Copyright (c) 2023 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)

chapter‹ Introduction ›

(*<*)
theory Introduction                                               
  imports "HOL-CSPM.CSPM"
begin 
(*>*)

section ‹Motivations›

text ‹\<^session>‹HOL-CSP› \<^cite>‹"HOL-CSP-AFP"› is a formalization in Isabelle/HOL of 
      the work of Hoare and Roscoe on the denotational semantics of the 
      Failure/Divergence Model of CSP. It follows essentially the presentation of CSP 
      in Roscoe's Book "Theory and Practice of Concurrency" \<^cite>‹"roscoe:csp:1998"›
      and the semantic details in a joint paper of Roscoe and Brooks
      "An improved failures model for communicating processes" \<^cite>‹"brookes-roscoe85"›.›

text ‹Basically, the session \<^session>‹HOL-CSP› introduces the type \<^typ>‹'α process›,
      several classic CSP operators and number of ``laws'' (i.e. derived equations)
      that govern their interactions.
      \<^session>‹HOL-CSP› has been extended by a theory of architectural operators \<^session>‹HOL-CSPM› 
      inspired by the ‹CSP⇩M› language of the model-checker FDR. While in FDR these operators are 
      basically macros over finite lists and sets, the \<^session>‹HOL-CSPM› theory treats them in their
      own right for the most general cases.›

text ‹The present work addresses the problem of operational semantics for CSP which are the
      foundations for finite model-checking and process simulation techniques.
      In the literature, there are a few versions of operational semantics for CSP,
      which lend themselves to the constructions of labelled transition systems (LTS).
      Of course, denotational and operational constructs are expected to coincide, 
      but this is not obvious at first glance.
      As a key contribution, we will define the operational derivation operators ‹P ↝⇩τ Q›
      (``‹P› evolves internally to ‹Q›) and ‹P ↝⇩e Q› (``‹P› evolves to ‹Q› by emitting ‹e›'')
      in terms of the denotational semantics and derive the expected laws for
      operational semantics from these.›

text ‹Additionally, we developed the theory of the interrupt operators ∗‹Sliding›, ∗‹Throw› 
      and ∗‹Interrupt› \<^cite>‹"Roscoe2010UnderstandingCS"› which have been traditionally
      introduced in the context of operational semantics.
      This part of the present theory reintroduces denotational semantics for these operators and
      constructs on this basis the operational laws for them.›

text ‹The overall objective of this work is to provide a formal, machine checked foundation
      for the laws provided by Roscoe in
      \<^cite>‹"roscoe:csp:1998" and "DBLP:journals/entcs/Roscoe15"›.
      In several places, our formalization efforts led to slight modifications of the original
      definitions in order to achieve the goal of a combined integrated theory.
      In some cases -- in particular in connection with the ∗‹Interrupt› operator definition --
      some corrections have been necessary since the fundamental invariants were not respected.›

text ‹\newpage›





section‹The Global Architecture of \<^session>‹HOL-CSP_OpSem››

text‹
\begin{figure}[ht]
  \centering
  \includegraphics[width=0.70\textwidth]{figures/session_graph.pdf}
	\caption{The overall architecture}
	\label{fig:fig1}
\end{figure}
›

text‹The global architecture of \<^session>‹HOL-CSP_OpSem› is shown in \autoref{fig:fig1}.

     The package resides on:
     ▪ \<^session>‹HOL-CSP› 2.0 from the Isabelle Archive of Formal Proofs
     ▪ \<^session>‹HOL-CSPM› from the Isabelle Archive of Formal Proofs.
›

(*<*)
end
(*>*)