Formal Methods and Tools Laboratory (FMT)

home | people | topics | projects | publications | software | news


Publications

2002  2003  2004  2005  2006  2007  2008  2009  2010  2011  2012  2013  2014  2015  2016  2017 

 
PUMA, and MetaPub allow for more selective retrieval from the collections of the CNR Institutes; in particular from the CSCE, CNUCE, IEI, and ISTI collections.


Journal articles

   2014
1Ali M., De Angelis F., Fanì D., Bertolino A., De Angelis G., Polini A. An extensible framework for online testing of choreographed services. In: Computer, vol. 47 (2) pp. 23 - 29. IEEE, 2014.        
2Bolognesi T. Teilhard de Chardin e Wolfram: modelli di universo computazionale ed emergenza del foglietto interno delle cose. In: Studium, vol. 110 (3) pp. 340 - 360. Teilhard de Chardin, oggi e domani. Ludovico Galleni (ed.). Edizioni Studium s.r.l, 2014.        
3Fantechi A., Gnesi S., Flalmmini F. Formal methods for railway control systems. In: International Journal on Software Tools for Technology Transfer(STTT), vol. 16 (6) pp. 643 - 646. SCOPUS: 2-s2.0-84919863128. Springer, 2014.        
4Ferrari A., Spagnolo G. O., Menabeni S., Martelli G. From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions. In: International Journal on Software Tools for Technology Transfer, article n. 1. Springer Berlin Heidelberg, [Online First 04 January 2014]        
5Ter Beek M. H., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Massink M. A quantitative approach to the design and analysis of collective adaptive systems for smart cities. In: ERCIM News, vol. 98 pp. 32 - 32. Special issue: Smart Cities. ERCIM, 2014.     
6Ter Beek M. H., Gnesi S., Mazzanti F. KandISTI: a family of model checkers for the analysis of software designs. In: ERCIM News, vol. 99 pp. 31 - 32. Special issue: Software Quality. ERCIM, 2014.     
7Ter Beek M. H., Kleijn J. On distributed cooperation and synchronised collaboration. In: Journal of Automata, Languages and Combinatorics, vol. 19 (1-4) pp. 17 - 32. Otto-von-Guericke-Universität Magdeburg, 2014.     

Contribution to Book/Monograph

   2014
1Ciancia V., Martinelli F., Matteucci I., Morisset C. Quantitative evaluation of enforcement strategies. In: Foundations and Practice of Security. 6th International Symposium. Revised Selected Papers. pp. 178 - 186. Jean Luc Danger, Mourad Debbabi, Jean-Yves Marion, Joaquin Garcia-Alfaro, Nur Zincir Heywood (eds.). (Lecture Notes in Computer Science, vol. 2014). Heidelberg: Springer, 2014.        
2Fantechi A. Twenty-five years of formal methods and railways: what next?. In: Software Engineering and Formal Methods. pp. 167 - 183. Steve Counsell, Manuel Núñez (eds.). (Lecture Notes in Computer Science, vol. 8368). Heidelberg: Springer-Verlag, 2014.        
3Latella D., Loreti M., Massink M. On-the-fly fast mean-field model-checking. In: Trustworthy Global Computing. 8th International Symposium, Revised Selected Papers. vol. 8358 pp. 297 - 314. Martín Abadi, Alberto Lluch Lafuente (eds.). (Lecture Notes in Computer Science, vol. 8358). Switzerland: Springer, 2014.        
4Ter Beek M. H., Kleijn J. Shuffles and synchronized shuffles: a survey. In: Discrete Mathematics and Computer Science. pp. 37 - 50. Gheorghe Paun, Grzegorz Rozenberg, and Arto Salomaa (eds.). Bucuresti, Romania: The Publishing House of the Romanian Academy, 2014.     

Proceedings

   2014
1Bonacchi A., Fantechi A. On the validation of an interlocking system by model-checking. In: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference (Florence, Italy, 11-12 September 2014). Proceedings, pp. 94 - 108. Frédéric Lang, Francesco Flammini (eds.). (Lecture Notes in Computer Science, vol. 8718). Springer-Verlag, 2014.        
2Bortolussi L., Sanguinetti G. A statistical approach for computing reachability of non-linear and stochastic dynamical systems. In: QEST 2014 - Quantitative Evaluation of Systems. 11th International Conference (Florence, Italy, 8-10 September 2014). Proceedings, pp. 41 - 56. Gethin Norman, William Sanders (eds.). (Lecture Notes in Computer Science, vol. 8657). Springer, 2014.           
3Bortolussi L., Paskauskas R. Mean-field approximation and quasi-equilibrium reduction of Markov population models. In: QEST 2014 - Quantitative Evaluation of Systems. 11th International Conference (Florence, Italy, 5-8 September 2014). Proceedings, pp. 106 - 121. Gethin Norman, William Sanders (eds.). (Lecture Notes in Computer Science, vol. 8657). Springer, 2014.           
4Bortolussi L., Lanciani R. Stochastic approximation of global reachability probabilities of Markov population models. In: EPEW 2014 - Computer Performance Engineering. 11th European Workshop (Florence, Italy, 11-12 September 2014). Proceedings, pp. 224 - 239. András Horváth, Katinka Wolter (eds.). (Lecture Notes in Computer Science, vol. 8721). Springer, 2014.           
5Ciancia V., Gilmore S., Latella D., Loreti M., Massink M. Data verification for collective adaptive systems: spatial model-checking of vehicle location data. In: FoCAS @ SASO - FoCAS Workshp @ SASO - 2014 IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops (Imperial College, London, UK, 8 September 2014). Proceedings, pp. 32 - 37. IEEE, 2014.        
6Ciancia V., Latella D., Loreti M., Massink M. Specifying and verifying properties of space. In: TCS 2014 - Theoretical Computer Science. 8th IFIP TC 1/WG 2.2 International Conference (Rome, Italy, 1-3 September 2014). Proceedings, pp. 222 - 235. Josep Diaz, Ivan Lanese, Davide Sangiorgi (eds.). (Lecture Notes in Computer Science, vol. 8705). Springer, 2014.        
7Cognini R., Corradini F., Gnesi S., Polini A., Re B. Research challenges in business process adaptability. In: SAC '14 - 29th Annual ACM Symposium on Applied Computing (Gyeongju, Republic of Korea, 24 - 28 March 2014). Proceedings, pp. 049 - 1054. Yookun Cho and Sung Y. Shin and Sang{-}Wook Kim and Chih{-}Cheng Hung and Jiman Hong (eds.). ACM, 2014.        
8Ferrari A., Dell'Orletta F., Spagnolo G. O., Gnesi S. Measuring and improving the completeness of natural language requirements. In: REFSQ 2014 - Requirements Engineering: Foundation for Software Quality. 20th International Working Conference (Essen, Germany, 7-10 April 2014). Proceedings, pp. 23 - 38. Camille Salinesi, Inge van de Weerd (eds.). (Lecture Notes in Computer Science, vol. 8396). Springer, 2014.        
9Ferrari A., Lipari G., Gnesi S., Spagnolo G. O. Pragmatic ambiguity detection in natural language requirements. In: AIRE 2014 - IEEE 1st International Workshop on Artificial Intelligence for Requirements Engineering (Karlskrona, Germany, 24-26 August 2014). Proceedings, pp. 1 - 8. IEEE, 2014.        
10Gnesi S., Matteucci I., Moiso C., Mori P., Petrocchi M., Vescovi M. My data, your data, our data: managing privacy preferences in multiple subjects personal data. In: APF 2014 - Privacy Technologies and Policy. Second Annual Privacy Forum (Athens, Greece, 20-21 May 2014). Proceedings, pp. 154 - 171. Bart Preneel, Demosthenes Ikonomou (eds.). (Lecture Notes in Computer Science, vol. 8450). Springer, 2014.        
11Latella D., Loreti M., Massink M. On-the-fly probabilistic model checking. In: ICE 2014 - 7th Interaction and Concurrency Experience (Berlin, Germany, 6 June 2014). Proceedings, pp. 45 - 59. Ivan Lanese, Alberto Lluch Lafuente, Ana Sokolova, Hugo Torres Vieira (eds.). (Electronic Proceedings in Theoretical Computer Science -, vol. 166). EPTCS, 2014.        
12Latella D., Loreti M., Massink M., Senni V. Stochastically timed predicate-based communication primitives for autonomic computing. In: QAPL 2014 - Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems (Grenoble, France, 12-13 April 2014). Proceedings, pp. 1 - 16. (Electronic Proceedings in Theoretical Computer Science, vol. 154). EPTCS, 2014.        
13Mazzanti F., Spagnolo G. O., Della Longa S., Ferrari A. Deadlock avoidance in train scheduling: a model checking approach. In: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference (Florence, Italy, 11-12 September 2014). Proceedings, pp. 109 - 123. Frédéric Lang, Francesco Flammini (eds.). (Lecture Notes in Computer Science, vol. 8718). Springer, 2014.        
14Mazzanti F., Spagnolo G. O., Ferrari A. Designing a deadlock-free train scheduler: a model checking approach. In: NFM 2014 - NASA Formal Methods. 6th International Symposium (Houston, TX, USA, 29 April - 1 May 2014). Proceedings, vol. 8430 pp. 264 - 269. Julia M. Badger, Kristin Yvonne Rozier (eds.). (Lecture Notes in Computer Science, vol. 8430). Springer, 2014.        
15Schaefer I., Ter Beek M. H. Formal methods and analyses in software product line engineering (Track Summary). In: ISoLA 2014 - Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. 6th International Symposium (Corfu, Greece, 8-11 October 2014). Proceedings, vol. I pp. 253 - 256. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 8802). Springer, 2014.        
16Spoletini P., Ferrari A., Gnesi S. Context transformations for goal models. In: MoDRE 2014 - IEEE 4th International Model-Driven Requirements Engineering Workshop (Karlskrona, Sweden, 25 August 2014). Proceedings, pp. 17 - 26. IEEE, 2014.        
17Ter Beek M. H., Fantechi A., Gnesi S. Challenges in modelling and analyzing quantitative aspects of bike-sharing systems. In: ISoLA 2014 - Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. 6th International Symposium (Corfu, Greece, 8-11 October 2014). Proceedings, vol. I pp. 351 - 367. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 8802). Springer, 2014.        
18Ter Beek M. H., Gnesi S., Mazzanti F. Model checking value-passing modal specifications. In: PSI 2014 - 9th International Conference on Perspectives of System Informatics (Peterhof, St. Petersburg, Russia, 24-27 June 2014). Proceedings, pp. 1PSI - 11PSI. (Lecture Notes in Computer Science, vol. 8974). A.P. Ershov Institute of Informatics Systems, 2014.  
19Ter Beek M. H., De Vink E. P. Software product line analysis with mCRL2. In: SPLat 2014 - First Workshop on Software Product Line Analysis Tools affiliated with the 18th International Software Product Line Conference (SPLC'14) (Florence, Italy, 16 September 2014). Proceedings, vol. 2 pp. 78 - 85. Stefania Gnesi, Alessandro Fantechi, Maurice ter Beek, Goetz Botterweck, Martin Becker (eds.). ACM, 2014.        
20Ter Beek M. H., De Vink E. P. Towards modular verification of software product lines with mCRL2. In: ISoLA 2014 - Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. 6th International Symposium (Corfu, Greece, 8-11 October 2014). Proceedings, vol. I pp. 368 - 385. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 8802). Springer, 2014.        
21Ter Beek M. H., De Vink E. P. Using mCRL2 for the analysis of software product lines. In: FormaliSE 2014 - 2nd FME Workshop on Formal Methods in Software Engineering (Hyderabad, India, 3 June 2014). Proceedings, pp. 31 - 37. Stefania Gnesi, Nico Plat (eds.). ACM, 2014.        
22Ter Beek M. H., Mazzanti F. VMC: recent advances and challenges ahead. In: SPLat 2014 - First Workshop on Software Product Line Analysis Tools, affiliated with the 18th International Software Product Line Conference (SPLC'14) (Florence, Italy, 16 September 2014). Proceedings, vol. 2 pp. 70 - 77. Stefania Gnesi, Alessandro Fantechi, Maurice ter Beek, Goetz Botterweck, Martin Becker (eds.). ACM, 2014.        

Editorials

   2014
1Gnesi S., Fantechi A., Heymans P., Rubin J., Czarnecki K., Dhungana D., (eds.) .. 18th International Software Product Line Conference. vol. 1 pp. vii - viii. ACM, 2014.     
2Gnesi S., Plat N., (eds.) .. 2nd FME Workshop on Formal Methods in Software Engineering. pp. iii - iv. ACM, 2014.     
3Gnesi S., Rensink A., (eds.) .. Fundamental Approaches to Software Engineering - 17th International Conference,. Springer, 2014.        
4Gnesi S., Fantechi A., Ter Beek M. H., Botterweck G., Becker M., (eds.) .. Proceedings of the 18th International Software Product Line Conference, Volume 2. vol. 2 pp. 1 - 150. Stefania Gnesi, Alessandro Fantechi, Maurice H. ter Beek, Goetz Botterweck, Martin Becker (eds.). ACM, 2014.     
5Massink M., Norman G., Wiklicky H., (eds.) .. Quantitative aspects of programming languages and systems (2011-12). Preface. vol. 538 article n. 1. Elsevier, 2014.        
6Ter Beek M. H., Ravara A., (eds.) .. Proceedings 10th International Workshop on Automated Specification and Verification of Web Systems. vol. 163 pp. i - ii. EPTCS, 2014.        

Technical reports

   2014
1Bolognesi T., Lamb A. Simple indicators for Lorentzian causets. Technical report, 2014.  
2Bolognesi T., Lamb A. Simple indicators for Lorentzian causets (v2). Versione 2 (10 dic. 2014), inviata a ArXiv - Cornell University Library, Technical report, 2014.     
3Bortolussi L., De Nicola R., Feng C., Galpin V., Hillston J., Latella D., Loreti M., Massink M., Senni V. QUANTICOL - CAS-SCEL language design. A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (QUANTICOL). Deliverable D4.1, 2014.  
4Bortolussi L., Cabri G., Di Marzo Serugendo G., Galpin V., Hillston J., Lanciani R., Massink M., Tribastone M., Weyns D. Verification of CAS. In: Dagstuhl Reports (ISSN: 2192-5283) V.4 n. 3/12 - Dagstuhl Publishing. 2014.        
5Ciancia V., Grilletti G., Latella D., Loreti M., Massink M. A spatio-temporal model-checker. QUANTICOL Technical Report TR-QC-10-2014. Technical report, 2014.  
6Ciancia V., Latella D., Massink M. Logics of space and time. QUANTICOL TR-QC-1-2014. Technical report, 2014.     
7Ciancia V., Latella D., Loreti M., Massink M. Specifying and verifying properties of space. QUANTICOL Technical Report TR-QC-06-2014. Technical report, 2014.  
8Ciancia V., Latella D., Loreti M., Massink M. Specifying and verifying properties of space. Extended Version. Logiche spaziali interpretate su spazi di chiusura e loro algoritmi di model checking. Technical report, 2014.     
9De Angelis G., Ferrari A., Gnesi S., Polini A. Software requirements elicitation in the context of a collaborative research project : technical report. Technical report, 2014.  
10De Nicola R., Latella D., Loreti M., Massink M. Two possibly alternative approaches to the semantics of stochastic process calculi. Essays for the Luca Cardelli Fest.. Martin Abadi, Philippa Gardner, Andrew D. Gordon, and Radu Mardare (eds.), pp. 95-108. Microsoft Research Technical Report MSR-TR-2014-104. Technical report, 2014.     
11Galpin V., Bortolussi L., Ciancia V., Clark A., De Nicola R., Feng C., Gilmore S., Gast N., Hillston J., Llunch-Lafuente A., Loreti M., Massink M., Nenzi L., Reijsbergen D., Senni V., Tiezzi F., Tribastone M., Tschaikowski M. QUANTICOL - A preliminary investigation of capturing spatial information for CAS. A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (QUANTICOL). Deliverable D2.1, 2014.  
12Galpin V., Feng C., Hillston J., Massink M., Tribastine M., Tschaikowski M. Review of time-based techniques for modelling space. QUANTICOL Technical Report. Technical report, 2014.  
13Gast N., Bortolussi L., Jane H., Paskauskas R., Trinabastone M. QUANTICOL - Multiscale modelling informed by smart grids. A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (QUANTICOL). Deliverable D1.1, 2014.  
14Gilmore S., Ter Beek M. H., Bortolussi L., Ciancia V., Galpin V., Hillston J., Massink M., Tribastone M. QUANTICOL - Dissemination plan for the project. QUANTICOL: A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours. Deliverable D6.1, 2014.     
15Latella D., Loreti M., Massink M. On-the-fly fluid model checking via discrete time population models - Extended version. Codice TR: TR-QC-08-2014, Technical report, 2014.     
16Latella D., Loreti M., Massink M. On-the-fly probabilistic model checking. Extended version. QUANTICOL Technical Report nr. TR-QC-09-2014. QUANTICOL Technical Report TR-QC-09-2014. Technical report, 2014.     
17Latella D., Loreti M., Massink M., Senni V. Stochastically timed predicate-based communication primitives for autonomic computing - Full Paper. QUANTICOL TR-QC-3-2014. Technical report, 2014.     
18Latella D., Loreti M., Massink M., Senni V. TR 11: On STOCS: a stochastic exten- sion of SCEL. ASCENS TR 11. Technical report, 2014.     
19Massink M. On-the-fly fast mean field model checking for collective adaptive systems. In: Dagstuhl Reports (ISSN: 2192-5283) V.4 n. 3/12 - Dagstuhl Publishing. 2014.        
20Massink M., Bortolussi L., Ciancia V., Hillston J., Lluch-Lafuente A., Latella D., Loreti M., Reijsbergen D., Vandin A. QUANTICOL - Foundations of scalable verification for stochastic logics. A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (QUANTICOL). Deliverable D3.1, 2014.  
21Spagnolo G. O., Ferrari A., Mazzanti F., Della Longa S. CBTC.ATS.006_00_03 Documentazione prototipo ATS. Technical report, 2014.  
22Spagnolo G. O., Coco A., Marchetti E. TCPS specifica business process e log. Technical report, 2014.  
23Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F. A collection of models of a bike-sharing case study. QUANTICOL TR-QC-07-2014. Technical report, 2014.     
24Ter Beek M. H., De Vink E. P. Using mCRL2 for the analysis of software product lines (extended version). Technische Eindhoven University of Technology CSR 14/02. Technical report, 2014.     

Software

   2014
1Ferrari A., Spagnolo G. O. Completeness assistant for requirements. [Software] , 05 May 2014.  
2Spagnolo G. O., Ferrari A., Mazzanti F. Prototipo schedurer ATS. [Software] , 16 December 2014.  
comments to Stefania Gnesi