4 Search Results for "Woodcock, Jim"

Document
DOI: 10.4230/LIPIcs.ITP.2025.30
Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Authors: Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We formalize nondeterministic asynchronous dataflow networks in Isabelle/HOL. Dataflow networks are comprised of operators that are capable of communicating with the network, performing silent computations, and making nondeterministic choices. We represent operators using a shallow embedding as codatatypes. Using this representation, we define standard asynchronous dataflow primitives, including sequential and parallel composition and a feedback operator. These primitives adhere to a number of laws from the literature, which we prove by coinduction using weak bisimilarity as our equality. Albeit coinductive and nondeterministic, our model is executable via code extraction to Haskell.
Cite as

Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic Asynchronous Dataflow in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.ITP.2025.30,
  author =	{Silva, Rafael Castro Gon\c{c}alves and Fernet, Laouen and Traytel, Dmitriy},
  title =	{{Nondeterministic Asynchronous Dataflow in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{30:1--30:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.30},
  URN =		{urn:nbn:de:0030-drops-246280},
  doi =		{10.4230/LIPIcs.ITP.2025.30},
  annote =	{Keywords: dataflow, verification, coinduction, Isabelle/HOL}
}
Document
DOI: 10.4230/LITES.8.2.3
Higher-Dimensional Timed and Hybrid Automata

Authors: Uli Fahrenberg

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.
Cite as

Uli Fahrenberg. Higher-Dimensional Timed and Hybrid Automata. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 03:1-03:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{fahrenberg:LITES.8.2.3,
  author =	{Fahrenberg, Uli},
  title =	{{Higher-Dimensional Timed and Hybrid Automata}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:16},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.3},
  URN =		{urn:nbn:de:0030-drops-192951},
  doi =		{10.4230/LITES.8.2.3},
  annote =	{Keywords: timed automaton, higher-dimensional automaton, precubical set, real time, non-interleaving concurrency, hybrid automaton}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.20
Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL

Authors: Simon Foster, Chung-Kil Hur, and Jim Woodcock

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for both activities. In this paper we apply Interaction Trees in Isabelle/HOL to produce a verification and simulation framework for state-rich process languages. We develop the core theory and verification techniques for Interaction Trees, use them to give a semantics to the CSP and Circus languages, and formally link our new semantics with the failures-divergences semantic model. We also show how the Isabelle code generator can be used to generate verified executable simulations for reactive and concurrent programs.
Cite as

Simon Foster, Chung-Kil Hur, and Jim Woodcock. Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{foster_et_al:LIPIcs.CONCUR.2021.20,
  author =	{Foster, Simon and Hur, Chung-Kil and Woodcock, Jim},
  title =	{{Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.20},
  URN =		{urn:nbn:de:0030-drops-143973},
  doi =		{10.4230/LIPIcs.CONCUR.2021.20},
  annote =	{Keywords: Coinduction, Process Algebra, Theorem Proving, Simulation}
}
Document
DOI: 10.4230/DagSemProc.09381.1
09381 Extended Abstracts Collection – Refinement Based Methods for the Construction of Dependable Systems

Authors: Jean-Raymond Abrial, Michael Butler, Rajev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock

Published in: Dagstuhl Seminar Proceedings, Volume 9381, Refinement Based Methods for the Construction of Dependable Systems (2010)

Abstract
With our growing reliance on computers, the total societal costs of their failures are hard to underestimate. Nowadays computers control critical systems from various domains such as aerospace, automotive, railway, business etc. Obviously, such systems must have a high degree of dependability – a degree of trust that can be justifiably placed on them. Although the currently operating systems do have an acceptable level of dependability, we believe that they development process is still rather immature and ad-hoc. The constantly growing system complexity poses an increasing challenge on the system developers and requires significant improvement on the existing developing practice. To address this problem, we investigated how to establish a set of refinement-based engineering methods that can provide the designers with a systematic methodology for development of complex systems.
Cite as

Jean-Raymond Abrial, Michael Butler, Rajev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock. 09381 Extended Abstracts Collection – Refinement Based Methods for the Construction of Dependable Systems. In Refinement Based Methods for the Construction of Dependable Systems. Dagstuhl Seminar Proceedings, Volume 9381, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{abrial_et_al:DagSemProc.09381.1,
  author =	{Abrial, Jean-Raymond and Butler, Michael and Joshi, Rajev and Troubitsyna, Elena and Woodcock, Jim C. P.},
  title =	{{09381 Extended Abstracts Collection – Refinement Based Methods for the Construction of Dependable Systems}},
  booktitle =	{Refinement Based Methods for the Construction of Dependable Systems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9381},
  editor =	{Jean-Raymond Abrial and Michael Butler and Rajeev Joshi and Elena Troubitsyna and Jim C. P. Woodcock},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09381.1},
  URN =		{urn:nbn:de:0030-drops-23746},
  doi =		{10.4230/DagSemProc.09381.1},
  annote =	{Keywords: Specification, refinement, verification, modelling, dependable systems}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2022
  • 1 2021
  • 1 2010

  • Refine by Author
  • 1 Abrial, Jean-Raymond
  • 1 Butler, Michael
  • 1 Fahrenberg, Uli
  • 1 Fernet, Laouen
  • 1 Foster, Simon
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 LITES
  • 1 DagSemProc

  • Refine by Classification
  • 2 Theory of computation → Concurrency
  • 1 Computing methodologies → Distributed algorithms
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Data flow languages
  • 1 Theory of computation → Timed and hybrid models

  • Refine by Keyword
  • 2 verification
  • 1 Coinduction
  • 1 Isabelle/HOL
  • 1 Process Algebra
  • 1 Simulation
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact