TAPAs is a software environment for supporting specification and analysis of concurrent systems via Process Algebras. TAPAs supports the use of process algebrae to specify and analyze concurrent systems. Systems are described as process algebras terms that are then mapped to Labelled Transition Systems (LTSs). Properties can be verified by checking equivalences between concrete and abstract system descriptions, or by model checking temporal formulae over the obtained LTS. Now TAPAs has its own wiki page and it is listed on Model Checking Tools wiki page. It is also inserted in this interesting verification tools database.
TAPAs is designed with a plug-in architecture: a set of software components (plug-ins) adds specific capabilities to a larger software application. Each plug-in supports a specific Process Algebra and it can be easy deployed in the TAPAs main application. Actually TAPAs has three different plug-ins that support three Process Algebras: CCSP, PEPA and StoKlaim.
CCSP PluginsThe CCSP (= CCS + CSP) is obtained from CCS by considering some operators of CSP. In CCSP Plugin, concurrent systems are described by means of processes, which are nondeterministic descriptions of system behaviours, and process systems, which are obtained by process compositions. This plug-in is specifically thought for teaching Concurrency Theory to undergraduate students. By its nature, Concurrency Theory is complicated not only study but also to teach. To facilitate the formalization and analysis of complex systems, CCSP plug-in provides both a graphical and textual system specification and it consistently updates terms when the graphical representation is changed and redraw process graphs when textual terms are modified. Moreover this plug-in provides graphical interfaces that guide users in analyzing and debugging the specified models. Actually, after creating a models TAPAs aloow to simulate its behaviour and analyse it using:
- Equivalence Checker which allows to compare pairs of automatons as regards to many definitions of equivalence;
- Model checker which allows to do model checking on processes.
PEPA PluginsPerformance 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 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, utilisation and response time as well as qualitative properties such as freedom from deadlock. Further details can be found in PEPA home page or in its wiki page.
For the specification phase, this plug-in provides a rich graphical interface that simplifies process specification. On the contrary, for the analysis phase, it exploits the PEPA libraries distributed with the "PEPA Eclipse Plug-in" developed by the PEPA group at University of Edinburgh. TAPAs uses this libraries to perform steady state and transient analysis on the specified models.The TAPAs developers would like to thank PEPA group for releasing the PEPA software under GPL license, in particular we would like to thank Mirco Tribastone for helping us in integrate PEPA libraries into TAPAs.
StoBioKlaim pluginThis plugin adds support for StoKlaim, a variant of Klaim. StoKlaim is an experimental language specifically designed to model distributed system with code mobility. StoKlaim is an experimental language specifically designed to model distributed system with code mobility. This plug-in is a research tool used for developing complex case studies. It provides only textual specification and it does not exploit TAPAs embedded analysis tools, but it implements new ones. StoKlaim allows to formalize properties by mean of a stochastic logic that, together with qualitative properties, permits specifying time-bounded probabilistic reachability properties. This plug-in can also be used for supporting analysis of biological system specified in BioKlaim (a variant of StoKlaim) introduced in this thesis. In BioKlaim a "molecules as tuples" approach is used: tuples are used to model the molecules, agents identifies the reactions enabled, and localities are used to model the spatial structure of biological systems.
HistoryTAPAs 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 old TAPAs version has been developed by two students of computer science of University of Florence, Fabio Collini and Massimiliano Gori. The new TAPAs version has been developed by three students of computer science of University of Florence, Francesco Calzolai, Guzman Tierno and Stefano Guerrini.