License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2016.12
URN: urn:nbn:de:0030-drops-98509
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9850/
Go to the corresponding LIPIcs Volume Portal

Igried, Bashar ; Setzer, Anton

Defining Trace Semantics for CSP-Agda

pdf-format:
LIPIcs-TYPES-2016-12.pdf (0.7 MB)

Abstract

This article is based on the library CSP-Agda, which represents the process algebra CSP coinductively in the interactive theorem prover Agda. The intended application area of CSP-Agda is the proof of properties of safety critical systems (especially the railway domain). In CSP-Agda, CSP processes have been extended to monadic form, allowing the design of processes in a more modular way. In this article we extend the trace semantics of CSP to the monadic setting. We implement this semantics, together with the corresponding refinement and equality relation, formally in CSP-Agda. In order to demonstrate the proof capabilities of CSP-Agda, we prove in CSP-Agda selected algebraic laws of CSP based on the trace semantics. Because of the monadic settings, some adjustments need to be made to these laws. The examples covered in this article are the laws of refinement, commutativity of interleaving and parallel, and the monad laws for the monadic extension of CSP. All proofs and definitions have been type checked in Agda. Further proofs of algebraic laws will be available in the repository of CSP-Agda.

BibTeX - Entry

@InProceedings{igried_et_al:LIPIcs:2018:9850,
  author =	{Bashar Igried and Anton Setzer},
  title =	{{Defining Trace Semantics for CSP-Agda}},
  booktitle =	{22nd International Conference on Types for Proofs and  Programs (TYPES 2016)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Silvia Ghilezan and Herman Geuvers and Jelena Ivetić},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9850},
  URN =		{urn:nbn:de:0030-drops-98509},
  doi =		{10.4230/LIPIcs.TYPES.2016.12},
  annote =	{Keywords: Agda, CSP, Coalgebras, Coinductive Data Types, Dependent Type Theory, IO-Monad, Induction-Recursion, Interactive Program, Monad, Monadic Programming, }
}

Keywords: Agda, CSP, Coalgebras, Coinductive Data Types, Dependent Type Theory, IO-Monad, Induction-Recursion, Interactive Program, Monad, Monadic Programming,
Collection: 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Issue Date: 2018
Date of publication: 05.11.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI