Italian National Research Council – Institute of Information Science and Technologies

The Institute of Information Science and Technologies (ISTI) is an institute of the Italian National Research Council (CNR), located in Pisa, Italy.  CNR was founded in 1923 as a national public research entity and is currently the largest public research institution of Italy. The first president of CNR was Vito Volterra, who played an active role in the creation of CNR as a national research council connected to the International Research Council of which he was vice-president at that time.

ISTI was constituted in September 2000 as a result of a merge between the Istituto CNUCE, founded in 1967, and the Istituto di Elaborazione dell’Informazione, founded in 1968, formerly Center for Studies on Electronic Computing, founded in 1954, where the first Italian electronic computer was built in 1961.

Expertise. The Formal Methods and Tools Laboratory (FMT) of CNRISTI has acquired a significant expertise in the development of tools and techniques for formal specification and verification through model checking of complex distributed and concurrent systems. Expertise has also been acquired in the area of semantic models, notations and techniques for the integrated modelling and analysis of qualitative and quantitative aspects of system behaviour, addressing scalability and emergent behavior, and the modeling and analysis of variability.

FMT is also involved in the FET Global Computing project ASCENS, on Autonomic Service-component Ensembles (as third party), in the Italian Regional project TRACE.IT on Train Control Enhancement via Information Technology and in the Italian PRIN project CINA. FMT has been recently involved in several other European and Italian projects contributing to the development of logics and model-checking tools for the specification and verification of qualitative and quantitative properties of service-oriented applications.

Role in QUANTICOL. CNR-ISTI will lead the research activities of WP3 (Logic and Scalable Verification Combining Micro and Macro Perspectives) and will play an important and active role in WP1 (Emergent Behaviour and Adaptivity), WP2 (Collective Adaptive Behaviour in Space), WP4 (Language and Design Methodology) and WP6 (Dissemination) by contributing to the development of verification techniques based on scalable quantitative model-checking for CAS and the development of related quantitative models, languages and logics to address spatial issues and variability.

Key members