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.
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, branching bisimulation, or 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 (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). 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.[1] The work was continued by ISTI-CNR of Pisa. The new TAPAs version was developed at the Dipartimento Sistemi ed Informatica of the University of Florence.
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, Springer-Verlag, pages 54–70, 2008.
tapas, model, checker, this, article, needs, additional, citations, verification, please, help, improve, this, article, adding, citations, reliable, sources, unsourced, material, challenged, removed, find, sources, news, newspapers, books, scholar, jstor, dece. This article needs additional citations for verification Please help improve this article by adding citations to reliable sources Unsourced material may be challenged and removed Find sources TAPAs model checker news newspapers books scholar JSTOR December 2022 Learn how and when to remove this template message 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 m 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 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 branching bisimulation or 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 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 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 1 The work was continued by ISTI CNR of Pisa The new TAPAs version was developed at the Dipartimento Sistemi ed Informatica of the University of Florence See also editList of Model Checking ToolsReferences editF 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 Springer Verlag pages 54 70 2008 JACK Just Another Cuncurrency Kit Web pageExternal links editTAPAS website Retrieved from https en wikipedia org w index php title TAPAs model checker amp oldid 1129100403, wikipedia, wiki, book, books, library,
