eliminated calamity with tick symbol, layout imprivements, eliminated docitem
This commit is contained in:
parent
850244844b
commit
762680a20c
|
|
@ -77,9 +77,8 @@ be distinguished:
|
|||
\<^enum> the \<^emph>\<open>external choice\<close>, written \<open>_\<box>_\<close>, which forces a process "to follow" whatever
|
||||
the environment offers, and
|
||||
\<^enum> the \<^emph>\<open>internal choice\<close>, written \<open>_\<sqinter>_\<close>, which imposes on the environment of a process
|
||||
"to follow" the non-deterministic choices made.
|
||||
"to follow" the non-deterministic choices made.\<close>
|
||||
|
||||
\<close>
|
||||
text\<open>
|
||||
Generalizations of these two operators \<open>\<box>x\<in>A. P(x)\<close> and \<open>\<Sqinter>x\<in>A. P(x)\<close> allow for modeling the concepts
|
||||
of \<^emph>\<open>input\<close> and \<^emph>\<open>output\<close>: Based on the prefix operator \<open>a\<rightarrow>P\<close> (event \<open>a\<close> happens, then the process
|
||||
|
|
@ -127,10 +126,10 @@ attempt to formalize denotational \<^csp> semantics covering a part of Bill Rosc
|
|||
omitted.\<close>}.
|
||||
\<close>
|
||||
|
||||
section*["pre"::tc,main_author="Some(@{docitem \<open>bu\<close>}::author)"]
|
||||
section*["pre"::tc,main_author="Some(@{author \<open>bu\<close>}::author)"]
|
||||
\<open>Preliminaries\<close>
|
||||
|
||||
subsection*[cspsemantics::tc, main_author="Some(@{docitem ''bu''})"]\<open>Denotational \<^csp> Semantics\<close>
|
||||
subsection*[cspsemantics::tc, main_author="Some(@{author ''bu''})"]\<open>Denotational \<^csp> Semantics\<close>
|
||||
|
||||
text\<open> The denotational semantics (following @{cite "roscoe:csp:1998"}) comes in three layers:
|
||||
the \<^emph>\<open>trace model\<close>, the \<^emph>\<open>(stable) failures model\<close> and the \<^emph>\<open>failure/divergence model\<close>.
|
||||
|
|
@ -190,7 +189,7 @@ of @{cite "IsobeRoggenbach2010"} is restricted to a variant of the failures mode
|
|||
|
||||
\<close>
|
||||
|
||||
subsection*["isabelleHol"::tc, main_author="Some(@{docitem ''bu''})"]\<open>Isabelle/HOL\<close>
|
||||
subsection*["isabelleHol"::tc, main_author="Some(@{author ''bu''})"]\<open>Isabelle/HOL\<close>
|
||||
text\<open> Nowadays, Isabelle/HOL is one of the major interactive theory development environments
|
||||
@{cite "nipkow.ea:isabelle:2002"}. HOL stands for Higher-Order Logic, a logic based on simply-typed
|
||||
\<open>\<lambda>\<close>-calculus extended by parametric polymorphism and Haskell-like type-classes.
|
||||
|
|
@ -219,10 +218,10 @@ domain theory for a particular type-class \<open>\<alpha>::pcpo\<close>, \<^ie>
|
|||
fixed-point induction and other (automated) proof infrastructure. Isabelle's type-inference can
|
||||
automatically infer, for example, that if \<open>\<alpha>::pcpo\<close>, then \<open>(\<beta> \<Rightarrow> \<alpha>)::pcpo\<close>. \<close>
|
||||
|
||||
section*["csphol"::tc,main_author="Some(@{docitem ''bu''}::author)", level="Some 2"]
|
||||
section*["csphol"::tc,main_author="Some(@{author ''bu''}::author)", level="Some 2"]
|
||||
\<open>Formalising Denotational \<^csp> Semantics in HOL \<close>
|
||||
|
||||
subsection*["processinv"::tc, main_author="Some(@{docitem ''bu''})"]
|
||||
subsection*["processinv"::tc, main_author="Some(@{author ''bu''})"]
|
||||
\<open>Process Invariant and Process Type\<close>
|
||||
text\<open> First, we need a slight revision of the concept
|
||||
of \<^emph>\<open>trace\<close>: if \<open>\<Sigma>\<close> is the type of the atomic events (represented by a type variable), then
|
||||
|
|
@ -273,7 +272,7 @@ but this can be constructed in a straight-forward manner. Suitable definitions f
|
|||
\<open>\<T>\<close>, \<open>\<F>\<close> and \<open>\<D>\<close> lifting \<open>fst\<close> and \<open>snd\<close> on the new \<open>'\<alpha> process\<close>-type allows to derive
|
||||
the above properties for any \<open>P::'\<alpha> process\<close>. \<close>
|
||||
|
||||
subsection*["operator"::tc, main_author="Some(@{docitem ''lina''})"]
|
||||
subsection*["operator"::tc, main_author="Some(@{author ''lina''})"]
|
||||
\<open>\<^csp> Operators over the Process Type\<close>
|
||||
text\<open> Now, the operators of \<^csp> \<open>Skip\<close>, \<open>Stop\<close>, \<open>_\<sqinter>_\<close>, \<open>_\<box>_\<close>, \<open>_\<rightarrow>_\<close>,\<open>_\<lbrakk>_\<rbrakk>_\<close> etc.
|
||||
for internal choice, external choice, prefix and parallel composition, can
|
||||
|
|
@ -298,7 +297,7 @@ The definitional presentation of the \<^csp> process operators according to @{ci
|
|||
follows always this scheme. This part of the theory comprises around 2000 loc.
|
||||
\<close>
|
||||
|
||||
subsection*["orderings"::tc, main_author="Some(@{docitem ''bu''})"]
|
||||
subsection*["orderings"::tc, main_author="Some(@{author ''bu''})"]
|
||||
\<open>Refinement Orderings\<close>
|
||||
|
||||
text\<open> \<^csp> is centered around the idea of process refinement; many critical properties,
|
||||
|
|
@ -328,7 +327,7 @@ states, from which no internal progress is possible.
|
|||
\<close>
|
||||
|
||||
|
||||
subsection*["fixpoint"::tc, main_author="Some(@{docitem ''lina''})"]
|
||||
subsection*["fixpoint"::tc, main_author="Some(@{author ''lina''})"]
|
||||
\<open>Process Ordering and HOLCF\<close>
|
||||
text\<open> For any denotational semantics, the fixed point theory giving semantics to systems
|
||||
of recursive equations is considered as keystone. Its prerequisite is a complete partial ordering
|
||||
|
|
@ -395,7 +394,7 @@ Fixed-point inductions are the main proof weapon in verifications, together with
|
|||
and the \<^csp> laws. Denotational arguments can be hidden as they are not needed in practical
|
||||
verifications. \<close>
|
||||
|
||||
subsection*["law"::tc, main_author="Some(@{docitem ''lina''})"]
|
||||
subsection*["law"::tc, main_author="Some(@{author ''lina''})"]
|
||||
\<open>\<^csp> Rules: Improved Proofs and New Results\<close>
|
||||
|
||||
|
||||
|
|
@ -437,12 +436,12 @@ cases to be considered as well as their complexity makes pen and paper proofs
|
|||
practically infeasible.
|
||||
\<close>
|
||||
|
||||
section*["newResults"::tc,main_author="Some(@{docitem ''safouan''}::author)",
|
||||
main_author="Some(@{docitem ''lina''}::author)", level= "Some 3"]
|
||||
section*["newResults"::tc,main_author="Some(@{author ''safouan''}::author)",
|
||||
main_author="Some(@{author ''lina''}::author)", level= "Some 3"]
|
||||
\<open>Theoretical Results on Refinement\<close>
|
||||
text\<open>\<close>
|
||||
subsection*["adm"::tc,main_author="Some(@{docitem ''safouan''}::author)",
|
||||
main_author="Some(@{docitem ''lina''}::author)"]
|
||||
subsection*["adm"::tc,main_author="Some(@{author ''safouan''}::author)",
|
||||
main_author="Some(@{author ''lina''}::author)"]
|
||||
\<open>Decomposition Rules\<close>
|
||||
text\<open>
|
||||
In our framework, we implemented the pcpo process refinement together with the five refinement
|
||||
|
|
@ -477,8 +476,8 @@ The failure and divergence projections of this operator are also interdependent,
|
|||
sequence operator. Hence, this operator is not monotonic with \<open>\<sqsubseteq>\<^sub>\<F>\<close>, \<open>\<sqsubseteq>\<^sub>\<D>\<close> and \<open>\<sqsubseteq>\<^sub>\<T>\<close>, but monotonic
|
||||
when their combinations are considered. \<close>
|
||||
|
||||
subsection*["processes"::tc,main_author="Some(@{docitem ''safouan''}::author)",
|
||||
main_author="Some(@{docitem ''lina''}::author)"]
|
||||
subsection*["processes"::tc,main_author="Some(@{author ''safouan''}::author)",
|
||||
main_author="Some(@{author ''lina''}::author)"]
|
||||
\<open>Reference Processes and their Properties\<close>
|
||||
text\<open>
|
||||
We now present reference processes that exhibit basic behaviors, introduced in
|
||||
|
|
@ -598,11 +597,11 @@ then it may still be livelock-free. % This makes sense since livelocks are worse
|
|||
|
||||
\<close>
|
||||
|
||||
section*["advanced"::tc,main_author="Some(@{docitem ''safouan''}::author)",level="Some 3"]
|
||||
section*["advanced"::tc,main_author="Some(@{author ''safouan''}::author)",level="Some 3"]
|
||||
\<open>Advanced Verification Techniques\<close>
|
||||
|
||||
text\<open>
|
||||
Based on the refinement framework discussed in @{docitem "newResults"}, we will now
|
||||
Based on the refinement framework discussed in @{technical "newResults"}, we will now
|
||||
turn to some more advanced proof principles, tactics and verification techniques.
|
||||
We will demonstrate them on two paradigmatic examples well-known in the \<^csp> literature:
|
||||
The CopyBuffer and Dijkstra's Dining Philosophers. In both cases, we will exploit
|
||||
|
|
@ -613,7 +612,7 @@ verification. In the latter case, we present an approach to a verification of a
|
|||
architecture, in this case a ring-structure of arbitrary size.
|
||||
\<close>
|
||||
|
||||
subsection*["illustration"::tc,main_author="Some(@{docitem ''safouan''}::author)", level="Some 3"]
|
||||
subsection*["illustration"::tc,main_author="Some(@{author ''safouan''}::author)", level="Some 3"]
|
||||
\<open>The General CopyBuffer Example\<close>
|
||||
text\<open>
|
||||
We consider the paradigmatic copy buffer example @{cite "Hoare:1985:CSP:3921" and "Roscoe:UCS:2010"}
|
||||
|
|
@ -661,7 +660,7 @@ of 2 lines proof-script involving the derived algebraic laws of \<^csp>.
|
|||
|
||||
After proving that \<open>SYSTEM\<close> implements \<open>COPY\<close> for arbitrary alphabets, we aim to profit from this
|
||||
first established result to check which relations \<open>SYSTEM\<close> has wrt. to the reference processes of
|
||||
@{docitem "processes"}. Thus, we prove that \<open>COPY\<close> is deadlock-free which implies livelock-free,
|
||||
@{technical "processes"}. Thus, we prove that \<open>COPY\<close> is deadlock-free which implies livelock-free,
|
||||
(proof by fixed-induction similar to \<open>lemma: COPY \<sqsubseteq> SYSTEM\<close>), from which we can immediately infer
|
||||
from transitivity that \<open>SYSTEM\<close> is. Using refinement relations, we killed four birds with one stone
|
||||
as we proved the deadlock-freeness and the livelock-freeness for both \<open>COPY\<close> and \<open>SYSTEM\<close> processes.
|
||||
|
|
@ -678,7 +677,7 @@ corollary deadlock_free COPY
|
|||
\<close>
|
||||
|
||||
|
||||
subsection*["inductions"::tc,main_author="Some(@{docitem ''safouan''}::author)"]
|
||||
subsection*["inductions"::tc,main_author="Some(@{author ''safouan''}::author)"]
|
||||
\<open>New Fixed-Point Inductions\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -728,7 +727,7 @@ The astute reader may notice here that if the induction step is weakened (having
|
|||
the base steps require enforcement.
|
||||
\<close>
|
||||
|
||||
subsection*["norm"::tc,main_author="Some(@{docitem ''safouan''}::author)"]
|
||||
subsection*["norm"::tc,main_author="Some(@{author ''safouan''}::author)"]
|
||||
\<open>Normalization\<close>
|
||||
text\<open>
|
||||
Our framework can reason not only over infinite alphabets, but also over processes parameterized
|
||||
|
|
@ -788,7 +787,7 @@ Summing up, our method consists of four stages:
|
|||
|
||||
\<close>
|
||||
|
||||
subsection*["dining_philosophers"::tc,main_author="Some(@{docitem ''safouan''}::author)",level="Some 3"]
|
||||
subsection*["dining_philosophers"::tc,main_author="Some(@{author ''safouan''}::author)",level="Some 3"]
|
||||
\<open>Generalized Dining Philosophers\<close>
|
||||
|
||||
text\<open> The dining philosophers problem is another paradigmatic example in the \<^csp> literature
|
||||
|
|
@ -880,7 +879,7 @@ for a dozen of philosophers (on a usual machine) due to the exponential combinat
|
|||
Furthermore, our proof is fairly stable against modifications like adding non synchronized events like
|
||||
thinking or sitting down in contrast to model-checking techniques. \<close>
|
||||
|
||||
section*["relatedwork"::tc,main_author="Some(@{docitem ''lina''}::author)",level="Some 3"]
|
||||
section*["relatedwork"::tc,main_author="Some(@{author ''lina''}::author)",level="Some 3"]
|
||||
\<open>Related work\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -947,7 +946,7 @@ restrictions on the structure of components. None of our paradigmatic examples c
|
|||
be automatically proven with any of the discussed SMT techniques without restrictions.
|
||||
\<close>
|
||||
|
||||
section*["conclusion"::conclusion,main_author="Some(@{docitem ''bu''}::author)"]\<open>Conclusion\<close>
|
||||
section*["conclusion"::conclusion,main_author="Some(@{author ''bu''}::author)"]\<open>Conclusion\<close>
|
||||
text\<open>We presented a formalisation of the most comprehensive semantic model for \<^csp>, a 'classical'
|
||||
language for the specification and analysis of concurrent systems studied in a rich body of
|
||||
literature. For this purpose, we ported @{cite "tej.ea:corrected:1997"} to a modern version
|
||||
|
|
|
|||
Loading…
Reference in New Issue