Matches in DBpedia 2014 for { <http://dbpedia.org/resource/TAPAs_model_checker> ?p ?o. }
Showing items 1 to 32 of
32
with 100 items per page.
- TAPAs_model_checker abstract "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:Equivalence Checker: allows to compare pairs of automatons as regards to many definitions of equivalence (Bisimulation, 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 (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.".
- TAPAs_model_checker wikiPageExternalLink jack3.html.
- TAPAs_model_checker wikiPageExternalLink index.htm.
- TAPAs_model_checker wikiPageExternalLink www.dsi.unifi.it.
- TAPAs_model_checker wikiPageExternalLink er37j25211820k63.
- TAPAs_model_checker wikiPageExternalLink www.unifi.it.
- TAPAs_model_checker wikiPageID "24748419".
- TAPAs_model_checker wikiPageRevisionID "521682358".
- TAPAs_model_checker hasPhotoCollection TAPAs_model_checker.
- TAPAs_model_checker subject Category:Model_checkers.
- TAPAs_model_checker type Assistant109815790.
- TAPAs_model_checker type Attendant109821831.
- TAPAs_model_checker type CausalAgent100007347.
- TAPAs_model_checker type Checker109913110.
- TAPAs_model_checker type LivingThing100004258.
- TAPAs_model_checker type ModelCheckers.
- TAPAs_model_checker type Object100002684.
- TAPAs_model_checker type Organism100004475.
- TAPAs_model_checker type Person100007846.
- TAPAs_model_checker type PhysicalEntity100001930.
- TAPAs_model_checker type Whole100003553.
- TAPAs_model_checker type Worker109632518.
- TAPAs_model_checker type YagoLegalActor.
- TAPAs_model_checker type YagoLegalActorGeo.
- TAPAs_model_checker comment "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.".
- TAPAs_model_checker label "TAPAs model checker".
- TAPAs_model_checker sameAs m.09v25lm.
- TAPAs_model_checker sameAs Q7669326.
- TAPAs_model_checker sameAs Q7669326.
- TAPAs_model_checker sameAs TAPAs_model_checker.
- TAPAs_model_checker wasDerivedFrom TAPAs_model_checker?oldid=521682358.
- TAPAs_model_checker isPrimaryTopicOf TAPAs_model_checker.