Process Algebra Compiler
What is The PAC?
The Process Algebra Compiler (PAC) is a tool that eases the task of
changing the design language accepted by the Concurrency Workbench for the New
Century (CWB-NC), a process-algebra-based verification tool. The
CWB-NC allows the user to describe a concurrent system in a design
language such as CCS and analyze the behavior of the system with
different methods such as equivalence checking, preorder checking,
model checking, or random simulation. The CWB-NC is designed in a
modular fashion so that the analysis routines are not dependent on the
specific design language that the tool accepts. Therefore, changing
the design language that the tool accepts is feasable; however, doing
so is a tedious and time-consuming task. The PAC greatly simplifies
this job. Figure 1 shows that given a high-level description of the
syntax and semantics of a design language, the PAC generates Standard
ML source code implementing a front end which allows the CWB-NC to
analyze systems specified in the new language.
Figure 1: Generating a CWB-NC front end for design language "foo"
PAC Language Descriptions
A PAC specification for a language includes a description of the
syntax of the language (given as a Yacc-like grammar) and a
description of the semantics of the language (given as sets of
Plotkin-style SOS rules. High-level, formal notations such as context
free grammars and regular expressions have proven to be ideal input
formats for parser and scanner generators. The PAC extends this
notion by using SOS rules as input for generating routines for
computing various user-defined semantic relations. For example, a
commonly defined semantic relation is one which determines the set of
single step transitions that a term in the specification language is
capable of performing. SOS rules have the following general form.
premises
------------(side condition)
conclusion
The intuitive reading of the rule is that if one is able to establish
the premises, which typically involve statements about the execution
behavior of subprograms of the one mentioned in the conclusion, and
the side condition holds, then one may infer the conclusion. As an
example, the following describes the synchronizations allowed by the
parallel composition operation in CCS.
p -- a --> p', q -- b --> q'
--------------------------------(inverses(a,b))
p | q -- t --> p' | q'
The rule states that if p can engage in an action a
and evolve to p' and q can engage in b and
evolve to q', and a and b are inverses
(i.e. constitute an input/output pair on the same communication
channel), then p|q can execute an internal action, t
(tau), corresponding to the synchronized execution of a and
b.
Although the initial purpose of the PAC was to change the
specifcation languages that verification tools accept, other uses may
be possible. For example, we would like to investigate the possibility
of using the PAC to develop interpreters and compilers. The syntactic
component of the PAC has also been used without the semantic component
as a simple way to generate scanners, parsers, and unparsers. The most
obvious advantage over using Lex and Yacc is that unparsers are also
generated from the grammar given to specify the parser.
A PAC language specification is divided into two files, one
containing the syntactic description (suffixed by .syn) and one
containing the semantic description (suffixed by .sos). Several
examples of PAC input are included with the distribution and the files
for CCS may be viewed here: ccs.syn and
ccs.sos. A complete description of the
PAC input notation is available in the user's manual available on line
via the papers link below.
Papers
Some PAC-related papers are available
here. The PAC User's Manual is
probably the best and most up to date place to start.
Distribution
The PAC is availble for use free of charge! The tool was developed
in the Department of Computer
Science at North Carolina State University (NCSU). Reactive Systems, Inc.
(RSI) is hosting this web site as a service to the research
community. Neither RSI nor NCSU offer any support for the tool and
although you may use the tool as you like, the license for the
software remains with its developers. You may read the license and
then download the distribution here.
The PAC Team
Contact
You may contact us via e-mail at pac@reactive-systems.com.
Acknowledgments
The PAC team would like to thank the US National Science
Foundation and the US Office of Naval Research for their support of
the this project.
|