TAPAs model checker
Encyclopedia
TAPAS is a tool for specifying and analyzing concurrent systems, its aim is to support teaching of process algebras. Systems are described as process algebras 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 double representation of each system: both graphical and textual. After a change in the graphic notation, the textual representation is updated immediately, but when a modification concern of the textual notation the updating has to be forced.
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, in TAPAs, is considered two process algebras: CCSP and PEPA
.
CCSP (= CCS
+ CSP
) is obtained from CCS
by considering some operators of CSP
. Actually, after creating a CCSP process system, the user can analyze it using:
PEPA
(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 and so give rise to a stochastic process, specifically a continuous-time Markov process (CTMC). 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 a collective work, started up in 1990 with the realization of a tool named JACK by IEI CNR of Pisa
and continued by ISTI CNR of Pisa
. The new TAPAs version has been developed at the Dipartimento Sistemi ed Informatica of the University of Florence.
Temporal logic
In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
(expressed as μ-calculus or ACTL
Computational tree logic
Computation tree logic is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realised...
) over the obtained LTS. A key feature of TAPAs, that makes it particularly suited for teaching, is that it maintains a consistent double representation of each system: both graphical and textual. After a change in the graphic notation, the textual representation is updated immediately, but when a modification concern of the textual notation the updating has to be forced.
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, in TAPAs, is considered two process algebras: CCSP and PEPA
PEPA
Performance Evaluation Process Algebra is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s...
.
CCSP (= CCS
Calculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
+ CSP
Communicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...
) is obtained from CCS
Calculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
by considering some operators of CSP
Communicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...
. Actually, after creating a CCSP process system, the user can analyze it using:
- Equivalence CheckerFormal equivalence checkingFormal equivalence checking process is a part of electronic design automation , commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior....
: allows to compare pairs of automatons as regards to many definitions of equivalence (BisimulationBisimulationIn theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
, Branching bisimulation, Decorated traces) - Model checker: 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
PEPA
Performance Evaluation Process Algebra is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s...
(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 and so give rise to a stochastic process, specifically a continuous-time Markov process (CTMC). 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 a collective work, started up in 1990 with the realization of a tool named JACK by IEI CNR of Pisa
Pisa
Pisa is a city in Tuscany, Central Italy, on the right bank of the mouth of the River Arno on the Tyrrhenian Sea. It is the capital city of the Province of Pisa...
and continued by ISTI CNR of Pisa
Pisa
Pisa is a city in Tuscany, Central Italy, on the right bank of the mouth of the River Arno on the Tyrrhenian Sea. It is the capital city of the Province of Pisa...
. The new TAPAs version has been developed at the Dipartimento Sistemi ed Informatica of the University of Florence.
See also
- List of Model Checking Tools
- Model checking
- Temporal logicsTemporal logicIn logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...