=Paper=
{{Paper
|id=Vol-1728/paper22
|storemode=property
|title=Formal Requirements Modeling for Simulation-Based Verification: from Theory to Practice
|pdfUrl=https://ceur-ws.org/Vol-1728/paper22.pdf
|volume=Vol-1728
|authors=Alfredo Garro
|dblpUrl=https://dblp.org/rec/conf/ciise/Garro16
}}
==Formal Requirements Modeling for Simulation-Based Verification: from Theory to Practice==
https://ceur-ws.org/Vol-1728/paper22.pdf
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.