Curriculum vitæ and research interests of Angelo Morzenti

1 Studies and academic activity

Born in 1960, Angelo Morzenti graduates at Liceo Scientifico F. Lussana, in Bergamo, in 1978. Thanks to a scholarship by American Field Service, he spends the next year in Darlington, Wisconsin, where he studies at Darlington High School, graduating in June 1979.

He graduates in Electronic Engineering at Politecnico di Milano in March 1985. From July 1985 to September 1986 he serves as a lieutenant in the Italian army.

In 1988 he gets a Ph.D. (Dottorato di Ricerca) in Ingegneria Elettronica dell'Informazione e dei Sistemi at Dipartimento di Elettronica of Politecnico di Milano. He participates to the NATO International summer school on Costructive Methods in Computing Science in Marktoberdorf, Germany in July/August 1988.

From 1990 he is researcher, and from 1998 associate professor at Dipartimento di Elettronica e Informazione of Politecnico di Milano. From Febbruary 1999 he is member of "Nucleo di Valutazione" of Politecnico di Milano.

2 Research Interests and Scientific Activity

The research interests of Angelo Morzenti are centered on languages, methods, and tools for the specification, the analysis and the design computer based systems with a particular emphasis on real-time, safety-critical, and distributed systems.

2.1 Specification, validation, and verification of time- and safety-critical systems

In [GGM 86, GGM87] logic programming is proposed as a paradigm for real-time system specification. In his doctoral thesis, Angelo Morzenti defines a new formal notation for executable specification of real-time systems. The study of the linguistic aspects of formal methods leads to the formulation of a language called TRIO, a temporal logic with metric on time, suitable for the specification and analysis of time critical systems [GMM 89, GMM 90]. The TRIO language constitutes the kernel of a specification environment, outlined in [MRR 89a], whose components are described in detail in [F&M 91] and [F&M 92, F&M 94], while [MRR 89] deals with issues related with the adoption of logic programming to support execution of TRIO specifications. The theoretical basis for the execution of TRIO specification are laid out in [MMG 92]. TRIO is successfully employed for the specification of timing aspects of hardware in [CMS 90, CMS 91].

Angelo Morzenti’s most relevant contributions to the research on methods and languages for the specification, validation, and verification of (time- and safety- critical) computer based systems include the following.

Angelo Morzenti’s work on the specification, validation, and verification of time- and safety-critical computer-based systems receive a high appraisal and have a vast influence in the international scientific computer science community, as testified by the following honors.

Besides the cited academic acknowledgments, which testify its scientific relevance, the work of Angelo Morzenti on the specification, validation, and verification of time- and safety- critical systems find an immediate and significant industrial application, in the development of complex automation systems at the Automation Center of ENEL, the Italian Energy Board, at FIAR SpA, at Italtel Telesys, and at Società Metropolitana Milanese [MPV 92, M&P 93, GLM96, CCM99]. The TRIO language and related methodology have been the foundation of several applied research projects, as listed below:

It is to be noticed that the ARTS and FAST projects, both based on the TRIO language and method, have been conceived and conducted outside and independently of Politecnico di Milano. The specification, validation and verification environment based on TRIO and developed at Politecnico di Milano is distributed to several academic and industrial institutions, among which ENEL-CRA (Automation Center of ENEL, the Italian Energy Board at Cologno Monzese); CISE SpA, Department of Computer Science at University of Maryland a College Park, MD, USA; Faculty of Technical Mathematics & Informatics dell’Università di Delft, Netherlands.

2.2 Specification, design and analysis of communication protocols and distributed systems

In 1986/87 Angelo Morzenti cooperates with CREI (Centro Rete Europea Informatica) in the ESPRIT project SEDOS (Software Environment for the Design of Open distributed Systems) for the specification of communication protocols. The research activity is centered on the use of formal methods for the specification protocols, based on extended state machines, with a particular emphasis on the specification of communication protocols of the ISO/OSI hierarchy [LMP 89]. In the framework of the ESPRIT project OpenDreams, Angelo Morzenti contributes to the definition of methods and tools for the specification of distributed systems based on the object based CORBA architecture, where modular specifications of the interactions between distributed components of a Supervision and Control application are systematically transformed into a high-level project and are used to verify the implementation [CCM98, CCM98a, MPR99].

2.3 Specification and prototyping of information systems through executable DFD

The research on formal methods for requirements specification of information systems leads to the definition of an extension of Data Flow Diagrams that allows the designer to express aspects related to synchronization and control of the processes that are defined in the analysis phase, and therefore provides executability to specification, permitting the construction of prototypes of the specified systems [FGM 88, FGM 88a, FGM 89]. The paper [FGM 93], appeared on the international journal "Software Practice and Experience", receives quite favorable reviews from the referees. The paper [GMP 88] illustrates the application of methods that combine and integrate logical formal methods and state machines to obtain executable specifications.

2.4 Specification and modeling of processes for Software production

In the field of software production processes Angelo Morzenti provides a useful contribution in terms of a thorough review of the state of the art and of a proposal of a formalism devoted to the unambiguous description of the processes and their animation [ABG 92, ABG 93, BGM95].

2.5 Problem complexity and approximability through logical characterization

In the field of computational complexity Angelo Morzenti contributes to recent results concerning the approximability of some graph theoretical problems, through their characterization in terms of formulas in higher-order logic. He is co-author of works on the approximability of various problems on maximal spanning trees, [GMM95, GMM97], on the approximability of spanning trees with maximal number of leaves [GMM94], and on the logical definability of such problems [GMM97a].

2.6 Editorial activity

Angelo Morzenti acts as a reviewer for several international conferences, and for Italian and international journals. In particolar, he is reviewer for "IEEE Transactions on Software Engineering", "ACM TOPLAS - Transactions on Programming Languages And Systems", "ACM TOSEM - Transactions on Software Engineering and Methodology", "Formal Methods In System Design", "Euromicro Journal", "Rivista di informatica dell'AICA" and for the conferences "ICSE" (International Conference on Software Engineering) and "ESEC" (European Software Engineering Conference).

References (complete publication list)

[ABG 92] P.Armenise, S.Bandinelli, C.Ghezzi, A.Morzenti, "Software Process Representation Languages: Survey and Assessment", 4th SEKE-International Conference on Software Engineering and Knowledge Engineering, Capri, June 1992.

[ABG 93] P.Armenise, S.Bandinelli, C.Ghezzi, A.Morzenti, "A Survey and Assessment of Software Process Representation Formalisms", International Journal of Software Engineering and Knowledge Engineering, Vol.3, no.3, September 1993.

[AGM97] A.Alborghetti, A.Gargantini, A.Morzenti, "Providing Automated Support to Deductive Analysis of Time Critical Systems", Proc. of Sixth European Software Engineering Conference ESEC 97, pp.211-226, September 22-25, 1997, Zurich, Switzerland.

[BCC95] M.Basso, E.Ciapessoni, E.Crivelli, D.Mandrioli, A.Morzenti, E.Ratto, P.San Pietro, "Experimenting a Logic-Based Approach to the Specification and Design of the Control System of a Pondage Power Plant", ICSE-17 Workshop on Industrial Application of Formal Methods, Seattle, WA, April 1995.

[BGM95] S.Bandinelli, C.Ghezzi, A.Morzenti, "A Survey and Assessment of Software Process Representation Formalisms", in David W. Hurley editor, "Software Engineering and Knowledge Engineering: Trends for the next Decade", Series on Software Engineering and Knowledge Engineering, Vol.4, World Scientific Publ., Singapore, 1995.

[CCC98] E.Ciapessoni, A.Coen-Porisini, E.Crivelli, D.Mandrioli, P.Mirandola, A.Morzenti, "From formal models to formally-based methods: an industrial experience", ACM TOSEM - Transactions On Software Engineering and Methodologies, vol. 8, No 1, January 1999, pages 80-115.

[CCM 90] F.Corsetti, E.Crivelli, D.Mandrioli, A.Montanari, A.Morzenti, P.San Pietro, E.Ratto, "Dealing with different time scales in formal specifications", 10o IEEE-ACM International Workshop on Software Specification and Design, Como, Italy, October 1991.

[CCM98] Riccardo Capobianchi, Alberto Coen-Porisini, Dino Mandrioli, Angelo Morzenti, "A framework architecture for supervision and control systems", accettato per pubblicazione sulla rivista ACM Computing Surveys.

[CCM98a] R.Capobianchi, D.Carcagno, A.Coen Porisini, D.Mandrioli, A.Morzenti, "A framework architecture for the development of new generation supervision and control systems", apparira` in M.Fayad e D.Schmidt eds., "Object Oriented Application Frameworks", John Wiley & sons. .

[CCM99] A. Casazza, D. Comini, A. Morzenti, M. Pradella, P. San Pietro, F. Schreiber, "Specification and Test Case Generation for the Safety Kernel of the Naples Subway", Proc. of the joint Conferences SCI'99 (Systems, Cybernetics and Informatics), and ISAS'99 (5th International Conference on Information Systems Analysis and Synthesis), July-August 1999, Orlando, Florida, USA, pp 533-540.

[CMS 90] A.Coen Porisini, A.Morzenti, D.Sciuto,"Hardware Specification with the Temporal Logic Language TRIO", TAU’90: 1990 ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, August 1990, Vancouver, British Columbia, Canada.

[CMS 91] A. Coen Porisini, A.Morzenti, D. Sciuto, "Specification and Verification of Hardware Systems using the Temporal Logic Language TRIO", "CHDL ’91: 10th International Symposium on Hardware Description Languages and their Applications", Marseille, France, April 1991.

[F&M 91] M.Felder, A.Morzenti, "Real-Time System Validation by Model Checking in TRIO", 3o Euromicro Workshop on Real-Time Systems, Parigi, Giugno 1991.

[F&M 92] M.Felder, A.Morzenti, "Validating real-time systems by history-checking TRIO specifications", 14th IEEE/ACM International Conference on Software Engineering, Melbourne, 1992.

[F&M 94] M.Felder, A.Morzenti, "Validating real-time systems by history-checking TRIO specifications", ACM TOSEM-Transactions On Software Engineering and Methodologies, vol.3, n.4, October 1994.

[FGM 88] A. Fuggetta, C. Ghezzi, D. Mandrioli, A.Morzenti, "VLP: a Visual Language for Prototyping", IEEE Workshop on Languages for automation, College Park, MD, August 1988.

[FGM 88a] A. Fuggetta, C. Ghezzi, D. Mandrioli, A.Morzenti, "Formal Data Flow Diagrams", 13o Congresso AICA, Cagliari, Settembre 1988; anche rapporto interno n.88-07 del Dipartimento di Elettronica del Politecnico di Milano.

[FGM 89] A. Fuggetta, C. Ghezzi, D. Mandrioli, A. Morzenti, "Toward flexible specification environments", in Advanced Programming Methodologies, G. Cioni e A. Salwicki ed., Academic Press, 1989; anche rapporto interno n.88-12 del Dipartimento di Elettronica del Politecnico di Milano.

[FGM 93] A. Fuggetta, C. Ghezzi, D. Mandrioli, A.Morzenti, "Executable Specifications with Data Flow Diagrams", "Software Practice and Experience", J. Wiley & sons, June 1993.

[FGM98] M.Felder, A.Gargantini, A.Morzenti, "A Theory of Implementation and Refinement in Timed Petri Nets", Theoretical Computer Science 202 (1998) 127-161..

[FM94] M.Felder, A.Morzenti, "A temporal Logic Approach to Implementation and Refinement in Timed Petri Nets", in Proc. of ICTL’94: 1st International Conference on Temporal Logic, Bonn, Germany, July 1994, Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) vol.827, pp.365-381.

[FMM 94] M.Felder, D.Mandrioli, A.Morzenti, "Proving properties of real-time systems through logical specifications and Petri net models", IEEE TSE-Transactions of Software Engineering, vol.20, no.2, Feb.1994, pp.127-141.

[G&M99] A.Gargantini, A.Morzenti, "Automated deductive analysis of time-critical systems based on methodical formal specification", Researcb Report, Politecnico di Milano, Dipartimento di Elettronica e Informazione, September 1999.

[GGM 86] F.Garzotto, C.Ghezzi, D.Mandrioli, A.Morzenti, "An exercise on the specification of real–time systems using logic programming", Rapporto interno no. 86–31, Dipartimento di Elettronica del Politecnico di Milano.

[GGM 87] F. Garzotto, C. Ghezzi, D. Mandrioli, A.Morzenti, "On the specification of Real-Time Systems using Logic Programming", ESEC '87 (European Software Engineering Conference) LNCS 289, Springer Verlag, 1987.

[GLM96] A. Gargantini, L. Liberati, A. Morzenti, C. Zacchetti, "Specifying, Validating, and testing a Traffic Management System in the TRIO environment", Proc. of COMPASS, 11th Annual Conference on Computer Assurance, June 1996, Gaitersburg, MA.

[GLM96] A. Gargantini, L. Liberati, A. Morzenti, C. Zacchetti, "Specifying, Validating, and testing a Traffic Management System in the TRIO environment", Proc. of COMPASS, 11th Annual Conference on Computer Assurance, June 1996, Gaitersburg, MA.

[GMM 89] C. Ghezzi e D. Mandrioli, A.Morzenti, "TRIO, a logic language for executable specifications of real–time systems", 10th French Tunisian Seminar on Computer Science, Tunis, Tunisia, 23-25 Maggio 1989; anche rapporto interno n.89-06 del Dipartimento di Elettronica del Politecnico di Milano.

[GMM 90] C. Ghezzi e D. Mandrioli, A. Morzenti, "TRIO, a logic language for executable specifications of real–time systems", The Journal of Systems and Software, Elsevier Science Publishing, vol.12, no.2, May 1990.

[GMM94] G.Galbiati, F.Maffioli, A.Morzenti, "A short note on the approximability of the maximum leaves spanning tree problem", Information Processing Letters 52 (1994) 45-49.

[GMM95] G. Galbiati, F. Maffioli, A. Morzenti, On the Approximability of Some Maximum Spanning Tree Problem, Lecture Notes in Comp. Science 911, (1995) 300-310. (Proceedings of LATIN '95: Theoretical Informatics, Second Latin American Symposium , Valparaiso, Chile, April 1995).

[GMM97] G.Galbiati, F.Maffioli, A.Morzenti, "On the Approximability of some Maximum Spanning Tree Problems", Theoretical Computer Science 181 (1997), pp. 107-118. .

[GMM97a] G. Galbiati, F. Maffioli, A. Morzenti, "On the Logical Definability of Some Maximum Leaves Problems", in (D.S.Bridges, C.S.Calude, J.Gibbons, S.Reeves, I.H.Witten eds): "Combinatorics, Complexity, & Logic", Proceedings of DMTCS’96 (Discrete Mathematics and Theoretical Computer Science), Auckland, New Zealand, December 1996, pp.214-225, Springer-Verlag Singapore, 1997.

[GMM99] A.Gargantini, D.Mandrioli, A.Morzenti, "Dealing with zero-time transitions in axiom systems" Information and Computation 150, 119-131 (1999).

[GMP 88] C. Ghezzi, A.Morzenti, M. Pezzè, "On the role of software reliability in software engineering", in Software reliability modelling and identification, S. Bittanti ed., Springer Verlag, LNCS 341, 1988; anche rapporto interno n.88-10 del Dipartimento di Elettronica del Politecnico di Milano.

[LMP 89] A. Lombardo, A.Morzenti, S. Palazzo, "On the use of Estelle in the OSI Framework", Computer Standard & Interfaces, Maggio 1989, North Holland, Elsevier Publishers B.V.

[M&P 93] A.Mella and M.Piguet, "Functional specification of the ESSDI’s acquisition subsystem using the TRIO and TRIO+ languages", Annesso tecnico al contratto di Ricerca 49/92, ENEL/CRA, Cologno Monzese, Milano.

[M&S91] A.Morzenti, P. San Pietro, "An Object-Oriented Logic Language for Modular System Specification", ECOOP 91: 5th European Conference on Object-Oriented Programming, Geneve, July 1991.

[M&S94] A.Morzenti, P. San Pietro, "Object-oriented logic specification of time critical systems", ACM TOSEM - Transactions on Software Engineering and Methodologies, vol.3, n.1, January 1994, pp. 56-98.

[MMG 92] A.Morzenti, D. Mandrioli, C. Ghezzi, "A Model-Parametric Real-Time Logic", ACM Transactions on Programming Languages and Systems, Vol.14, n.4, October 1992.

[MMM92] D.Mandrioli, S.Morasca, A.Morzenti, "Functional Test case Generation for Real-Time Systems", DCCA-3: 3rd IFIP Working Conference on Dependable Computing for Critical Applications, Sept.1992. Mondello, Italy.

[MMM95] D.Mandrioli, S.Morasca, A.Morzenti, "Generating Test Cases for Real-Time Systems
from Logic Specifications", ACM TOCS-Transactions On Computer Systems, Vol. 13, No. 4, November 1995. pp.365-398.

[MMS96] S.Morasca, A.Morzenti, P.San Pietro, "Generating Functional Test Cases in-the-large for Time-critical Systems from Logic-based Specifications", Proc. of ISSTA 1996, ACM-SIGSOFT International Symposium on Software Testing and Analysis, January 1996, San Diego, CA, U.S.A.

[Mor 91] A.Morzenti, "La Specifica dei Sistemi in Tempo Reale: Proposta di un Formalismo Logico", ed. CLUP, Collana Atenei, 1991.

[Mor 91b] A.Morzenti, "Validating Real-Time Systems by Executing Logic Specifications", Proceedings of the REX Workshop "Real-Time Theory in Practice", Plasmolen-Mook, The Nederlands, June 1991, "Lecture Notes on Computer Science", n.600, Berlin, 1991, Springer Verlag.

[MPR99] Angelo Morzenti, Matteo Pradella, Matteo Rossi, Stefano Russo, Antonio Sergio "A Case Study in Object-oriented modeling and Design of Distributed Multimedia Applications", Proc. of 2nd IEEE Symposium on Software Engineering for Parallel and Distributed Systems (PDSE'99), pp.217-223, 17-18 may 1999, Los Angeles, CA,

[MPV 92] A.Morzenti, M.Paci, F.Veroni, "Specifica TRIO+ dell’Unità di Elaborazione Periferica", Annesso tecnico al contratto di Ricerca 49/92, ENEL/CRA, Cologno Monzese, Milano.

[MRC 91] A.Montanari, E.Ratto, E.Corsetti, A.Morzenti, "Embedding time granularity in logical specifications of real-time systems", 3rd Euromicro Workshop on Real-Time Systems, Paris, France, June 1991.

[MRR 89] A.Morzenti, E.Ratto, M.Roncato, L.Zoccolante, "Un ambiente per la specifica di sistemi in tempo reale basato su un formalismo logico", 4o Convegno Nazionale di Programmazione Logica, Bologna, Giugno 1989.

[MRR 89a] A.Morzenti, E. Ratto, M. Roncato, L. Zoccolante, "TRIO, a logic formalism for the specification of real–time systems" Euromicro Workshop on real–time, Centro Alessandro Volta, Villa Olmo, Como, 14–16 Giugno, 1989.

[SMM98] Pierluigi San Pietro, Angelo Morzenti, Sandro Morasca, "Generation of Execution Sequences for Modular Time Critical Systems", accettato per pubblicazione sulla rivista IEEE TSE – Transactions on Software Engineering.