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

   2016
1Basile D., Chiaradonna S., Di Giandomenico F., Gnesi S. A stochastic model-based approach to analyze reliable energy-saving rail road switch heating systems. In: Journal of Rail Transport Planning and Management, vol. 6 (2) pp. 163 - 181. Elsevier, 2016.           
2Bolognesi T., Lamb A. Simple indicators for Lorentzian causets. In: Classical and Quantum Gravity, vol. 33 (18) article n. 185004. IOP Publishing, 2016.        
3Ciancia V., Latella D., Loreti M., Massink M. Model checking spatial logics for closure spaces. In: Logical Methods in Computer Science, vol. 12 (4) pp. 1 - 51. Logical Methods in Computer Science, 2016.        
4Ciancia V., Latella D., Loreti M., Massink M. Spatio-temporal model-checking for collective adaptive systems. In: Ada User Journal. The journal for the international Ada community, vol. 37 (4) pp. 223 - 227. Special Issue: Workshop proceedings of De-CPS 2016. Ada Europe, 2016.     
5Cognini R., Corradini F., Gnesi S., Polini A., Re B. Business process flexibility - a systematic literature review with a software systems perspective. In: Information Systems Frontiers. A Journal of Research and Innovation, vol. 2016 Springer, [Online First 22 July 2016]        
6Ferrari A., Spoletini P., Gnesi S. Ambiguity and tacit knowledge in requirements elicitation interviews. In: Requirements Engineering, vol. 21 (3) pp. 333 - 355. Springer, 2016. [Online First 26 March 2016]           
7Gnesi S., Bacciu D., Carta A., Semini L. Adopting a machine learning approach in the design of smart transportation systems. In: ERCIM News, vol. 105 pp. 24 - 24. Ercim, 2016.  
8Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F. Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. In: Journal of Logical and Algebraic Methods in Programming, vol. 85 (2) pp. 287 - 315. [Online first: 2015-11-30] Elsevier, 2016.        

Contribution to Book/Monograph

   2016
1Bolognesi T. Humanity is much more than the sum of humans. In: How Should Humanity Steer the Future?. pp. 15 - 26. Anthony Aguirre, Brendan Foster, Zeeya Merali (eds.). (The Frontiers Collection, vol. 2016). Cham, Switzerland: Springer, 2016.        
2Bolognesi T. Let's consider two spherical chickens. In: Trick or Truth? The Mysterious Connection Between Physics and Mathematics. pp. 55 - 66. Anthony Aguirre, Brendan Foster, Zeeya Merali (eds.). (The Frontiers Collection, vol. 2016). Switzerland: Springer, 2016.        
3Bolognesi T. Spacetime computing: towards algorithmic causal sets with special-relativistic properties. In: Advances in Unconventional Computing. Volume 1: Theory. pp. 267 - 304. Andrew Adamatzky (ed.). (Emergence, Complexity and Computation, vol. 22 (2017)). Switzerland: Springer, 2016.        
4Ciancia V., Latella D., Loreti M., Massink M. Spatial logic and spatial model checking for closure spaces. In: Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems. pp. 156 - 201. Bernardo M., De Nicola R., Hillston J (eds.). (Lecture Notes in Computer Science, vol. 9700). Germania: Springer, 2016.        
5Fantechi A., Gnesi S. Refinement of behavioural models for variability description. In: From Action Systems to Distributed Systems: the Refinement Approach. pp. 155 - 169. Luigia Petre, Emil Sekerinski (eds.). Berkeley, California, U.S.A.: Chapman and Hall/CRC, 2016.        

Proceedings

   2016
1Basile D., Degano P., Ferrari G., Tuosto E. Playing with our CAT and Communication-Centric Applications. In: FORTE 2016 - Formal Techniques for Distributed Objects, Components, and System. 36th IFIP WG 6.1 International Conference (Heraklion, Crete, Greece, 6-9 June 2016). Proceedings, pp. 62 - 73. Elvira Albert, Ivan Lanese (eds.). (Lecture Notes in Computer Science, vol. 9688). Springer International Publishing, 2016.           
2Basile D., Di Giandomenico F., Gnesi S. Tuning energy consumption strategies in the railway domain: a model-based approach. In: ISoLA 2016 - Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. 7th International Symposium (Corfu, Greece, 10-14 October 2016). Proceedings, vol. II pp. 315 - 330. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 9953). Springer International Publishing, 2016.           
3Belmonte G., Ciancia V., Latella D., Massink M. From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging. In: FORECAST 2016 - Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems (Vienna, Austria, 8 July 2016). Proceedings, pp. 81 - 92. (Electronic Proceedings in Theoretical Computer Science, vol. 217). EPTCS.org, 2016.        
4Bolognesi T., Ciancia V. Nominal cellular automata. In: ICE 2016 - 9th Interaction and Concurrency Experience (Heraklion, Crete, Greece, 8-9 June 2016). Proceedings, pp. 24 - 35. (Electronic Proceedings in Theoretical Computer Science, vol. 223). EPTCS.org, 2016.        
5Calabrò A., Lonetti F., Marchetti E., Spagnolo G. O. Enhancing business process performance analysis through coverage-based monitoring. In: QUATIC 2016 - 10th International Conference on the Quality of Information and Communications Technology (Lisbon, Portugal, 6-9 September 2016). Proceedings, pp. 35 - 43. IEEE, 2016.     
6Ciancia V., Latella D., Massink M., Paskauskas R., Vandin A. A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: ISOLA 2016 - Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium (Corfu, Greece, 10-14 October 2016). Proceedings, vol. Part I pp. 657 - 673. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 9952). Springer, 2016.        
7Ciancia V., Latella D., Massink M. On-the-fly mean-field model-checking for attribute-based coordination. In: COORDINATION 2016 - DisCoTec 2016 - Coordination Models and Languages. 18th IFIP WG 6.1 International Conference - Held as Part of the 11th International Federated Conference on Distributed Computing Techniques (Heraklion, Crete, Greece, 6-9 June 2016). Proceedings, pp. 67 - 83. A. Lluch Lafuente, J. Proença (eds.). (Lecture Notes in Computer Science, vol. 9686). Springer, 2016.        
8De Angelis G., Ferrari A., Gnesi S., Polini A. Collaborative requirements elicitation in a european research project. In: SAC 2016 - 31st Annual ACM Symposium on Applied Computing (Pisa, Italy, 4-8 April 2016). Proceedings, pp. 1282 - 1289. ACM, 2016.        
9Fantechi A., Ferrari A., Gnesi S. Formal methods and safety certification: challenges in the railways domain. In: ISoLA 2016 - Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. 7th International Symposium (Corfu, Greece, 10-14 October 2016). Proceedings, vol. II pp. 261 - 265. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science (LNCS), vol. 9953). Springer International Publishing, 2016.           
10Ferrari A., Spoletini P., Gnesi S. Ambiguity cues in requirements elicitation interviews. In: RE 2016 - 2016 IEEE 24th International Requirements Engineering Conference (Beijing, China, 12-16 September 2016). Proceedings, pp. 56 - 65. IEEE, 2016.           
11Ferrari A., Spoletini P., Brock C., Shahwar R. Empowering requirements elicitation interviews with vocal and biofeedback analysis. In: RE 2016 - 2016 IEEE 24th International Requirements Engineering Conference (Beijing, China, 12-16 September 2016). Proceedings, pp. 371 - 376. IEEE, 2016.           
12Franco M., Ferrari A., Spagnolo G. O. Experiments in formal modelling of a deadlock avoidance algorithm for a CBTC system. In: ISoLA 2016 - Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. 7th International Symposium (Corfu, Greece, 10-14 October 2016). Proceedings, vol. II pp. 297 - 314. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 9953). Springer International Publishing, 2016.        
13Latella D. On formal methods for collective adaptive system engineering. {Scalable approximated, spatial} analysis techniques. Extended abstract. In: FORECAST 2016 - FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems (Vienna, Austria, 8 July 2016). Proceedings, pp. 53 - 61. (Electronic Proceedings in Theoretical Computer Science, vol. 217). EPTCS.org, 2016.        
14Sanne U., Witschel H. F., Ferrari A., Gnesi S. Ensuring action: identifying unclear actor specifications in textual business process descriptions. In: IC3K 2016 - International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management (Porto, Portugal, 9-11 November 2016). Proceedings, vol. 3 pp. 140 - 147. Ana Fred, Jan Dietz, David Aveiro, Kecheng Liu, Jorge Bernardino, Joaquim Filipe. SCITEPRESS, 2016.        
15Spagnolo G. O., Marchetti E., Coco A., Scarpellini P., Querci A., Fabbrini F., Gnesi S. An experience on applying process mining techniques to the Tuscan port community system. In: SWQD 2016 - Software Quality. The Future of Systems and Software Development. 8th International Conference (Vienna, Austria, 18-21 January 2016). Proceedings, pp. 49 - 60. Dietmar Winkler, Stefan Biffl, Johannes Bergsmann (eds.). (Lecture Notes in Business Information Processing, vol. 238). Springer, 2016.        
16Ter Beek M. H., Carmona J., Kleijn J. Conditions for compatibility of components: the case of masters and slaves. In: ISoLA'16 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Corfu, Greece, 10-14 October 2016). Proceedings, pp. 784 - 805. T. Margaria, B. Steffen (eds.). (Lecture Notes in Computer Science, vol. 9952). Springer, 2016.        
17Ter Beek M. H., Hähnle R., Schaefer I. Correctness-by-construction and post-hoc verification: friends or foes?. In: ISoLA'16 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Corfu, Greece, 10-14 October 2016). Proceedings, pp. 723 - 729. T. Margaria, B. Steffen (eds.). (Lecture Notes in Computer Science, vol. 9952). Springer, 2016.        
18Ter Beek M. H., Legay A., Lluch Lafuente A., Vandin A. Statistical model checking for product lines. In: ISoLA'16 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Corfu, Greece, 10-14 October 2016). Proceedings, pp. 114 - 133. T. Margaria, B. Steffen (eds.). (Lecture Notes in Computer Science, vol. 9952). Springer, 2016.        
19Ter Beek M. H., Reniers M. A., De Vink E. P. Supervisory controller synthesis for product lines using CIF 3. In: ISoLA'16 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Corfu, Greece, 10-14 October 2016). Proceedings, pp. 856 - 873. T. Margaria, B. Steffen (eds.). (Lecture Notes in Computer Science, vol. 9952). Springer, 2016.        
20Ter Beek M. H., De Vink E. P., Willemse T. A. Towards a feature mu-calculus targeting SPL verification. In: FMSPLE 2016 - Formal Methods and Analysis in Software Product Line Engineering (Eindhoven, The Netherlands, 3 April 2016). Proceedings, vol. 206 pp. 61 - 75. Julia Rubin, Thomas Thüm (eds.). (Electronic Proceedings in Theoretical Computer Science, vol. 206). EPTCS, 2016.        
21Ter Beek M. H., Fantechi A., Gnesi S., Semini L. Variability-based design of services for smart transportation systems. In: ISoLA'16 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Corfu, Greece, 10-14 October 2016). Proceedings, pp. 465 - 481. T. Margaria, B. Steffen (eds.). (Lecture Notes in Computer Science, vol. 9953). Springer, 2016.        

Editorials

   2016
1Gnesi S., Nico P. 4th FME Workshop on Formal Methods in Software Engineering Procedings. pp. vii - vii. ACM, 2016.     
2Gnesi S., Fitzgerald J. S., Heitmeyer C. L., Philippou A., (eds.) .. FM 2016. pp. V - VI. Springer, 2016.        
3Ter Beek M. H., Lisitsa A., Nemytykh A. P., Ravara A., (eds.) .. Automated verification of programs and Web systems. vol. 85 (5, Part 1) pp. 653 - 654. Special Issue on Automated Verification of Programs and Web Systems. Elsevier, 2016.        
4Ter Beek M. H., Gnesi S., Knapp A., (eds.) .. Critical systems: formal methods and automated verification. pp. v - vi. Springer, 2016.        
5Ter Beek M. H., Melgratti H., Torres Vieira H., (eds.) .. Editorial message - Special Track on Service-Oriented Architectures and Programming (SOAP). pp. 1588 - 1589. ACM, 2016.     
6Ter Beek M. H., Clarke D., Schaefer I., (eds.) .. Editorial preface for the JLAMP Special Issue on Formal Methods for Software Product Line Engineering. vol. 85 (1) pp. 123 - 124. Elsevier, 2016.        
7Ter Beek M. H., Loreti M., (eds.) .. Preface. vol. Electronic Proceedings in Theoretical Computer Science, 217 pp. 1 - 2. EPTCS.org, 2016.        

Technical reports

   2016
1Banterle F., Barsocchi P., Candela L., Carlini E., Carrara F., Cassarà P., Ciancia V., Cintia P., Dellepiane M., Esuli A., Gabrielli L., Germanese D., Girardi M., Girolami M., Kavalionak H., Lonetti F., Lulli A., Moreo Fernandez A., Moroni D., Nardini F. M., Monteiro De Lira V. C., Palumbo F., Pappalardo L., Pascali M. A., Reggiannini M., Righi M., Rinzivillo S., Russo D., Siotto E., Villa A. ProgettISTI 2016. Technical report, 2016.  
2Barsocchi P., Candela L., Ciancia V., Dellepiane M., Esuli A., Girardi M., Girolami M., Guidotti R., Lonetti F., Malomo L., Moroni D., Nardini F. M., Palumbo F., Pappalardo L., Pascali M. A., Rinzivillo S. ISTI Young Research Award 2016. Technical report, 2016.  
3Basile D., Chiaradonna S., Di Giandomenico F., Gnesi S. Stochastic model-based evaluation of reliable energy-saving rail road switch heating systems. Progetti: PRIN CINA, PRIN TENACE, Technical report, 2016.  
4Bortolussi L., Ciancia V., Gilmore S., Hillston J., Latella D., Loreti M., Massink M., Nenzi L., PašKauskas R., Tribastone M., Tschaikowski M. Scalable verification for spatial stochastic logics. QUANTICOL Internal Report 3.1. Technical report, 2016.  
5Ciancia V., Latella D., Loreti M., Massink M. Model checking spatial logics for closure spaces - Extended Version. QUANTICOL Technical Report TR-QC-03-2016. Technical report, 2016.  
6Ciancia V., Gilmore S., Grilletti G., Latella D., Loreti M., Massink M. On spatio-temporal model-checking of vehicular movement in public transport systems. QUANTICOL Technical Report TR-QC-02-2016. Technical report, 2016.  
7Ciancia V., Latella D., Massink M. On-the-fly mean-field model-checking for attribute-based coordination preliminary version. Quanticol Technical Report TR-QC-01-2016. Versione semplificata del Technical Report CNR-ISTI 2015-TR-041. Technical report, 2016.  
8Re B., Polini A., Corradini F., Thönssen B., Efendioglu N., Simard J., Sergiacomi A., Balducci A., Giorgio L., Carota S., Ferrari A., Gnesi S., Spagnolo G. O., Bertolino A. LEARN PAD - Demonstrators populated learning platform. Learn PAd - Model-Based Social Learning for Public Administrations. Deliverable D8.3, 2016.  
9Ter Beek M. H., Gnesi S., Knapp A., (eds.) .. Research Ideas FMICS-AVoCS 2016. Research Ideas FMICS-AVoCS 2016 (ISTI-CNR, Pisa, Italy, 26-28 September 2016), Technical report, 2016.  

Software

   2016
1Spagnolo G. O., Ferrari A. Content analysis component. [Software] Release 2.0 , 5 April 2016.  
2Spagnolo G. O., Ferrari A. User Interface for guidelines verification component. [Software] , 5 April 2016.  
3Spagnolo G. O., Ferrari A. User interface for content analysis component. [Software] , 5 April 2016.  
4Spagnolo G. O., Ferrari A. Verification component understandability BPMN. [Software] Release 2.1 , 5 April 2016.  

Dissertations

   2016
1Spagnolo G. O. Agile processes and formal methods in railway systems. Università degli studi di Firenze, Dipartimento di Ingegneria dell'Informazione. Ph.D. Dissertation, 2016.  

Abstracts

   2016
1Basile D., Di Giandomenico F., Gnesi S. Energy-saving buildings assessment through stochastic hybrid model-based evaluation. In: I-CiTies 2016 - 2th CINI Annual Conference on ICT for Smart Cities & Communities (Benevento, Italy, 29-30 Settembre 2016).      
comments to Stefania Gnesi