Using Hoare Logic in a Process Algebra Setting

This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning with the equational axioms of the process algebra.

CASE STUDIES IN THE HYBRID PROCESS ALGEBRA HyPA

HyPA is an algebraic theory based on the classical process algebra Algebra of Communicating Processes (ACP) for the specification and analysis of hybrid systems. We have the idea that HyPA is also well suited for addressing various aspects of digital embedded systems including hardware, software and concurrency, as well as mixed-signal designs. To show that HyPA is useful for the specification and analysis of hybrid systems and that our idea is correct, we illustrate the use of HyPA with some case studies: a point-to-point communication , a thermostat, a positive-edge-triggered D flip flop, and a small part of a mixed-signal fuzzy controller.

Syntax and Defining Equations for an Interrupt Mechanism in Process Algebra1

A mechanism is introduced to describe priorities in ACP, the algebra of communicating processes, whereby some actions have priority over others in a non-deterministic choice (or sum). This mechanism can be used to model the working of interrupts in a distributed system. This is illustrated in an extensive example.