(*<*)
―‹ ********************************************************************
* Project : CSP-RefTK - A Refinement Toolkit for HOL-CSP
* Version : 1.0
*
* Author : Burkhart Wolff, Safouan Taha, Lina Ye.
*
* This file : Conclusion
*
* Copyright (c) 2020 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‹Conclusion› (*<*) theory Conclusion imports DiningPhilosophers begin (*>*)
text‹ We presented an analysis of the connection of the refinement notions for CSP, a 'classical'
for the specification and analysis of concurrent systems studied in a rich body of
. A modern formalisation of CSP, called HOL-CSP2.0 or just HOL-CSP and
in the Isabelle AFP @{cite "HOL-CSP-AFP"}, is the basis of this
. In particular, we introduced the theory of the ‹Trace-Divergence-Refinement›term‹P ⊑DT Q›,
is an alternative to the standard refinements known from the literature. \‹NOTE: This part of the theory development has meanwhile been integrated in HOL-CSP2.0.›]
developed a novel set of deadlock - and livelock inference proof principles based on
and denotational characterizations. In particular, we formally investigated the relations
different refinement notions in the presence of deadlock - and livelock; an area where
CSP literature skates over the nitty-gritty details. Finally, we demonstrated how to
these results for deadlock/livelock analysis of protocols.
put a large body of abstract CSP laws and induction principles together to form
verification technologies for generalized classical problems, which have been considered
far from the perspective of data-independence or structural parametricity. The underlying novel
of ``trading rich structure against rich state'' allows one to convert processes
classical transition systems for which established invariant techniques become applicable.
present a first example using these proof methods, notably for Dijkstra's Dining Philosophers;
show that our techniques allow for proving that this cyclic proof architecture is deadlock free
an arbitrary number of philosopher processes.
applications of HOL-CSP 2 could comprise a combination with model checkers, where our theory
its derived rules can be used to certify the output of a model-checker over CSP. In our experience,
transition systems generated by model checkers may be used to steer inductions or to construct
normalized processes ‹Pnorm[τ,υ]› automatically, thus combining efficient finite reasoning
finite sub-systems with globally infinite systems in a logically safe way. ›
(*<*) end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
