Proceedings details
Title: Communicating Process Architectures 2012
Editors: Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
Publisher: Open Channel Publishing Ltd., Bicester
ISBN: 978-0-9565409-5-9
Papers
| Title: |
Designing a Concurrent File Server
|
| Authors: |
James Whitehead |
| Abstract: |
In this paper we present a design and architecture for a concurrent file
system server. This architecture is a compromise between the fully
concurrent V6 UNIX implementation, and the simple sequential
implementation in the MINIX operating system. The design of the server
is made easier through the use of a disciplined model of concurrency,
based on the CSP process algebra. By viewing the problem through this
restricted lens, without traditional explicit locking mechanisms, we can
construct the system as a process network of components with explicit
connections and dependencies. This provides us with insight into the
problem domain, and allows us to analyse the issues present in
concurrent file system implementation. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
JCircus 2.0: an Extension of an Automatic Translator from Circus to Java
|
| Authors: |
S.L.M. Barrocas, Marcel Oliveira |
| Abstract: |
The use of formal methods in the development of concurrent systems
considerably reduces the complexity of specifying their behaviour and
verifying properties that are inherent to them. Development, however,
targets the generation of executable programs; hence, translating the
final specification into a practical programming language becomes
imperative. This translation is usually rather problematic due to the
high probability of introducing errors in manual translations: the
mapping from some of the original concepts in the formal concurrency
model into a corresponding construct in the programming language is
non-trivial. In recent years, there is a growing effort in providing
automatic translation from formal specifications into programming
languages. One of these efforts, JCircus, translates specifications
written in Circus (a combination of Z and CSP) into Java programs that
use JCSP, a library that implements most of the CSP constructs. The
subtle differences between JCSP and Circus implementation of
concurrency, however, imposed restrictions to the translation strategy
and, consequently, to JCircus. In this paper, we extend JCircus by
providing: (1) a new optimised translation strategy to multi-way
synchronisation; (2) the translation of complex communications, and; (3)
the translation of CSP sharing parallel and interleaving. A performance
analysis of the resulting code is also in the context of this paper and
provides important insights into the practical use of our results. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
A Distributed Multi-Agent Control System for Power Consumption in Buildings
|
| Authors: |
Anna Kosek, Oliver Gehrke |
| Abstract: |
This paper presents a distributed controller for adjusting the
electrical consumption of a residential building in response to an
external power setpoint in Watts. The controller is based on a
multi-agent system and has been implemented in JCSP. It is modularly
built, capable of self-configuration and adapting to a dynamic
environment. The paper describes the overall architecture and the design
of the individual agents. Preliminary results from proof-of-concept
tests on a real building are included. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Specification of APERTIF Polyphase Filter Bank in ClaSH
|
| Authors: |
Rinse Wester, Dimitrios Sarakiotis, Eric Kooistra, Jan Kuper |
| Abstract: |
ClaSH, a functional hardware description language based on Haskell, has
several abstraction mechanisms that allow a hardware designer to
describe architectures in a short and concise way. In this paper we
evaluate ClaSH on a complex DSP application, a Polyphase Filter Bank as
it is used in the ASTRON APERTIF project. The Polyphase Filter Bank is
implemented in two steps: first in Haskell as being close to a standard
mathematical specification, then in ClaSH which is derived from the
Haskell formulation by applying only minor changes. We show that the
ClaSH formulation can be directly mapped to hardware, thus exploiting
the parallelism and concurrency that is present in the original
mathematical specification. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Schedulability Analysis of Timed CSP Models Using the PAT Model Checker
|
| Authors: |
Oguzcan Oguz, Jan F. Broenink, Angelika Mader |
| Abstract: |
Timed CSP can be used to model and analyse real-time and concurrent
behaviour of embedded control systems. Practical CSP implementations
combine the CSP model of a real-time control system with prioritized
scheduling to achieve efficient and orderly use of limited resources.
Schedulability analysis of a timed CSP model of a system with respect to
a scheduling scheme and a particular execution platform is important to
ensure that the system design satisfies its timing requirements. In
this paper, we propose a framework to analyse schedulability of
CSP-based designs for non-preemptive fixed-priority multiprocessor
scheduling. The framework is based on the PAT model checker and the
analysis is done with dense-time model checking on timed CSP models. We
also provide a schedulability analysis workflow to construct and
analyse, using the proposed framework, a timed CSP model with scheduling
from an initial untimed CSP model without scheduling. We demonstrate
our schedulability analysis workflow on a case study of control software
design for a mobile robot. The proposed approach provides
non-pessimistic schedulability results. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
|
