|
Docente
|
TRONCI ENRICO
(programma)
Il Model Based Design (MBD) è al centro degli approcci moderni alla progettazione ed analisi di Sistemi Ciber-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.
Definizione di sistema astratto. Teoria della stabilità. Proprietà strutturali (raggiungibilità ed osservabilità). Modellazione di sistemi cyber-fisici con Modelica. Modellazione di proprietà di safety attraverso monitors. Verifica e validazione di sistemi usando statistical model checking. Self Adaptive Systems.
Materiale didattico reso disponibile dal docente sulla pagina del corso suol sito elearning della Sapienza:
https://elearning2.uniroma1.it/
Libri di testo consigliati:
A. Astolfi.
Systems and Control Theory- An Introduction. 2006.
http://www3.imperial.ac.uk/pls/portallive/docs/1/31851696.PDF
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
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
|
