2003
Software
Metadata Only Access
JACK3 - Just Another Concurrency Kit [Release 3.0]
Trentanni G
JACK3 stands for /Just Another Concurrency Kit/. It is an environment integrating a set of verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment proposes several functionalities for the design, analysis and verification of concurrent systems specified using process algebra. In particular, the concurrent systems that are suitable to be studied by means of the latest release JACK3-Lite are that ones described by process algebrae as Esterel, Meije, CCS and Basic Lotos. The basic idea of JACK3-Lite is simple: to put together tools for drawing, minimising and partitioning automata, for transforming algebraic processes into automata and to perform model checking on them, under an unified environment with a graphical user interface with the aim of automatizing the various ways by which these tools exchange data each other and giving to the user a general system to build up the preferred specification/verification development cycle in an expandable environment.
Trentanni G
JACK3 stands for /Just Another Concurrency Kit/. It is an environment integrating a set of verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment proposes several functionalities for the design, analysis and verification of concurrent systems specified using process algebra. In particular, the concurrent systems that are suitable to be studied by means of the latest release JACK3-Lite are that ones described by process algebrae as Esterel, Meije, CCS and Basic Lotos. The basic idea of JACK3-Lite is simple: to put together tools for drawing, minimising and partitioning automata, for transforming algebraic processes into automata and to perform model checking on them, under an unified environment with a graphical user interface with the aim of automatizing the various ways by which these tools exchange data each other and giving to the user a general system to build up the preferred specification/verification development cycle in an expandable environment.
See at:
fmt.isti.cnr.it 
| CNR IRIS
2011
Other
Open Access
QuARS versus QuARS Express
Trentanni G
QuARS and QuARS Express (Quality Analyzer of Requirements Specifications) are tools that make it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. The Express edition of QuARS represent a parallel evolution of the main tool exploiting the same core engine for an increased usability and a more expressive set of reports. In this article a comparison is presented.
Trentanni G
QuARS and QuARS Express (Quality Analyzer of Requirements Specifications) are tools that make it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. The Express edition of QuARS represent a parallel evolution of the main tool exploiting the same core engine for an increased usability and a more expressive set of reports. In this article a comparison is presented.
See at:
CNR IRIS 
| ISTI Repository | CNR IRIS
2011
Other
Open Access
Addressing Readability in NL Requirements Analysis
Trentanni G
What is "readability" and why does it matter? According to Wikipedia (2006), "Readability is a measure of the accessibility of a piece of writing, indicating how wide an audience it will reach. Readability is a judgment of how easy a text is to understand". In the following the use of Readability Metrics in automated analysis of Natural Language expressed Requirements is investigated and some use case is presented.
Trentanni G
What is "readability" and why does it matter? According to Wikipedia (2006), "Readability is a measure of the accessibility of a piece of writing, indicating how wide an audience it will reach. Readability is a judgment of how easy a text is to understand". In the following the use of Readability Metrics in automated analysis of Natural Language expressed Requirements is investigated and some use case is presented.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2011
Other
Open Access
QuARS Express - User Manual (version 0.1)
Trentanni G
The QuARS Express (Quality Analyzer of Requirements pecifications - Express edition) is a tool that makes it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. In the following is presented the user manual.
Trentanni G
The QuARS Express (Quality Analyzer of Requirements pecifications - Express edition) is a tool that makes it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. In the following is presented the user manual.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2002
Software
Metadata Only Access
JACK3 - Just Another Concurrency Kit [Release 1.0]
Trentanni G
JACK is an environment based on the use of process algebras, automata and temporal logic formalisms, which supports many phases of the system development process. The idea behind the JACK environment is to integrate different specication and verication tools, independently developed at different research institutes (I.E.I.- C.N.R. and the University of Rome La Sapienza in Italy, and INRIA in France), to provide an environment in which a user can choose from several verication tools by means of auser-friendly graphic interface. This last feature is quite an important one since it is nowadays widely recognized that there is no single specication and verication technique which can cover all aspects of system design in a satisfactory way; rather, different techniques and tools match different stages of design. JACK includes also a model-checker for ACTL, a branching time temporal logic suitable to express proper ties of reactive systems whose behaviour is characterized by the actions they perform and whose semantics is dened by means of Labelled Transition Systems.
Trentanni G
JACK is an environment based on the use of process algebras, automata and temporal logic formalisms, which supports many phases of the system development process. The idea behind the JACK environment is to integrate different specication and verication tools, independently developed at different research institutes (I.E.I.- C.N.R. and the University of Rome La Sapienza in Italy, and INRIA in France), to provide an environment in which a user can choose from several verication tools by means of auser-friendly graphic interface. This last feature is quite an important one since it is nowadays widely recognized that there is no single specication and verication technique which can cover all aspects of system design in a satisfactory way; rather, different techniques and tools match different stages of design. JACK includes also a model-checker for ACTL, a branching time temporal logic suitable to express proper ties of reactive systems whose behaviour is characterized by the actions they perform and whose semantics is dened by means of Labelled Transition Systems.
See at:
fmt.isti.cnr.it | CNR IRIS
2007
Software
Metadata Only Access
WCS - Witness and Counterexample Server - online tool [Release 2.5 , 01 January 2007]
Trentanni G, Meolic R
Witness and counterexample automata (WCA) are automata that recognize the set of finite linear witnesses and counterexamples, respectively. ACTL is an action-based CTL. Program takes the model (subset of standard CCS) and the set of ACTL formulae on the input and produces a textual representation of a corresponding WCA.
Trentanni G, Meolic R
Witness and counterexample automata (WCA) are automata that recognize the set of finite linear witnesses and counterexamples, respectively. ACTL is an action-based CTL. Program takes the model (subset of standard CCS) and the set of ACTL formulae on the input and produces a textual representation of a corresponding WCA.
See at:
fmt.isti.cnr.it | CNR IRIS
2004
Software
Metadata Only Access
WCS - Witness and Counterexample Server - online tool [Release 1.0 , 03 December 2004]
Trentanni G, Meolic R
Witness and counterexample automata (WCA) are automata that recognize the set of finite linear witnesses and counterexamples, respectively. ACTL is an action-based CTL. Program takes the model (subset of standard CCS) and the set of ACTL formulae on the input and produces a textual representation of a corresponding WCA.
Trentanni G, Meolic R
Witness and counterexample automata (WCA) are automata that recognize the set of finite linear witnesses and counterexamples, respectively. ACTL is an action-based CTL. Program takes the model (subset of standard CCS) and the set of ACTL formulae on the input and produces a textual representation of a corresponding WCA.
See at:
fmt.isti.cnr.it | CNR IRIS
2014
Other
Metadata Only Access
Sito Web "SPLC 2014 - 18th International Software Product Line Conference"
Trentanni G
Web Site related to the 18th International Software Product Line Conference (SPLC 2014)
Trentanni G
Web Site related to the 18th International Software Product Line Conference (SPLC 2014)
See at:
CNR IRIS | splc2014.isti.cnr.it
2021
Other
Metadata Only Access
Sito web del laboratorio ISTI "Formal Methods & Tools"
Trentanni G
Web Site related to the Formal Methods and Tools (FMT) Laboratory afferent to the Institute of Information Science and Technologies "Alessandro Faedo" (ISTI) of the National Research Council of Italy (CNR)
Trentanni G
Web Site related to the Formal Methods and Tools (FMT) Laboratory afferent to the Institute of Information Science and Technologies "Alessandro Faedo" (ISTI) of the National Research Council of Italy (CNR)
See at:
CNR IRIS | www.fmt.isti.cnr.it
2013
Other
Metadata Only Access
Sito Web "Vamos 2013 - Seventh International Workshop on Variability Modelling of Software-intensive Systems"
Trentanni G
Web Site related to the Seventh International Workshop on Variability Modelling of Software-intensive Systems (VAMOS) in 2013
Trentanni G
Web Site related to the Seventh International Workshop on Variability Modelling of Software-intensive Systems (VAMOS) in 2013
See at:
CNR IRIS | vamos2013.isti.cnr.it
2010
Other
Metadata Only Access
Sito web "SEFM2010 - The eighth IEEE International Conference on Software Engineering and Formal Methods"
Trentanni G
Web Site related to the eighth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010)
Trentanni G
Web Site related to the eighth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010)
See at:
CNR IRIS | www.sefm2010.isti.cnr.it
2004
Journal article
Open Access
An automatic tool for improving the quality of software requirements
Lami G, Trentanni G
We present the Quality Analyzer for Requirements Specifications (QuARS), an innovative tool that enables the user to analyse NL requirements automatically.Source: ERCIM NEWS, vol. 58, pp. 18-19
Lami G, Trentanni G
We present the Quality Analyzer for Requirements Specifications (QuARS), an innovative tool that enables the user to analyse NL requirements automatically.Source: ERCIM NEWS, vol. 58, pp. 18-19
2004
Conference article
Restricted
Verification on the web of mobile systems
Ferrari G, Gnesi S, Montanari U, Raggi R, Trentanni G, Tuosto E
The vast majority of current available verification environments have been built by sticking to traditional architectural style centralized and without dealing with interoperability and dynamic recongurability. In this paper we present a verification toolkit whose design and implementation exploit the Web service architectural paradigm.DOI: 10.5220/0002660300720074
Metrics:
Ferrari G, Gnesi S, Montanari U, Raggi R, Trentanni G, Tuosto E
The vast majority of current available verification environments have been built by sticking to traditional architectural style centralized and without dealing with interoperability and dynamic recongurability. In this paper we present a verification toolkit whose design and implementation exploit the Web service architectural paradigm.DOI: 10.5220/0002660300720074
Metrics:
See at:
CNR IRIS | CNR IRIS | www.scitepress.org
2010
Book
Open Access
SEFM 2010 - Poster and Tool Demo Session Proceedings
Mazzanti F, Trentanni G
Proceedings of the Poster and Tool Demo Session during the 8th IEEE International Conference on Software and Formal Methods (SEFM 2010) - CNR, Pisa, Italy 13-18 September 2010
Mazzanti F, Trentanni G
Proceedings of the Poster and Tool Demo Session during the 8th IEEE International Conference on Software and Formal Methods (SEFM 2010) - CNR, Pisa, Italy 13-18 September 2010
2003
Software
Metadata Only Access
HAL (History dependant Automata Laboratory) - online version [Release 1.2]
Gnesi S, Pistore M, Trentanni G
The HD-Automata Laboratory (HAL) is an integrated tool set for the specification, verification and analysis of concurrent and distributed systems. The core of HAL are the HD-automata: they are used as a common format for the various history-dependant languages. The HAL environment includes modules which implement decision procedures to calculate behavioral equivalences, and modules which support verification of behavioral properties expressed as formulae of suitable temporal logics. At this moment HAL works only with concurrent and distributed systems expressed by pi-calculus formalism. The HAL environment allows pi-calculus agents to be translated into ordinary automata, so that existing equivalence checkers can be used to calculate whether the pi-calculus are bisimilar. The environment also supports verification of logical formulae expressing desired properties of the behavior of pi-calculus agents.
Gnesi S, Pistore M, Trentanni G
The HD-Automata Laboratory (HAL) is an integrated tool set for the specification, verification and analysis of concurrent and distributed systems. The core of HAL are the HD-automata: they are used as a common format for the various history-dependant languages. The HAL environment includes modules which implement decision procedures to calculate behavioral equivalences, and modules which support verification of behavioral properties expressed as formulae of suitable temporal logics. At this moment HAL works only with concurrent and distributed systems expressed by pi-calculus formalism. The HAL environment allows pi-calculus agents to be translated into ordinary automata, so that existing equivalence checkers can be used to calculate whether the pi-calculus are bisimilar. The environment also supports verification of logical formulae expressing desired properties of the behavior of pi-calculus agents.
See at:
CNR IRIS
2002
Other
Open Access
Verification on the WEB
Ferrari G, Gnesi S, Montanari U, Raggi R, Trentanni G, Tuosto E
Web services allow the components of applications to be highly decentralized, dynamically reconfigurable. Moreover, Web services can interoperate easily inside an eterogeneous network environment. The vast majority of current available verification environments have been built by sticking to traditional architectural styles. Hence, they are centralized and none of them deal with interoperability and dynamic reconfigurability. In this paper we present a verification toolkit whose design and implementation exploit the Web service architectural paradigm. We describe the architectural design and the discuss in detail the current implementation efforts.
Ferrari G, Gnesi S, Montanari U, Raggi R, Trentanni G, Tuosto E
Web services allow the components of applications to be highly decentralized, dynamically reconfigurable. Moreover, Web services can interoperate easily inside an eterogeneous network environment. The vast majority of current available verification environments have been built by sticking to traditional architectural styles. Hence, they are centralized and none of them deal with interoperability and dynamic reconfigurability. In this paper we present a verification toolkit whose design and implementation exploit the Web service architectural paradigm. We describe the architectural design and the discuss in detail the current implementation efforts.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2007
Other
Open Access
Conciliating TOP-DOWN and BOTTOM-UP approaches in Websites quality evaluation
Biscoglio I, Trentanni G
Websites are the most important media of our times. Consequently a method which allows us to better evaluate websites quality is priceless. In this paper two websites evaluation opposite approaches, namely "bottom-up" and "top-down", are compared and an hypothesis of their meeting in the middle is shown.
Biscoglio I, Trentanni G
Websites are the most important media of our times. Consequently a method which allows us to better evaluate websites quality is priceless. In this paper two websites evaluation opposite approaches, namely "bottom-up" and "top-down", are compared and an hypothesis of their meeting in the middle is shown.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2007
Other
Open Access
QuARS. User Manual (version 0.5)
Lami G, Trentanni G
The QuARS (Quality Analyzer of Requirements Specifications) tool makes it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. In the following is presented the user manual.
Lami G, Trentanni G
The QuARS (Quality Analyzer of Requirements Specifications) tool makes it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. In the following is presented the user manual.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2007
Other
Open Access
Strumenti per la valutazione software di Sistemi di Biglietterie Automatizzate di tipo client-server per la gestione di eventi (spettacoli e intrattenimenti) con posti non numerati
Coco A, Trentanni G
L'ispezione e la valutazione dei Sistemi Informatici di Emissione Biglietti (o Biglietterie Elettroniche) per eventi e spettacoli è parte integrante del processo di certificazione degli apparecchi misuratori fiscali. In questo documento viene presentato uno strumento sviluppato in ambiente MS Excel per le verifiche funzionali di una biglietteria automatizzata di tipo client-server idonea all'emissione e gestione di titoli di accesso per intrattenimenti e attività spettacolistiche con posti non numerati.
Coco A, Trentanni G
L'ispezione e la valutazione dei Sistemi Informatici di Emissione Biglietti (o Biglietterie Elettroniche) per eventi e spettacoli è parte integrante del processo di certificazione degli apparecchi misuratori fiscali. In questo documento viene presentato uno strumento sviluppato in ambiente MS Excel per le verifiche funzionali di una biglietteria automatizzata di tipo client-server idonea all'emissione e gestione di titoli di accesso per intrattenimenti e attività spettacolistiche con posti non numerati.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2007
Other
Open Access
Strumenti per la valutazione software di Sistemi di Biglietterie Automatizzate di tipo client-server per la gestione di eventi (spettacoli e intrattenimenti) con posti numerati e abbonamenti
Coco A, Trentanni G
L'ispezione e la valutazione dei Sistemi Informatici di Emissione Biglietti (o Biglietterie Elettroniche) per eventi e spettacoli è parte integrante del processo di certificazione degli apparecchi misuratori fiscali. In questo documento viene presentato uno strumento sviluppato in ambiente MS Excel per le verifiche funzionali di una biglietteria automatizzata di tipo client-server idonea all'emissione e gestione di titoli di accesso (per singolo ingresso e abbonamenti a turno fisso e a turno libero) per intrattenimenti e attività spettacolistiche con posti numerati e controllo degli accessi abilitati.
Coco A, Trentanni G
L'ispezione e la valutazione dei Sistemi Informatici di Emissione Biglietti (o Biglietterie Elettroniche) per eventi e spettacoli è parte integrante del processo di certificazione degli apparecchi misuratori fiscali. In questo documento viene presentato uno strumento sviluppato in ambiente MS Excel per le verifiche funzionali di una biglietteria automatizzata di tipo client-server idonea all'emissione e gestione di titoli di accesso (per singolo ingresso e abbonamenti a turno fisso e a turno libero) per intrattenimenti e attività spettacolistiche con posti numerati e controllo degli accessi abilitati.
See at:
CNR IRIS | ISTI Repository | CNR IRIS