Records |
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
Title |
Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation |
Type |
Conference Article |
Year |
2014 |
Publication |
In Proceedings of 17th EuroMicro Conference on Digital System Design (DSD 2014) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ |
Serial |
122 |
Permanent link to this record |
|
|
|
Author |
Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Mari, F.; Leeners, B. |
Title |
Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins |
Type |
Journal Article |
Year |
2020 |
Publication |
|
Abbreviated Journal |
Fundamenta Informaticae |
Volume |
174 |
Issue |
|
Pages |
283-310 |
Keywords |
Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation |
Abstract |
In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine ). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IOS Press |
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
1875-8681 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ |
Serial |
187 |
Permanent link to this record |
|
|
|
Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Salvo, I.; Sinisi, S.; Tronci, E.; Ehrig, R.; Röblitz, S.; Leeners, B. |
Title |
Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction |
Type |
Conference Article |
Year |
2018 |
Publication |
25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ |
Serial |
175 |
Permanent link to this record |
|
|
|
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
Title |
SyLVaaS: System Level Formal Verification as a Service |
Type |
Conference Article |
Year |
2015 |
Publication |
Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), special session on Formal Approaches to Parallel and Distributed Systems (4PAD) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ |
Serial |
123 |
Permanent link to this record |
|
|
|
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
Title |
Simulator Semantics for System Level Formal Verification |
Type |
Conference Article |
Year |
2015 |
Publication |
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ |
Serial |
125 |
Permanent link to this record |
|
|
|
Author |
Toni Mancini; Enrico Tronci; Ivano Salvo; Federico Mari; Annalisa Massini; Igor Melatti |
Title |
Computing Biological Model Parameters by Parallel Statistical Model Checking |
Type |
Journal Article |
Year |
2015 |
Publication |
International Work Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015) |
Abbreviated Journal |
|
Volume |
9044 |
Issue |
|
Pages |
542-554 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ |
Serial |
124 |
Permanent link to this record |
|
|
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
Title |
An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks |
Type |
Conference Article |
Year |
2018 |
Publication |
Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
302-312 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
Best Paper |
Approved |
no |
Call Number |
MCLab @ davi @ DBLP:conf/ismis/ManciniMMST18 |
Serial |
176 |
Permanent link to this record |
|
|
|
Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
Title |
SyLVaaS: System Level Formal Verification as a Service |
Type |
Journal Article |
Year |
2016 |
Publication |
Fundamenta Informaticae |
Abbreviated Journal |
|
Volume |
149 |
Issue |
1-2 |
Pages |
101-132 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ DBLP:journals/fuin/ManciniMMMT16 |
Serial |
160 |
Permanent link to this record |
|
|
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L. |
Title |
Parallel Statistical Model Checking for Safety Verification in Smart Grids |
Type |
Conference Article |
Year |
2018 |
Publication |
2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
1-6 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ mancini-etal:2018:smartgridcomm |
Serial |
170 |
Permanent link to this record |
|
|
|
Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
Title |
Anytime system level verification via parallel random exhaustive hardware in the loop simulation |
Type |
Journal Article |
Year |
2016 |
Publication |
Microprocessors and Microsystems |
Abbreviated Journal |
|
Volume |
41 |
Issue |
|
Pages |
12-28 |
Keywords |
Model Checking of Hybrid Systems; Model checking driven simulation; Hardware in the loop simulation |
Abstract |
Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
0141-9331 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ Mancini201612 |
Serial |
155 |
Permanent link to this record |