Formal Requirements Modeling for Simulation-Based Verification: from theory to practice Alfredo Garro Department of Informatics, Modeling, Electronics and Systems Engineering (DIMES), University of Calabria Via Ponte P. Bucci 41C, Rende (CS), 87036 Italy alfredo.garro@unical.it Copyright © held by the author. ABSTRACT through a Probability Model. Proceedings of the 6th International Workshop on Applied Modeling and Simulation (WAMS), Buenos Modeling of system properties deals with formally Aires, Argentina, 24-27 November, 2013. expressing constraints and requirements that influence and [5] A. Garro, A. Tundis, L. Rogovchenko-buffoni, P. Fritzson. From Safety determine the structure and behavior of a system. System Requirements to Simulation-driven Design of Safe Systems. Proceedings Property Models enable the verification of system properties of the 12th International Conference on Modeling and Applied Simulation (MAS 2013), Athens, Greece, 25 - 27 September, 2013. through real or simulated experiments so as to support their evaluation during system design and their monitoring during [6] L. Rogovchenko-Buffoni, P. Fritzson, A.Garro, A. Tundis, and M. Nyberg. Requirement Verification and Dependency Tracing During system operation. However, several challenges should be Simulation in Modelica. Proceedings of the 8th EUROSIM Congress on addressed to effectively handle systems properties, ranging Modelling and Simulation (EUROSIM 2013), Cardiff, Wales, UK, 10- from conceptual properties representation to tracing and 13 September, 2013. verification. In this context, the tutorial aims at discussing these [7] A. Tundis, L. Rogovchenko-buffoni, P. Fritzson, A. Garro. Modeling main challenges and presenting some promising solutions by System Requirements in Modelica: Definition and Comparison of focusing on those resulting from recent Systems Engineering Candidate Approaches. Proceedings of the 5th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools research efforts. In particular, a proposal on how to model (EOOLT 2013), University of Nottingham, UK, 19 April, 2013. formal requirements in Modelica for simulation-based verification is presented. The approach is implemented in the AUTHOR BIOGRAPHY open source Modelica_Requirements library. It requires extensions to the Modelica language that have been Alfredo Garro is an Associate Professor of Computer and prototypically implemented in the Dymola and Open-Modelica Systems Engineering at the Department of Informatics, software. The design of the library is based on the FOrmal Modeling, Electronics and Systems Engineering (DIMES) of Requirement Modeling Language (FORM-L) and on industrial the University of Calabria (Italy). He was Visiting Professor use cases developed in the context of the ITEA3 MODRIO (from January to October 2016) at NASA Johnson Space (Model Driven Physical Systems Operation) Project Center (JSC), working with the Software, Robotics, and (https://itea3.org/project/modrio.html) involving 38 partners of Simulation Division (ER). From 1999 to 2001, he was a six different European countries. researcher at CSELT, the Telecom Italia Group R&D Lab. From 2001 to 2003, he worked with the Institute of High Performance Computing and Networking of the Italian REFERENCES National Research Council (CNR). On February 2005 he received the PhD Degree in Systems and Computer [1] A. Garro, A. Tundis, D. Bouskela, A. Jardin, N. Thuy, M. Otter, L. Engineering from the University of Calabria. From January Buffoni, P. Fritzson, M. Sjölund, W. Schamai, H. Olsson. On formal 2005 to December 2011, he was an Assistant Professor of cyber physical system properties modeling: a new temporal logic language and a Modelica-based solution. Proceedings of the IEEE Computer and Systems Engineering at the DIMES Department International Symposium on Systems Engineering (IEEE ISSE 2016), (formerly DEIS) of the University of Calabria. His main Edinburg, Scotland, UK, October 03-05, 2016. research interests include: Modeling and Simulation, Systems [2] A. Garro, A. Tundis. Modeling of System Properties: research and Software Engineering, Reliability Engineering. His list of challenges and promising solutions. Proceedings of the IEEE publications contains about 100 papers published in International Symposium on Systems Engineering (IEEE ISSE 2015), international journals, books and proceedings of international Rome, Italy, September 29-30, 2015. and national conferences. In 2014, he founded the [3] M. Otter, N. Thuy, D. Bouskela, L. Buffoni, H. Elmqvist, P. Fritzson, A. Departmental Research Laboratory “System Modeling And Garro, A. Jardin, H. Olsson, M. Payelleville, W. Schamai, E. Thomas, A. Tundis. Formal Requirements Modeling for Simulation-Based Simulation Hub Lab (SMASH Lab)”. He is vice chair of the Verification. Proceedings of the 11th International Modelica Conference, Space Reference Federation Object Model (SRFOM) Product Versailles, France, September 21-23, 2015. Development Group (PDG) of SISO. He is the Technical [4] P. Fritzson, A. Garro, M. Nyberg, L. Rogovchenko-buffoni, A. Tundis. Director of the “Italian Chapter” of INCOSE (International Performing Fault Tree Analysis of a Modelica-based System Design Council on Systems Engineering). He is a member of the Executive Committee and National Coordinator for Italy in the is the Faculty Advisor and Member of the Executive MODRIO European Project. He is the Technical Leader for Committee of the Simulation Exploration Experience (SEE) UNICAL in the Open Source Modelica Consortium (OSMC). project. He is involved in the activities of the IEEE Computer He is a Member of the CINI National Lab on Cyber Security Society, IEEE Reliability Society and IEEE Aerospace and and of the Technological District on Cyber Security (DCS). He Electronic Systems Society.