A selection of the publications of Diego Latella (most papers can be downloaded from the FM&&T web site)

• Journals:

• M. ter Beek, S. Gnesi, D. Latella, M. Massink, S. Sebastianis.
  Assisting the design of a groupware system - Model checking usability aspects of thinkteam.
  The Journal of Logic and Algebraic Programming. Elsevier Science 78(4):191--232, 2009.
  
  
• R. De Nicola, J.P. Katoen, D. Latella, M. Loreti, and M. Massink.
  Model Checking Mobile Stochastic Logic.
  Theoretical Computer Science. Elsevier. 382(1):42--70, 2007. http://dx.doi.org/10.1016/j.tcs.2007.05.008
  
  
• M. Massink , D. Latella, and S. Gnesi.On Testing UML Statecharts.
  The Journal of Logic and Algebraic Programming. Elsevier Science, 69(1-2):1--74, 2006
  
  
• S. Gnesi, D. Latella, and M. Massink.
  Modular semantics for a UML Statechart Diagrams kernel and its extension to Multicharts and Branching Time Model Checking.
  The Journal of Logic and Algebraic Programming. Elsevier Science, 51(1):43--75, 2002.
  
• A. Bondavalli,  A. Fantechi, D. Latella, and L. Simoncini.
  Design validation of embedded dependable systems.
  IEEE MICRO, 21(5):52--62, 2001.
  
•  A. Bondavalli, M. Dal Cin , D. Latella, I. Majzik, A. Pataricza, and G. Savoia.
  Dependability analysis in the early phases of  UML  based system design.
  Computer Systems Science & Engineering. CRL Publishing Ltd., 16(5):265--275, 2001.
  
• J.P. Katoen, C. Baier, and D. Latella.
  Metric semantics for true concurrent real time.
  Theoretical Computer Science. Elsevier, 254(1-2):501--542, 2001.
  
• S. Gnesi and D. Latella. Guest Editors
  Special issue on formal methods for industrial critical systems.
  Journal of Formal Methods in Systems Design. Kluwer Academic Publishers, 19(2):119--120, 2001
  
• D. Latella, I. Majzik, and M. Massink.
  Automatic verification of a behavioural subset of UML statechart  diagrams using the SPIN model-checker.
  Formal Aspects of Computing. The International Journal of Formal Methods. Springer, 11(6):637--664, 1999.
  
• J. Cuellar, S. Gnesi, and D. Latella. Guest Editors.
  Special issue on formal methods for industrial critical systems.
  Science of Computer Programming. Elsevier, 36(1), 2000.
  
• H. Bowman, G. Faconti, J. Katoen, D. Latella, and M. Massink.
  Automatic verification of a lip-synchronisation protocol using UPPAAL.
  Formal Aspects of Computing. Springer-Verlag, 10(5-6):550--575, 1998.
  
• S. Gnesi and D. Latella. Guest Editors.
  Special issue on formal methods for industrial critical systems.
  Formal Aspects of Computing. Springer-Verlag, 10(4):311--434, 1998.
  
• S. Gnesi and D. Latella. Guest Editors.
  Special issue on formal methods for industrial critical systems.
  Journal of Formal Methods in Systems Design. Kluwer Academic Publishers, 12(2), 1998.
  
• J.P. Katoen, D. Latella, R. Langerak, E. Brinksma, and T. Bolognesi.
  A consistent causality based view on a timed process algebra  including urgent interactions.
  Journal of Formal Methods in Systems Design. Kluwer Academic Publishers, 12(2):189--216, 1998.
  
• E. Brinksma, J. Katoen, R. Langerak, and D. Latella.
  Partial order models for quantitative extensions of LOTOS.
  Computer Networks and ISDN Systems. North-Holland, 30(9-10):925--950, 1998.
  
• E. Brinksma, J.P. Katoen, R. Langerak, and D. Latella.
  A stochastic causality-based process algebra.
  The Computer Journal. Oxford University Press., 38(7):552--565, 1995.
  
• F. Giannotti and D. Latella.
  Gate splitting in LOTOS specifications using abstract interpretation.
  Science of Computer Programming. Elsevier, (23):127--149, 1994.
  
• T. Bolognesi, O. Hagsang, D. Latella, and B. Pehrson.
  The definition of a graphical G-LOTOS editor using the meta-tool LOGGIE.
  Computer Networks and ISDN Systems. North-Holland, 22:61--77, 1991.
  
  
• Books and Proceedings:

• M. Massink, D. Latella, A. Bracciali, J. Hillston.
  Modelling Non-linear Crowd Dynamicsin Bio-PEPA.
  In D. Giannakopoulou and F. Orejas, editors, Fundamental Approaches to Software Engineering (FASE 2011), volume  6603 of LNCS, pages 96--110, Springer-Verlag, 2011.

• M. Massink, D. Latella, A. Bracciali, M. Harrison.
  A Scalable Fluid Flow Process Algebraic Approach to Emergency Egress Analysis.
  In A. Maggiolo Schettini, J. Fiadeiro, and S.Gnesi, editors, 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010), pages 169--180. IEEE Computer Society Press, 2010.

• M. Massink, M. Harrison, D. Latella.
  Scalable Analysis of Collective Behaviour in Smart Service Systems.
  In S. Shin, S. Ossowski, M. Schumacher, M. Palakal, C. Hung, D. Shin, B. Faltings, J. Hong, C. Monnet, and H. Haddad, editors, Proceedings of the 25th Annual ACM Symposium on Applied Computing 2010, pages 1173--1180. Association for Computing Machinery - ACM, 2010.
  
• R. De Nicola, D. Latella, M. Loreti, M. Massink.
  On a Uniform Framework for the Definition of Stochastic Process Languages.
  In M Alpuente, B. Cook, and C. Joubert, editors, Formal Methods for Industrial Critical Systems - FMICS 2009, volume 5825 of LNCS, pages 9--25. Springer-Verlag, 2009.
  
  
• R. De Nicola, D. Latella, M. Loreti, M. Massink.
  Rate-based Transition Systems for Stochastic Process Calculi.
  In Albers S., A. Marchetti-Spaccamela, Y. Matias, S. Nikoletseas,and W. Thomas, editors, Automata, Languages and Programming. Part II,volume 5556 of LNCS, pages 435--446. Springer-Verlag, 2009
  
  
• R. De Nicola, D. Latella, M. Loreti, M. Massink.
  MarCaSPiS: a Markovian Extension of a Calculus for Services.
  In M. Hennessy and B. Klin, editors, Proceedings of the 5^th Workshop on Structural Operational Semantics (SOS 2008), volume 229 of Electronic Notes in Theoretical Computer Science, pages 11--26. Elsevier Science Publishers B.V., 2009.
  
  
• M. Bravetti, D. Latella, M. Loreti, M. Massink, G. Zavattaro.
  Combining Timed Coordination Primitives and Probabilistic Tuple Spaces.
  In C. Kaklamanis and F. Nielson, editors, Trustworthy Global Computing, 4th International Symposium, TGC 2008, Barcelona, Spain, November 3-4, 2008, Revised Selected Papers, volume 5474 of LNCS, pages 52--68. Springer, 2009
  
  
• M. Harrison, M. Massink, D. Latella.
  Engineering Crowd Interaction within Smart Environments.
  In G. Calvary, T. Nicholas Graham, and P.~Gray, editors, Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 117--122. Association for Computing Machinery - ACM, 2009.
  
  
• M. Massink, D. Latella, M. ter Beek, M. Harrison, M. Loreti.
  A Fluid flow Approach to Usability Analysis of Multi-user Systems.
  In P. Forbrig and F. Paterno', editors, Engineering Interactive Systems 2008 (HCSE/TAMODIA 2008). Volume 5247 of LNCS, pages166--180. Springer-Verlag, 2008
  
  
• M. ter Beek, M. Massink, D. Latella.
  Towards Model Checking Stochastic Aspects of the thinkteam User Interface.
  In  Design, Specification, and Verification of Interactive Systems 2005
  Volume 3941 of Lecture Notes in Computer Science. Springer-Verlag, pages 39—50, 2005

• R. De Nicola, J. Katoen, D. Latella, M. Massink.
  Towards a Logic for Performance and Mobility.
  In A. Cerone, H. Wiklicky, editors
  Electronic Notes in Theoretical Computer Science, vol 153, pages 161—175. Elsevier Science Publishers B.V., 2006

• M. ter Beek, M. Massink, D. Latella, S. Gnesi, A. Forghieri, M. Sebastianis
  A Case Study on the Automated Verification of Groupware Protocols
  In Proceedings of the 27th International Conference on Software Engineering, pages 596--603.
  Association for Computing Machinery - ACM, 2005.

• R. De Nicola, D. Latella, M. Massink.
  Formal Modeling and quantitative analysis of KLAIM-based mobile systems
  In H. Haddad, L. Liebrock, A. Omicini, R. Wainwright, M. Palakal, M. Wilds, and H. Clausen, editors,
  APPLIED COMPUTING 2005. Proceedings of the 20th Annual ACM Symposium on Applied Computing}, pages 428--435.
   Association for Computing Machinery - ACM, 2005

• D. Latella, M. Massink, H. Baumeister, and M. Wirsing.
  Mobile UML Statecharts with Localities.
  In C. Priami and P. Quaglia, editors,  
  Global Computing: Programming Environments, Languages, Security and Analysis of Systems
  Volume 3267 of Lecture Notes in Computer Science. Springer-Verlag, pages 34—58. 2004

• M. Massink, J-P. Katoen, and D. Latella
  Model Checking Dependability Attributes of Wireless Group Communication.
  In 2004 International Conference on Dependable Systems & Networks, pages 711--720.
  IEEE Computer Society Press, 2004 ISBN 0-7695-2052-9.

• M. ter Beek, M. Massink, D. Latella, and S. Gnesi
  Model Checking Groupware Protocols.
  In F. Darses, R. Dieng, C. Simone, and M. Zacklad, editors,
  Cooperative Systems Design. Scenario-Based Design of Collaborative Systems}},
  volume 107 of Frontiers in Artificial Intelligence and Applications, pages 179--194.
  IOS Press, 2004. ISBN 1 58603 422 7.

• S. Gnesi, D. Latella, and M. Massink.
  Formal Test-case Generation for UML STatecharts.
  In P. Bellini, S. Bohner, and B. Steffen, editors,  
  9th IEEE International Conference on Engineering of Complex Computer Systems, pages 75--84.
  IEEE Computer Society Press, 2004. ISBN 0-7695-2109-6.
• D. Latella and M. Massink.
  On mobility extensions of UML Statecharts; a pragmatic approach.
  In E. Najm, U. Nestmann, and P. Stevens, editors,
  Formal Methods for Open Object-Based Distributed Systems,
  volume 2884 of  Lecture Notes in Computer Science, pages 199--213. Springer-Verlag, 2003.

• L. Andrade, P. Baldan, H. Baumeister, R. Bruni, A. Corradini, R. De Nicola, J. Fiadeiro, F. Gadducci, S. Gnesi, P. Hoffman, N. Koch, P. Kosiuczenko, A. Lapadula, D. Latella, A. Lopes, M. Loreti, M. Massink, F. Mazzanti, U. Montanari, C. Oliveira, R. Pugliese, A. Tarlecki, M. Wermelinger, M. Wirsing and A. Zawlocki
  AGILE: Software Architecture for Mobility
  In M. Wirsing, D. Pattinson, and R. Hennicker, editors,
  Recent Trends in Algebraic Develeopment Techniques---16th International Workshop, WADT 2002, Frauenchiemsee, Germany, Sept.  24--27, 2002,
  volume 2755 of Lecture Notes in Computer Science, pages 1--33. Springer-Verlag, 2003.

• D. Latella and M. Massink.
  Deriving Manuals from Formal Specifications.
  In  J. Jacko and C. Stephanidis, editors,  Proceedings of HCI International 2003, volume 1.
  Lawrence Erlbaum Associates Publishers, pages 163--167, 2003, ISBN 0-8058-4930-0.
  
  
• D. Latella and M. Massink.
  On testing and conformance relations of UML Statechart Diagrams Behaviours
  In International Symposium on Software Testing and Analysis.
  In P. Frankl, editor, Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and
  Analysis. ACM Press, pages 144--153, 2002 (Available as ACM Software Engineering Notes 27(4), ISBN 1-58113-562-9).

• D. Latella and M. Massink.
  A formal testing framework for UML Statechart Diagrams  behaviours: From theory to automatic verification.
  In Sixth IEEE International High-Assurance Systems Engineering Symposium.
  IEEE Computer Society Press, pages 11--22 2001.
  
• T. Ruys, R. Langerak, J. Katoen, D. Latella, and M. Massink.
  Mean runtime analysis of stochastic process algebra using partial orders.
  In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of  Lecture Notes in Computer Science, pages 220--235. Springer-Verlag, 2001.
  
• T. Bolognesi and D. Latella, editors.
  Formal Methods for Distributed System Development.
  Kluwer Academic Publishers, 2000.
  ISBN 0-7923-7968-3.
  
• S. Gnesi, D. Latella, and M. Massink.
  A stochastic extension of a behavioural subset of UML statechart diagrams.
  In L. Palagi and R. Bilof, editors,
  Fifth IEEE International High-Assurance Systems Engineering Symposium,
  pages 55--64. IEEE Computer Society Press, 2000. ISBN 0-7695-0927-4.
  
• S. Gnesi, D. Latella, G. Lenzini, C. Abbaneo, A. Amendola, and P. Marmo.
  An automatic SPIN validation of a safety critical railway control system.
  In 2000 IEEE International Conference on Dependable Systems & Networks,
  pages 119--124. IEEE Computer Society Press, 2000. ISBN 0-7695-0707-7.
  
• S. Gnesi, D. Latella, G. Lenzini, C. Abbaneo, A. Amendola, and P. Marmo.
  Formal specification and validation of a critical system in presence of byzantine errors.
  In S. Graf and M. Schwartzbach, editors,
  Tools and Algorithms  for the Construction and Analysis of Systems,
  volume 1785 of Lecture Notes in Computer Science,
  pages 535--549. Springer-Verlag, 2000.
  
• A. Bondavalli, M. Dal Cin, D. Latella, and A. Pataricza.
  High-level integrated design environment for dependability (HIDE).
  In Proceedings of the 5th Int. Workshop on Object-oriented Real-time Dependable Systems,
  pages 87--92. IEEE Computer Society Press,  2000. ISBN 0-7695-0616-X.
  
• S. Gnesi, D. Latella, and M. Massink.
  Model checking UML statechart diagrams using JACK.
  In A. Williams, editor, Fourth IEEE International High-Assurance Systems Engineering Symposium,
  pages 46--55. IEEE Computer Society Press, 1999. ISBN 0-7695-0418-3.
  
• A. Bondavalli, A. Fantechi, D. Latella, and L. Simoncini.
  Towards a discipline of system engineering: Validation of dependable systems.
  In P. Ammann, B. Barnes, S. Jajodia, and H. Sibley, editors,
  Computer Security, Dependability, & Assurance: From Needs to Solutions,
  pages 144--164. IEEE Press, 1999.ISBN 0-7695-0337-3.
  
• D. Latella, I. Majzik, and M. Massink.
  Towards a formal operational semantics of UML statechart diagrams.
  In P. Ciancarini and R. Gorrieri, editors,
  IFIP TC6/WG6.1 Third  International Conference on Formal Methods for Open Object-Oriented Distributed Systems, pages 331--347. Kluwer Academic Publishers, 1999, ISBN 0-7923-8429-6
  
• C. Baier, J.P. Katoen, and D. Latella.
  Metric semantics for true concurrent real time (Ext. Abs.)
  In K.J. Larsen, S. Skyum, and G. Winskel, editors,
  Automata, Languages and Programming, volume 1443 of  Lecture Notes in Computer  Science,
  pages 568--579. Springer-Verlag, 1998.
  
• H. Bowman, G. Faconti, J. Katoen, D. Latella, and M. Massink.
  Automatic verification of a lip synchronisation algorithm using  UPPAAL - extended version.
  In J.F. Groote, editor,
  Proceedings of the 3th workshop on Formal Methods for Industrial Critical Systems, Amsterdam,
  pages 97--123.  CWI, May 1998, ISBN 9061964806.
  
• D. Latella and P. Quaglia.
  Stochastic analysis via a probabilistic process algebra.
  In E. Brinksma and A. Nymeyer, editors,
  Proceedings of the 5th workshop on process algebras and performance modeling,
  pages 187--206. Univ. of Twente Emschede, June 1997. CTIT Tech. Rep. Series, No 97-14 - ISSN 1381 - 3625.
  
• A. Fantechi, S. Gnesi, and D. Latella.
  Towards automatic temporal logic verification of value passing  process algebra using abstract interpretation.
  In U. Montanari and V. Sassone, editors,
  Concur '96, volume 1119 of Lecture Notes in Computer Science,
  pages 562--578. Springer-Verlag, 1996.
  
• J.P. Katoen, D. Latella, R. Langerak, and E. Brinksma.
  On specifying real-time systems in a causality-based setting.
  In B. Jonsson and J. Parrow, editors,
  4th International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, volume 1135 of  Lecture Notes in Computer Science,
  pages 385--404. Springer-Verlag, 1996.
  
• J.P. Katoen, D. Latella, R. Langerak, E. Brinksma, and T. Bolognesi.
  A consistent causality based view on a timed process algebra.
  In  Third AMAST Workshop on Real-Time Systems,
  pages 212--226, 1996.
  Extended Abstract - Available also as CTIT Technical Report series no 96-03 - ISSN 1381 - 3625.
  
• J. Katoen, E. Brinksma, D. Latella, and R. Langerak.
  Stochastic simulation of event structures.
  In M. Ribaudo, editor,
  Proceedings of the 4th workshop on process algebras and performance modeling,
  pages 21--40. CLUT, Torino, July 1996, ISBN 88-7992-120-7.
  
• T. Bolognesi, D. De Frutos, R. Langerak, and D. Latella.
  Correctness preserving transformations for the early phases of software development.
  In T. Bolognesi and C. A. Vissers J. v. d. Lagemaat, editors,
  LOTOSPHERE - Software Development using LOTOS - Results of the LOTOSPHERE Project,
  pages 161--180. Kluwer Academic Publishers, 1995. ISBN 0-7923-9529-8.
  
• E. Brinksma, J.P. Katoen, R. Langerak, and D. Latella.
  Performance analysis and true concurrency semantics.
  In T. Rus and C. Ratray, editors, \em Theories and Experiences for Real-Time System Development,
  AMAST Series in Computing,
  Chapter 12, pages 309--337.
  World Scientific Publishing Co., Inc., New Jersey - London -  Singapore, 1994.
  Available also as Memoranda Informatica 94-39/TIOS 94-10, University of Twente, June 1994.
  
• J.P. Katoen, R. Langerak, and D. Latella.
  Modeling systems by probabilistic process algebra: An event structures approach.
  In R. Tenney, P. Amer, and M. Uyar, editors,
  FORMAL DESCRIPTION TECHNIQUES, VI - Proceedings of the IFIP TC96/WG6.1 Sixth International
  Conference on Formal Description Techniques - FORTE '93 Boston, MA, USA,
  pages 253--268. North-Holland Publishing Company, 1994.
  
• E. Brinksma, J.P. Katoen, R. Langerak, and D. Latella.
  Performance analysis and true concurrency semantics (extended abstract).
  In U. Herzog and M. Rettelbach, editors,
  Proceedings of the 2nd workshop on process algebras and performance modeling,
  pages 157--174, July 1994. Erlangen, Germany - ISSN 0344-3515.
  
• F. Giannotti and D. Latella.
  Gate splitting in LOTOS specifications using abstract interpretation.
  In M.C. Gaudel and J.P. Jouannaud, editors,
  TAPSOFT '93: Theory and Practice in Software Development - 4th International Joint Conference  CAAP/FASE - Orsay, France - Proceedings, volume 668 of Lecture Notes in Computer Science,
  pages 437--452. Springer-Verlag, 1993.
  
• D. Latella and P. Quaglia.
  A fully parallel calculus of synchronizing processes.
  In M.C. Gaudel and J.P. Jouannaud, editors,
  TAPSOFT '93: Theory and Practice in Software Development - 4th International Joint Conference  CAAP/FASE - Orsay, France - Proceedings, volume 668 of  Lecture Notes in  Computer Science,
  pages 732--745. Springer-Verlag, 1993.
  
• T. Bolognesi, D. Latella, and E. Zuppa.
  Non-standard interpretations of LOTOS specifications.
  In Samson Abramski and T. S. E. Maibaum, editors,
  TAPSOFT '91, Volume 2, volume 494 of  Lecture Notes in Computer Science,
  pages 217--134. Springer-Verlag, 1991.

The complete list of publications can be found in the  Curriculum Vitae  (in italian).

Back to Diego Latella page