Il Model Based Design (MBD) è al centro degli approcci moderni alla progettazione ed analisi di Sistemi Cyber-Fisici. In tale contesto, questo corso presenta metodi e tools per supportare la Verifica e Validazione (V&V) basata su modelli che, da sola, rappresenta tipicamente più del 50% del costo dello sviluppo di un sistema software industriale. Il corso presenterà metodi e tools per: modellare formalmente il comportamento del sistema da verificare; modellare formalmente i requisiti del sistema da verificare; verificare automaticamente che il sistema soddisfi i suoi requisiti. Nello specifico verranno trattati i seguenti argomenti. Modellazione di Sistemi Cyber Fisici usando DAE (Differential Algebraic Equations). V&V di sistemi cyber fisici attraverso la simulazione di DAE. Modelica. Algoritmi di simulazione di DAE. Statistical Model Checking per sistemi cyber fisici.

Materiale didattico reso disponibile dal docente sulla pagina del corso suol sito elearning della Sapienza: https://elearning2.uniroma1.it/ Libri di testo consigliati: François E. Cellier, Ernesto Kofman. Continuous System Simulation. Springer. Modelica Language Specifications. Version 3.3 - rev. 1 https://www.modelica.org/documents Open Modelica Simulator: https://openmodelica.org/ Radu Grosu, Scott A. Smolka. Monte Carlo Model Checking. Proceedings of the 11th international conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer 2005 https://pdfs.semanticscholar.org/6eb5/cddce284bfb351f47f72a2d284eb010598bc.pdf Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., and Gupta, A. 2013. Probabilistic temporal logic falsification of cyber-physical systems. ACM Transactions on Embedded Computing Systems 12, 2s, Article 95 (May 2013), DOI:http://dx.doi.org/10.1145/2465787.2465797 Antonio Filieri, Henry Hoffmann, and Martina Maggio. 2014. Automated design of self-adaptive software with control-theoretical formal guarantees. In Proceedings of the 36th International Conference on Software Engineering (ICSE 2014). Association for Computing Machinery, New York, NY, USA, 299–310. DOI:https://doi.org/10.1145/2568225.2568272 A. Astolfi. Introduction to Optimisation. http://www3.imperial.ac.uk/pls/portallive/docs/1/7288263.PDF

Il Model Based Design (MBD) è al centro degli approcci moderni alla progettazione ed analisi di Sistemi Cyber-Fisici. In tale contesto, questo corso presenta metodi e tools per supportare la Verifica e Validazione (V&V) basata su modelli che, da sola, rappresenta tipicamente più del 50% del costo dello sviluppo di un sistema software industriale. Il corso presenterà metodi e tools per: modellare formalmente il comportamento del sistema da verificare; modellare formalmente i requisiti del sistema da verificare; verificare automaticamente che il sistema soddisfi i suoi requisiti. Nello specifico verranno trattati i seguenti argomenti. Modellazione di Sistemi Cyber Fisici usando DAE (Differential Algebraic Equations). V&V di sistemi cyber fisici attraverso la simulazione di DAE. Modelica. Algoritmi di simulazione di DAE. Statistical Model Checking per sistemi cyber fisici.

Materiale didattico reso disponibile dal docente sulla pagina del corso suol sito elearning della Sapienza: https://elearning2.uniroma1.it/ Libri di testo consigliati: François E. Cellier, Ernesto Kofman. Continuous System Simulation. Springer. Modelica Language Specifications. Version 3.3 - rev. 1 https://www.modelica.org/documents Open Modelica Simulator: https://openmodelica.org/ Radu Grosu, Scott A. Smolka. Monte Carlo Model Checking. Proceedings of the 11th international conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer 2005 https://pdfs.semanticscholar.org/6eb5/cddce284bfb351f47f72a2d284eb010598bc.pdf Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., and Gupta, A. 2013. Probabilistic temporal logic falsification of cyber-physical systems. ACM Transactions on Embedded Computing Systems 12, 2s, Article 95 (May 2013), DOI:http://dx.doi.org/10.1145/2465787.2465797 Antonio Filieri, Henry Hoffmann, and Martina Maggio. 2014. Automated design of self-adaptive software with control-theoretical formal guarantees. In Proceedings of the 36th International Conference on Software Engineering (ICSE 2014). Association for Computing Machinery, New York, NY, USA, 299–310. DOI:https://doi.org/10.1145/2568225.2568272 A. Astolfi. Introduction to Optimisation. http://www3.imperial.ac.uk/pls/portallive/docs/1/7288263.PDF