TAPAs is a tool for specifying and analyzing concurrent systems. Its aim is to support teaching of process algebras. Systems are described as process algebra terms that are then mapped to
labeled transition systems (LTSs). Properties can be verified by checking equivalences between concrete and abstract system descriptions or by model checking
temporal formulas (expressed as
μ-calculus or
ACTL) over the obtained LTS. A key feature of TAPAs that makes it particularly suited for teaching is that it maintains a consistent graphical and textual representation of each system. After a change in the graphic notation, the textual representation is updated immediately; but after textual modifications, the update of the graphical representation has to be manually triggered.
In TAPAs, concurrent systems are described by means of processes, which are nondeterministic descriptions of system behaviors, and process systems, which are obtained by process compositions. Notably, processes can be defined in terms of other processes or process systems. Processes and process systems are composed by using the operators of a given process algebra. Currently, TAPAs supports two process algebras: CCSP and
PEPA
Performance Evaluation Process Algebra (PEPA) is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s. The language extends classical process algebras such as Milner's ...
.
CCSP (=
CCS +
CSP) is obtained from
CCS by considering some operators of
CSP. After creating a CCSP process system, the user can analyze it using one of the following tools.
*
Equivalence Checker: allows to compare pairs of automata using a choice of equivalence (
bisimulation
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa.
Intuitively two systems are bisimilar if ...
, branching bisimulation, or decorated traces)
*
Model checker
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...
: given a model of a system, test automatically whether this model meets a given specification
* Simulator: following one possible execution path through the system and presenting the resulting execution trace to the user.
PEPA
Performance Evaluation Process Algebra (PEPA) is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s. The language extends classical process algebras such as Milner's ...
(Performance Evaluation Process Algebra) is a stochastic process algebra designed for modeling computer and communication systems introduced by Jane Hillston in the 1990s. The language extends classical process algebras such as Milner's CCS and Hoare's CSP by introducing probabilistic branching and timing of transitions. Rates are drawn from the exponential distribution and PEPA models are finite state, so they give rise to a stochastic process---specifically a continuous-time Markov process (
CTMC
A continuous-time Markov chain (CTMC) is a continuous stochastic process in which, for each state, the process will change state according to an exponential random variable and then move to a different state as specified by the probabilities of ...
). Thus the language can be used to study quantitative properties of models of computer and communication systems such as throughput, utilization and response time as well as qualitative properties such as freedom from deadlock. The language is formally defined using a structured operational semantics in the style invented by Gordon Plotkin.
TAPAS is the result of collective work, beginning in 1990 with a tool named JACK by IEI CNR of
Pisa
Pisa ( , or ) is a city and ''comune'' in Tuscany, central Italy, straddling the Arno just before it empties into the Ligurian Sea. It is the capital city of the Province of Pisa. Although Pisa is known worldwide for its leaning tower, the cit ...
.
JACK (Just Another Cuncurrency Kit) Web page
/ref> The work was continued by ISTI- CNR of Pisa
Pisa ( , or ) is a city and ''comune'' in Tuscany, central Italy, straddling the Arno just before it empties into the Ligurian Sea. It is the capital city of the Province of Pisa. Although Pisa is known worldwide for its leaning tower, the cit ...
. The new TAPAs version was developed at the Dipartimento Sistemi ed Informatica of the University of Florence.
See also
* List of Model Checking Tools
This article lists model checking tools and gives an overview of the functionality of each.
Overview of some model checking tools
The following table includes model checkers that have
# a web site from which it can be downloaded,
# a declared li ...
References
*F. Calzolai, R. De Nicola, M. Loreti, F. Tiezzi
TAPAs: a Tool for the Analysis of Process Algebras
In Transactions on Petri Nets and Other Models of Concurrency (ToPNoC) Special Issue, volume 5100 of LNCS
''Lecture Notes in Computer Science'' is a series of computer science books published by Springer Science+Business Media since 1973.
Overview
The series contains proceedings, post-proceedings, monographs, and Festschrifts. In addition, tutorials, ...
, Springer-Verlag
Springer Science+Business Media, commonly known as Springer, is a German multinational publishing company of books, e-books and peer-reviewed journals in science, humanities, technical and medical (STM) publishing.
Originally founded in 1842 in ...
, pages 54–70, 2008.
{{reflist
External links
TAPAS website
Model checkers